saymrwulf/ltl-accumulator-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/ltl-accumulator-verified.git synced 2026-09-03 19:53:48 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
ltl-accumulator-verified/verification/Proofs
History
mrwulf f47663b890 S5.3 drill (2nd pass): anchor refactor-equivalence provenance to git history 
The previous drill's equivalence theorems were only as strong as their
RHS matching the ACTUAL historical base (not a from-memory
reconstruction) and 'nothing else changed' being true. Both now verified
against the repository itself: git show cfde9b2 confirms the RHS forms
verbatim; git diff cfde9b2..8795e82 confirms the refactor is base-only
(eight lines). Provenance recorded in Refactor.lean's header so the
argument is self-contained: unchanged remainder (git) + equal base
(kernel) => whole-function equality. 26 certs green. LTL untouched.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
2026-07-11 19:55:38 +02:00
..
AxiomCheck.lean S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact) 2026-07-11 19:25:04 +02:00
AxiomCheck.olean S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact) 2026-07-11 19:25:04 +02:00
Basic.lean S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) 2026-07-11 19:18:26 +02:00
Basic.olean S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) 2026-07-11 19:18:26 +02:00
Binding.olean S3/L4-L5: root binding (Lemma 2, Path instance) + Theorem 2, constructive 2026-07-11 13:21:17 +02:00
Binding3.lean S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) 2026-07-11 19:18:26 +02:00
Binding3.olean S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) 2026-07-11 19:18:26 +02:00
Completeness.lean S3.5: explicit collision extractor — Theorem 2 made non-vacuous, vacuous forms removed 2026-07-11 15:31:21 +02:00
Completeness.olean S3.5: explicit collision extractor — Theorem 2 made non-vacuous, vacuous forms removed 2026-07-11 15:31:21 +02:00
Consistency.lean S5 stage 2: extractConsNode extractor defined (consistency, Theorem 3 steps 1-2) 2026-07-11 17:55:51 +02:00
Consistency.olean S5 stage 2: extractConsNode extractor defined (consistency, Theorem 3 steps 1-2) 2026-07-11 17:55:51 +02:00
Descent.lean S4: descent extractor extractMTH (Theorem 3 step 3 + F2 restoration), non-vacuous 2026-07-11 16:46:58 +02:00
Descent.olean S4: descent extractor extractMTH (Theorem 3 step 3 + F2 restoration), non-vacuous 2026-07-11 16:46:58 +02:00
Extract.lean S3.5 Fable re-audit: permanent non-vacuity witness + honest ledger 2026-07-11 16:38:34 +02:00
Extract.olean S3.5 Fable re-audit: permanent non-vacuity witness + honest ledger 2026-07-11 16:38:34 +02:00
Probe.olean S3.5: explicit collision extractor — Theorem 2 made non-vacuous, vacuous forms removed 2026-07-11 15:31:21 +02:00
ProbeAx.olean S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) 2026-07-11 19:18:26 +02:00
ProbeInduct.olean S5.3: consRecBinding PROVEN — Theorem 3 steps 1-2 kernel-checked (the hardest object) 2026-07-11 19:18:26 +02:00
ProbeRefactor.olean S5.3 Fable re-audit: machine-verify the ConsRec base refactor (permanent artifact) 2026-07-11 19:25:04 +02:00
Refactor.lean S5.3 drill (2nd pass): anchor refactor-equivalence provenance to git history 2026-07-11 19:55:38 +02:00
Refactor.olean S5.3 drill (2nd pass): anchor refactor-equivalence provenance to git history 2026-07-11 19:55:38 +02:00