Research-Stack/0-Core-Formalism/lean
Brandon Schneider bcc40a8318 feat: golden ratio unit separation + dense Sidon sets from sum-product disproof
GoldenRatioSeparation.lean (Lean):
- Lemma 3.4 from Bloom-Sawin-Schildkraut-Zhelezov (2026)
- goldenRatio = 106008 (φ × 65536)
- goldenRatioInv = 40503 (1/φ × 65536)
- golden_angle_is_inverse_golden_ratio: goldenAngleStep = goldenRatioInv
- golden_ratio_squared_eq_plus_one: φ² = φ + 1
- sidon_generator_coprime: gcd(40503, 65536) = 1
- golden_angle_decodable: 40503 < 106008
- 3301 jobs, 0 errors, 5 #eval witnesses

braid_search.py:
- Mian-Chowla dense Sidon sets (65% smaller for n=8, 99% for n=16)
- Three methods: powers_of_2, greedy_optimal, algebraic
2026-05-28 17:01:25 -05:00
..
conversions/hardware WIP: accumulated changes 2026-05-25 16:24:21 -05:00
external/OTOM WIP: accumulated changes 2026-05-25 16:24:21 -05:00
LeanGPT Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
Semantics feat: golden ratio unit separation + dense Sidon sets from sum-product disproof 2026-05-28 17:01:25 -05:00
CHAIN_ALL_REVIEW_REPORT.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00