PFP I: Exact Graph Repair and the Boundary Between a Proposal and a Certificate

A proposed solution and a checked solution are different objects. This paper develops that distinction within the Proposal Fidelity Protocol (PFP), in which a proposer supplies a candidate and a host checks a declared mathematical predicate before accepted state changes. The worked setting is a finite directed graph with rational edge reports and positive penalties. The weighted absolute residual of a proposed potential measures the proposal. The least such cost measures the inconsistency of the fixed reports; it is unchanged when a difference of potentials is added to the reports, and it is zero exactly when the reports are consistent. A potential and a balanced circulation within the penalties, with equal objective values, certify the minimum. On a directed cycle the minimum is the smallest penalty times the absolute cycle sum. A triangle with reports (1, 1, 1) and penalties (1, 2, 3) costs 6 at the zero potential and 3 at an optimum, matched by a unit circulation of value 3. Some optimal residual uses at most |E| − rank B edges, a weighted null-space property suffices for uniqueness, and strictly decreasing rational costs need not terminate, so a run needs finite fuel. The package contains a paper-local Python reference that builds and checks the full primal and dual certificate on small graphs, and a native Rust solver that returns the minimum and a minimizing potential by capped spanning-forest enumeration, without a dual certificate. Tests, three notebooks, a figure script, and three small Lean 4 statements accompany the manuscript. The contribution is a reproducible protocol and an exposition of established optimization facts; no model-accuracy or general reasoning claim is made.

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-10-03
DOI
https://doi.org/10.5281/zenodo.23114044
Primary Topic
Formal Methods in Verification
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

PFP I: Exact Graph Repair and the Boundary Between a Proposal and a Certificate

JEREMY H. CARROLL
Zenodo (CERN European Organization for Nuclear Research)
Formal Methods in Verification
preprint

PFP I: Exact Graph Repair and the Boundary Between a Proposal and a Certificate

JEREMY H. CARROLL
preprint en

Abstract

A proposed solution and a checked solution are different objects. This paper develops that distinction within the Proposal Fidelity Protocol (PFP), in which a proposer supplies a candidate and a host checks a declared mathematical predicate before accepted state changes. The worked setting is a finite directed graph with rational edge reports and positive penalties. The weighted absolute residual of a proposed potential measures the proposal. The least such cost measures the inconsistency of the fixed reports; it is unchanged when a difference of potentials is added to the reports, and it is zero exactly when the reports are consistent. A potential and a balanced circulation within the penalties, with equal objective values, certify the minimum. On a directed cycle the minimum is the smallest penalty times the absolute cycle sum. A triangle with reports (1, 1, 1) and penalties (1, 2, 3) costs 6 at the zero potential and 3 at an optimum, matched by a unit circulation of value 3. Some optimal residual uses at most |E| − rank B edges, a weighted null-space property suffices for uniqueness, and strictly decreasing rational costs need not terminate, so a run needs finite fuel. The package contains a paper-local Python reference that builds and checks the full primal and dual certificate on small graphs, and a native Rust solver that returns the minimum and a minimizing potential by capped spanning-forest enumeration, without a dual certificate. Tests, three notebooks, a figure script, and three small Lean 4 statements accompany the manuscript. The contribution is a reproducible protocol and an exposition of established optimization facts; no model-accuracy or general reasoning claim is made.

Zenodo (CERN European Organization for Nuclear Research)
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

PFP I: Exact Graph Repair and the Boundary Between a Proposal and a Certificate — JEREMY H. CARROLL · Zenodo (CERN European Organization for Nuclear Research) (2026) | TGRS Research Map | TGRS