B Theorem ledger
On this page · Permalink · Source line 2450
Written denotes a written proof. Lean denotes the specified interface with fresh compiler and kernel-replay evidence in this edition, not a formalization of the entire monograph. Mixed distinguishes checked counts from their written probabilistic interpretation. The separate Lean concordance lists every source declaration and its scope.
| ID | RESULT AND IMPLEMENTATION SUPPORT | EVIDENCE |
|---|---|---|
| PPT-001 | Finite derivability is unique and computable in topological order. ProofField.derive | Written |
| PPT-002 | An AND-DAG has a least certificate pair, stopping at admissible leaves. unique_and_dag_certificate | Written |
| PPT-003 | AND-DAG core extraction is linear with indexed adjacency. graph algorithm, not a runtime certificate | Written |
| PPT-004 | Minimum Certificate Decision is NP-complete. Set Cover example | Written |
| PPT-005 | Certified paths transport functorially. structural theorem | Written |
| PPT-006 | Local auditable certificates compose under a certificate functor. structural theorem | Written |
| PPT-007 | Task information loss follows from compression collisions. task API | Lean |
| PPT-008 | Recoverability is a preorder. recoverability_preorder | Written |
| PPT-009 | The quotient by mutual recoverability is a partial order. equivalence API | Written |
| PPT-010 | Least sufficient retention masks depend on the task family. finite countermodel | Written |
| PPT-011 | Zero verification loss can coexist with positive discovery loss. AND-DAG example | Written |
| PPT-012 | Compression debt is monotone under retention. compression_debt | Written |
| PPT-013 | Bridge criticality equals target domination. dominated_targets | Written |
| PPT-014 | Weighted future reach is monotone and submodular. exhaustive finite checker | Written |
| PPT-015 | Greedy cardinality retention achieves at least \(1-1/e\) for positive feasible cardinality budgets. greedy and exact solvers | Written |
| PPT-016 | Append-only certified updates preserve derivability. versioning check | Written |
| PPT-017 | Forward dependency closure is the minimal closed syntactic review set. affected_descendants | Written |
| PPT-018 | Equicorrelated review has the stated effective count. covariance implementation | Written |
| PPT-019 | GLS weights minimize unbiased linear review variance. generalized_least_squares_weights | Written |
| PPT-020 | Constant-rate audit queues have exact stable, critical, and unstable regimes. queue simulation | Written |
| PPT-021 | Optimal expansion depth depends on the goal. refinement implementation | Written |
| PPT-022 | Pure retention projections commute and are idempotent. retention_projection | Written |
| PPT-023 | Retention masks form a Boolean lattice. retention_meet, retention_join | Written |
| PPT-024 | A locally refuted route can coexist with another certified route. Alternative justification field | Written |
| PPT-025 | A checked local refutation persists under unchanged interpretation. Scoped witness principle | Written |
| PPT-026 | Finite arrow-covered matching views glue uniquely. FiniteViewSystem.glue | Lean |
| PPT-027 | Protected realizations admit exact solutions or obstruction witnesses, with classified fibers. analyze_affine_realizations | Lean |
| PPT-028 | Finite affine fibers have exact observation counts. Uniform entropy is a written corollary. Lean counts and binary tests | Mixed |
| PPT-029 | Common offset and correlated error have the displayed reviewer MSE. shared_bias_mse | Written |
| PPT-030 | Declared derivability equals membership in every declared field model. Closure and countermodels | Lean |
| PPT-031 | Local models form a contravariant diagram with an explicit realization equivalence. Field.modelEquivSections | Lean |
| PPT-032 | Whole-support matching local models glue. Pairwise coverage can fail. Proof-field views and counterexample | Lean |
| PPT-033 | All predicate tasks are sufficient exactly for injective encodings. Compression collision theorem | Lean |
| PPT-034 | Attained decoding is equivalent to fiber constancy. The decoder is unique on attained values. Recovery and finite decoder checks | Lean |
| PPT-035 | Joint tasks are sufficient exactly when each coordinate task is. Recovery maps compose. Recovery and joint partitions | Lean |
| PPT-036 | Protected rule data have an extension exactly when their least closure avoids the forbidden nodes. Extension and independent trace replay | Lean |
| PPT-037 | Closing earlier data before later data preserves the closure. Adding observations preserves obstructions. Extension | Lean |
| PPT-038 | A cover has universal gluing exactly when its visible rules entail every original rule. SemanticCover and finite cover certificates | Lean |
| PPT-039 | Typed rule transports preserve derivations, pull models back, and transport obstruction witnesses. RuleTransport | Lean |
| PPT-040 | A valid rule transport can collapse compatible source observations into an impossible target request. ExtensionExamples | Lean |
| PPT-041 | Hashing cannot add recoverable tasks. Restricted injectivity prevents further task loss. Recovery | Lean |
| PPT-042 | Executable trace replay preserves derivability and composes. Trace and TraceCompleteness | Lean |
| PPT-043 | Accepted complete traces identify the least seeded model. Trace and TraceCompleteness | Lean |
| PPT-044 | Accepted forbidden-node witnesses exist exactly for infeasible protected requests. Trace and TraceCompleteness | Lean |
| PPT-045 | Typed JSON encoding has a left inverse and is injective. Trace.Wire | Lean |
| PPT-046 | Accepted JSON records certify the exact decoded protected answer. Trace.Wire | Lean |
| PPT-047 | Valid indexed problems derive only bounded node addresses. Trace.Wire | Lean |