Formalize singleton and mutual inductive generation - #3

Merged

johnchandlerburnham merged 67 commits into

devfrom

jcb/formalization

Aug 8, 2026

Commits on Aug 7, 2026

feat: retain constructor validation traces
johnchandlerburnham
committed
e2de5fc
docs: record L4L-01C completion
johnchandlerburnham
committed
b906b7f
proof: establish constructor universe foundation
johnchandlerburnham
committed
2c7695f
docs: record L4L-01D1 completion
johnchandlerburnham
committed
7069e6f
proof: establish post-family constructor semantics
johnchandlerburnham
committed
c66b69c
docs: record L4L-01D2 completion
johnchandlerburnham
committed
2344a9c
proof: establish pre-family constructor safety
johnchandlerburnham
committed
fe09b62
docs: record L4L-01D3 completion
johnchandlerburnham
committed
ff22360
proof: establish analyzer-owned constructor view WF
johnchandlerburnham
committed
64091a2
docs: record L4L-01D4 completion
johnchandlerburnham
committed
54b35dd
proof: establish generic singleton package closure
johnchandlerburnham
committed
9bb7bc3
docs: record L4L-01E completion
johnchandlerburnham
committed
98d3f90
proof: establish level subsumption evaluation
johnchandlerburnham
committed
75fea6b
docs: record L4L-02A completion
johnchandlerburnham
committed
f07f6f5
proof: establish level equivalence soundness
johnchandlerburnham
committed
a042697
docs: record L4L-02B completion
johnchandlerburnham
committed
89ab8f0
proof: verify constructor level comparison
johnchandlerburnham
committed
b3a9d21
docs: record L4L-02C completion
johnchandlerburnham
committed
6645ec7
proof: widen D3 constructor replay
johnchandlerburnham
committed
130da26
fix: emit recursors over checked parameters
johnchandlerburnham
committed
dfef1da
test: cover definitionally equal constructor parameters
johnchandlerburnham
committed
fd9862f
proof: certify definitionally equal parameter replay
johnchandlerburnham
committed
dbd26dc
proof: close L4L-03 validation parity
johnchandlerburnham
committed
d978220
proof: add L4L-04 normalization matrix core
johnchandlerburnham
committed
ddb79f2
proof: replay L4L-04 matrix through theory environment
johnchandlerburnham
committed
c640c90
proof: complete L4L-04 normalization matrix
johnchandlerburnham
committed
deb6efb
proof: add L4L-05 constructor-validity matrix core
johnchandlerburnham
committed
f28ce39
proof: retain normalization execution provenance
johnchandlerburnham
committed
e60e737
proof: certify executable candidate identity
johnchandlerburnham
committed
9f3b25b
proof: recover candidate execution provenance
johnchandlerburnham
committed
7821e62
proof: expose transparent validation replay
johnchandlerburnham
committed
4ed3f82
proof: replay accepted constructor validity fixtures
johnchandlerburnham
committed
807d912
proof: make fixture closure checks structural
johnchandlerburnham
committed
93ab2d0
proof: reduce fixture replay oracle surface
johnchandlerburnham
committed
b5d6d8f
checker: make normalization equality transparent
johnchandlerburnham
committed
1458f76
checker: add structural identity replay
johnchandlerburnham
committed
cdd55d6
checker: replay accepted family identities
johnchandlerburnham
committed
d2d988f
checker: replay accepted constructor identities
johnchandlerburnham
committed
85dd4d2
proof: derive fixture replay shapes structurally
johnchandlerburnham
committed
903f24f
proof: replay Prop constructor universes structurally
johnchandlerburnham
committed
6f537e4
proof: recover exact candidate views structurally
johnchandlerburnham
committed
a7bca5f
proof: replay PRB validation and alignment structurally
johnchandlerburnham
committed
e232cf9
proof: replay PRB pre-family safety structurally
johnchandlerburnham
committed
b78403e
proof: close L4L-05 constructor validity parity
johnchandlerburnham
committed
0293093
proof: generalize recursor generation by elimination mode
johnchandlerburnham
committed
ceca681
proof: certify elimination mode and recursor levels
johnchandlerburnham
committed
460b6d8
proof: certify recursor K-target metadata
johnchandlerburnham
committed
6e3f6c5
proof: close K-target parity
johnchandlerburnham
committed
1462a11
proof: cover empty and singleton generation edges
johnchandlerburnham
committed
66a502e
proof: close empty and singleton edge parity
johnchandlerburnham
committed
dc750a0
verify: add singleton parity matrix
johnchandlerburnham
committed
85a48d0
verify: add singleton rejection and replay inventories
johnchandlerburnham
committed
3c010c2
verify: replay all fixed singleton families
johnchandlerburnham
committed
8411d55
verify: close L4L-07 singleton parity
johnchandlerburnham
committed
349a5d6
theory: add mutual checked representation
johnchandlerburnham
committed
d695b3d
inductive: complete mutual validation semantics
johnchandlerburnham
committed
b26262a
inductive: add block-wide mutual generation
johnchandlerburnham
committed
12040b3
ci: reconcile the sorry audit with the formalization line
johnchandlerburnham
committed
6bc3079
inductive: type mutual motive selection
johnchandlerburnham
committed
3d97ac1
inductive: type mutual minors and recursors
johnchandlerburnham
committed
6311fa6
inductive: establish mutual recursor transaction invariants
johnchandlerburnham
committed
48882b9
inductive: prove mutual rule generation well-formed
johnchandlerburnham
committed
67d6592
inductive: compare complete mutual kernel metadata
johnchandlerburnham
committed
1d28096
inductive: replay mutual blocks through environments
johnchandlerburnham
committed
eeae528
inductive: generalize public transaction to mutual blocks
johnchandlerburnham
committed
1159c65
inductive: audit mutual metadata and replay
johnchandlerburnham
committed
aa10005
inductive: close mutual generation milestone
johnchandlerburnham
committed
c8977a1