Proof Path TheoryStatements and proofs
Statements and proofs
Find a statement anywhere in this work by title, printed number, type or source label. Entries follow the chapter order. Each proof link opens the written proof passage.
Statements by chapter
Claim types and logical boundaries
Typed proof fields
The ambient proof field and the meaning of failure
Certificates and verification closure
Alternative derivations and certificate complexity
Certified paths as a category
Komorebi Space, realization fibers, and informative questions
A checked realization bridge for proof fields
- Theorem 9.1: Soundness and relative completeness
- Proposition 9.2: The proof-field view laws
- Theorem 9.3: Whole-support gluing
- Example 9.4: Pairwise dependencies do not suffice
- Theorem 9.5: A linear certificate alternative
- Theorem 9.6: Exact observation counts
- Theorem 9.7: Least protected extension and a complete obstruction
- Corollary 9.8: Exact extension of a partial valuation
- Proposition 9.9: Staged closure and persistent obstructions
- Theorem 9.10: Exact criterion for universal gluing
- Theorem 9.11: Compositional rule transport
- Example 9.12: Why transport is not an equivalence
- Definition 9.13: Finite indexed problem and trace
- Theorem 9.14: Replay preserves derivability and composes
- Theorem 9.15: Acceptance identifies the least seeded model
- Definition 9.16: Checked forbidden-node witness
- Theorem 9.17: Sound and complete obstruction witnesses
- Corollary 9.18: Meaning of a complete result certificate
- Theorem 9.19: Lossless encoding at the typed syntax boundary
- Theorem 9.20: Accepted JSON records certify their decoded answer
Compression relative to a task family
- Definition 10.1: Task
- Definition 10.2: Task-sufficient representation
- Theorem 10.3: Task information loss criterion
- Definition 10.4: Recoverability preorder
- Proposition 10.5: Recoverability is a preorder
- Corollary 10.6: Quotient poset
- Definition 10.7: Retention projection
- Theorem 10.8: Retention projection algebra
- Corollary 10.9: Task monotonicity under retention
- Theorem 10.10: Task-family dependence of minimal compression
- Theorem 10.11: All predicates distinguish exactly injective encodings
- Theorem 10.12: Attained factorization and unique decoding
- Example 10.13: The empty-domain boundary
- Theorem 10.14: Joint task representation and compositional recovery
Endpoint, audit, and discovery equivalence
Vector-valued loss
Compression debt
A proof ecology rather than one ideal form
Proof compilers and shared ledgers
Latent bridge graphs
Retention under a budget
Versioned proof objects
Evidence ledgers and provenance
Correlated review
Shared interpretation, review dependence, and identification
Verification bandwidth and audit queues
Recursive proof cubes and expansion depth
Open theorem program
- Problem 28.1: Proof-path view functors and comparison
- Problem 28.2: Counterfactual proof-search observations
- Problem 28.3: Collective evaluation without shared-context confounding
- Problem 28.4: Infinite proof fields
- Problem 28.5: Parameterized certificate complexity
- Problem 28.6: Probabilistic bridge calibration
- Problem 28.7: Proof assistant interoperability
- Problem 28.8: Higher proof transformations
- Problem 28.9: Privacy and attribution
- Problem 28.10: Empirical validation
- Problem 28.11: Distributed audit systems