allaun b54a1f1ed6 fix(lean): analyze cleanMerge_preservesGap — theorem false as stated ... Discovery: the theorem with only resonanceDegeneracy=0 is FALSE. Counterexample: s=[1,0,1,0,...] e=[0,0,0,1,0,1,...] — no overlap, both gap-valid, but merge has adjacent active bins at positions 2,3. Missing hypothesis: cross-input gap (no active bin from s adjacent to active bin from e). This holds in Sidon-basis context (powers-of-2 labels ensure min separation ≥ 2). The sorry is now documented with: - Exact counterexample - Required cross-input gap hypothesis - Proof path when cross-gap is available - Boolean model (Fin 8 → Bool) verification strategy Build: 3314 jobs, 0 errors (Compiler surface)		2026-06-22 13:23:45 -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): analyze cleanMerge_preservesGap — theorem false as stated	2026-06-22 13:23:45 -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