allaun f6cf32e2a7 fix(lean): add crossInputGap + strengthen cleanMerge_preservesGap ... Theorem restated with crossInputGap hypothesis (no active bin from s adjacent to active bin from e). Without this, the theorem is false: counterexample s=[1,0,1,0,...] e=[0,0,0,1,0,1,...] has merge with adjacent active bins despite resonanceDegeneracy=0. Added to Spectrum.lean: - crossInputGap: cross-input adjacency check on adjacent bin pairs Added to GraphRank.lean: - boolGap8: boolean gap check on 8 explicit values - Complete mathematical proof sketch in docstring (4 steps) The sorry remains: the Q16_16↔Bool bridge for 8-element lists requires list-level induction on activeBins/verifySpectralGap/resonanceDegeneracy/ crossInputGap. The boolean kernel (boolGap8) is defined and ready for native_decide verification once the bridge is automated. Build: 3314 jobs, 0 errors (Compiler surface)		2026-06-22 13:35:26 -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): add crossInputGap + strengthen cleanMerge_preservesGap	2026-06-22 13:35:26 -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