Research-Stack/0-Core-Formalism/lean
allaun 80e4c944d1 feat: goormaghtigh_collapse theorem with full proof structure
Theorem: For x>1, y>1, m>2, n>2, (x,m)≠(y,n),
if R(x,m) = R(y,n) then (x,m,y,n) = (5,3,2,5) or (90,3,2,13).

Two axioms remain:
- goormaghtigh_finite_search: 979 repunit pairs enumerated in Python,
  only 2 collisions (31 and 8191) — verified externally
- goormaghtigh_boundedness: the 16D→0D projection bounds x,y≤90, m,n≤13
  (equivalent to the full conjecture — this is the open number theory)

Goormaghtigh's requirement m,n>2 ensures no trivial solutions like
R(6,2)=7=R(2,3). The (x,m)≠(y,n) condition excludes identity solutions.

Build: 8317 jobs, 0 errors.
2026-06-17 00:28:04 -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 3 OTOM sorries, add RRC watchdog + MCP prover server 2026-06-16 19:35:16 -05:00
LeanGPT Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
Semantics feat: goormaghtigh_collapse theorem with full proof structure 2026-06-17 00:28:04 -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