allaun b5babeba06 fix(lean): improve cleanMerge_preservesGap proof sketch ... The sorry remains but now has a concrete proof strategy: - Boolean abstraction: convert Q16_16 bins to Bool (zero vs non-zero) - Prove gap-preservation on finite 2^8 boolean model (native_decide) - Lift to Q16_16 via contrapositive: merge active → input active Blocker: native_decide can't handle free List Bool variables; needs Fin 8 → Bool representation or custom tactic for the lift. See TODO(lean-port) marker in theorem docstring.		2026-06-22 13:06:27 -05:00
..
conversions/hardware	chore(repo): push local 768-commit branch state onto clean remote baseline	2026-06-15 22:46:50 -05:00
external/OTOM	feat(lean): close gaussian_line_integral_unit_dir + consolidate infrastructure	2026-06-18 16:53:23 -05:00
LeanGPT	Remove legacy Python prototypes superseded by Lean formalization	2026-05-19 15:34:17 +00:00
Semantics	fix(lean): improve cleanMerge_preservesGap proof sketch	2026-06-22 13:06:27 -05:00
singer-theorem-lean	chore(repo): push local 768-commit branch state onto clean remote baseline	2026-06-15 22:46:50 -05:00
CHAIN_ALL_REVIEW_REPORT.md	initial: sovereign research stack (consolidated, weightless, and lfs-optimized)	2026-05-04 18:11:36 -05:00