Formal-Verification Proofs — Records

Append-only record of formal proof documentation written in prose (proof notes and invariant write-ups) for the library's correctness arguments. These capture the proofs of subsumption properties and position invariants, plus subdirectory collections for higher-layer proofs. Preserved verbatim as a record of the verification effort. For the authoritative status of machine-checked artifacts, see the verification manifest at ../../verification/FORMAL_VERIFICATION_MANIFEST.tsv.

Records

• 01_subsumption_properties.md — Subsumption Properties — Formal Proof Documentation
• 02_position_invariants.md — Position Invariants — Formal Proof Documentation
• 06_contextual_completion/ — Contextual completion proofs (context visibility, draft consistency, checkpoint stack, query fusion, distance correctness, hierarchical visibility, finalization)

Status: Historical — append-only scientific record; indexed, not edited.

← Documentation Index