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
- JEREMY H. CARROLL
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