26 What the theory establishes
On this page · Permalink · Source line 2262
The finite theory establishes the following structural facts.
A proof field can represent conjunction within a justification and alternatives among justifications without confusing candidate edges with certified edges.
Derivability in a finite acyclic selected subfield is well defined and computable in topological order.
A fixed AND-DAG, expanded only outside its admitted leaves, has a least certificate pair.
Alternative derivations make minimum certificate selection NP-complete in general.
Compression is meaningful only relative to a task family.
Task-relative recoverability forms a preorder and a quotient partial order.
Verification loss, discovery loss, meaning loss, bridge loss, and audit loss can diverge.
Expected reconstruction debt decreases monotonically as more required material is retained.
Bridge criticality is domination in the declared future-reach graph.
Weighted future reach is monotone and submodular.
Greedy cardinality retention has the standard \((1-1/e)\) guarantee.
Append-only certified updates preserve existing derivability.
The forward dependency closure is the least set containing the changed nodes and closed under outgoing dependency edges. It marks potential review, not automatic falsehood.
Positive review dependence lowers the variance-equivalent count. Under a positive definite covariance model, generalized least squares gives the minimum-variance unbiased linear aggregate.
Constant-rate audit queues have an exact stable, critical, or unstable classification.
Optimal proof expansion depth depends on the presentation goal.
These results turn the original methodological insight into a finite mathematical branch with explicit objects, algorithms, complexity, and failure boundaries.
The extension results add three further capabilities. A protected rule-model request returns its least feasible model or a derivation of a forbidden node. A cover has universal gluing exactly when its visible rules entail every original rule. A representation admits a task decoder exactly when equal encodings have equal task answers. These outputs are respectively model witnesses, rule derivations, and decoding or collision witnesses. None can replace the others merely because it is called a certificate.
The realization theory gives the proof field a contravariant diagram of local models and an explicit equivalence with its coherent sections. Whole-support gluing proves extension from suitably covering patches. The protected linear alternative classifies feasible fibers and supplies normalized witnesses for infeasibility. Exact finite-field counts yield an information formula only after a uniform distribution is chosen. The native exporter supplies syntactic dependencies from compiled declarations, not the complete history of discovery.