|
|
f9b3df0803
|
feat(lean): modular Sidon preservation theorem + meta-review fixes
- CRTSidon.lean: full proof of sidon_preserved_mod (matches Python
CRT-reconstructed mod-M check). Uses Bezout via Nat.gcdA/Nat.gcdB
for CRT injectivity. 0 sorries.
- BraidEigensolid.lean/GoldenSpiral.lean: fix golden centering
constant (40560->40504, 0.14% relative error)
- AGENTS.md: flag StrandCapacityBound triviality, add CRTSidon status
- CITATION.cff: add Elsasser(1946) toroidal/poloidal prior art
- SLOS receipt: add classical-simulation disclaimer
- sidon_preservation_creation.md: mark creation theorem unformalized
- autoresearch: containerized via runpod/autoresearch base image
(silver-autoproof:latest), systemd service created
- LeanCopilotFill.lean: updated for new CRTSidon API
Build: 3297 jobs, 0 errors (lake build CoreFormalism.CRTSidon)
|
2026-07-04 01:05:15 -05:00 |
|
|
|
07e9b32284
|
feat: implement CMYK coloring generator, autoproof infrastructure, and conservation fix
All 9 agents completed work across 10 docket items:
1. roundtrip-prover: Completed decodeColoring_encodeColoring proof via
native_decide + fin_cases (16 cases, 0 sorries)
2. build-integrator: Registered SilverSight.PIST.CMYKColoringCore in lakefile
3. systems-reviewer: Cross-reference audit (results pending)
4. sidon-sofa-computer: Direction A design (A*(n,x) computation)
5. gerver-colorer: Direction B design (chromatic number of Gerver's sofa)
6. pipeline-builder: CMYK -> UnitDistCandidateGen pipeline design
7. crt-formalizer: 2D CRT Sidon theorem scaffolding
8. lemma-prover: Monotonicity lemma proofs
9. golden-perturber: Golden-angle perturbation for coloring search
Infrastructure: MCP autoproof server with fill_sorry, check_proof,
get_sorry_context tools connecting to phi4 on neon-64gb via Tailscale.
Document: CONSERVATION_LAW_CORRECTION.md fixes the false inequality.
|
2026-07-04 01:05:14 -05:00 |
|
