27 Limitations and claim boundaries
On this page · Permalink · Source line 2294
Proof Path Theory does not establish a theorem by preserving the history of an argument. A richly documented wrong proof remains wrong. Bridge value is not validity. Explanatory power is not validity. Consensus is not validity. The certified subfield remains the object that carries deductive force.
The dependency graph is a declared model. It records the dependencies that were formalized, not every historical influence on discovery. Tacit knowledge, visual intuition, unrecorded conversations, and changes in vocabulary may be absent.
The value and cost coordinates are task models. Verification can often be specified sharply. Meaning and future bridge value are partly prospective. Their use is justified when assumptions are stated, not when the numbers are treated as intrinsic physical constants.
The finite bridge graph does not predict every future theorem. It supports conditional statements of the form: under these declared future targets and transfer edges, this retention policy preserves this amount of modeled reach.
The exact minimum certificate algorithm is exponential in the worst case. The package makes this limitation explicit through a search-state bound.
The review and queue models are deliberately elementary. They isolate dependence and capacity effects, but they do not model every institutional or psychological feature of mathematical review.
Finally, the monograph does not claim that graphs, hypergraphs, proof theory, submodular optimization, covariance-aware aggregation, or queueing recurrences were invented here. The contribution is the formal assembly of these structures around proof compression, discovery fields, mathematical memory, and versioned proof portfolios.
The remaining implementation boundary.
On this page · Permalink · Source line 2312
Theorem 9.20 proves the meaning of an accepted decoded answer. It does not prove that every named-field export preserves its source, or that the text parser and Python producer always realize that contract. Those are the next refinement obligations, not hypotheses silently supplied by successful tests.