Iota Reduction - #43

Open

barabbs wants to merge 14 commits into

digama0:masterfrom

Commits on Jul 21, 2026

refactor: relocate Pattern core to Theory/Pattern
barabbs
committed
cb920e1
feat: add pats schematic-rule registry to VEnv
barabbs
committed
5a4bdda
feat: add IsDefEq.pat iota rule and discharge break-fixes
barabbs
committed
a3d6076
feat: real VEnv.addInduct with iota-rule registration
barabbs
committed
41f3fb6
feat: addInduct env-extension lemmas and Params instance
barabbs
committed
e92f762
feat: Verify AddInduct wiring and exposed downstream iota lemmas
barabbs
committed
d0a1ae7
feat: prove TrEnv.pats_iota (remove consumer trust surface)
barabbs
committed
9e186e6
feat: discharge three Params side-conditions via pats population invariant
barabbs
committed
3c78d08

Commits on Aug 6, 2026

Commits on Aug 7, 2026

refactor: keep Pattern.lean in Theory/Typing (revert M0 relocation)
barabbs
committed
3bbdb22

Commits on Aug 8, 2026

docs: trim iota comments to the repo's terser style
barabbs
committed
349da4b

Commits on Aug 11, 2026

feat: name the ι witness and compose it into an ι-reduction step
barabbs
committed
1a1ebe8

Commits on Aug 18, 2026

fix: repair Lean4Lean.Experimental for the ι additions
barabbs
committed
eddf009