SilverSight/formal
allaun dfc53bffeb fix: HachimojiN8 theorem bug, all Lean module tests pass
- HachimojiN8: n8_is_minimum had inverted truth (claimed allOk=true for N<8
  but the theorem proves allOk=false for all N<8). Fixed statement.
- Tests: 9/9 Lean module tests passing (FeasibleSet, RRC Emit, Q16_16Manifold,
  FixedPoint, SidonSets, InteractionGraphSidon, GoormaghtighEnumeration, HachimojiN8)
- Entry gate now checks GoormaghtighEnumeration (2 known Goormaghtigh collisions:
  31 and 8191) as a cached-artifact check (heavy decide ~480K quadruples)
- SidonSets added to entry gate (Erdos bounds on Sidon sets)
2026-06-30 06:29:34 -05:00
..
BindingSite feat(phi): Hachimoji N=8 foundation, Phi pipeline, AVMIsa audit report 2026-06-28 00:11:39 -05:00
CoreFormalism chore: commit all pending work from prior sessions 2026-06-30 04:54:40 -05:00
PVGS_DQ_Bridge chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
RRCLib feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SilverSight fix: HachimojiN8 theorem bug, all Lean module tests pass 2026-06-30 06:29:34 -05:00
UniversalEncoding chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00