allaun
07e9b32284
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.
2.9 KiB
Conservation Law Correction Summary
Date: 2026-07-03
File: docs/research/SIDON_SOFA_COLORING.md, Section 5.5 (lines 248-349)
Status: CORRECTED
What Was Wrong
The original claim in Section 5.5 was:
log(Area(S)) + log(χ(Γ_γ)) ≥ K(P)
This inequality is demonstrably false. The counterexample:
- Let S be a disk of radius ε = 10⁻¹⁰
- Area(S) = πε² ≈ 3.14 × 10⁻²⁰
- log₂(Area) ≈ -64.8 (negative!)
- χ(Γ_γ) = 1 (no unit-distance edges for tiny disk)
- log₂(χ) = 0
- LHS = -64.8, RHS = K(P) ≥ 0
- Claim: -64.8 ≥ 0 ✗ FALSE
Root Cause
The original conservation law from INVARIANT_COMPUTATION_GEOMETRY.md:
program_size + residual_size ≥ K(data)
works because both terms are description lengths (non-negative bit-counts). The sofa version incorrectly substituted:
log(Area)for program_size — but Area is a geometric measure that can be < 1, making log negativelog(χ)for residual_size — but this captures only O(log n) bits, while K(P) scales as Ω(n log n)
The analogy conflated geometric quantities with information-theoretic quantities.
The Corrected Version
Valid inequality (proven by chain rule):
K(S) + K(γ) + K(P | S, γ) ≥ K(P) - O(log n)
where:
- K(S) = Kolmogorov complexity of the shape description
- K(γ) = Kolmogorov complexity of the motion path
- K(P | S, γ) = conditional complexity of boundary points given shape and motion
- K(P) = total Kolmogorov complexity of the Sidon boundary set
This is proven (chain rule of Kolmogorov complexity) and preserves the intended conservation intuition: you cannot simultaneously minimize shape complexity, motion complexity, and residual specification cost below the information content of the boundary structure.
Geometric version (open conjecture):
A conservation-type inequality using native geometric quantities (Area, χ) requires:
- Non-negative area term (e.g., log₂(Area/ε₀²) instead of log₂(Area))
- Coloring cost scaled by n (n · ⌈log₂(χ)⌉ instead of log₂(χ))
- Sidon density coupling (n ≤ O(D/ε) relates area to boundary complexity)
Whether such a bound exists is an open question.
What Changed in the Document
Lines 248-349 now contain:
- Reference to the original conservation law with explanation of why it works
- The valid K-based analog with proof sketch
- Operational meaning of the trade-off
- Explicit counterexample showing why the geometric version fails
- Root cause diagnosis
- Open conjecture with precise conditions for a geometric version
Lines 350+ remain unchanged (Section 6 onwards).
Honesty About Proven vs. Conjectural
- ✅ Proven: The K-based inequality (chain rule of Kolmogorov complexity)
- ⚠️ Open: Whether a geometric version with Area and χ exists
- ❌ Disproven: The original claim log(Area) + log(χ) ≥ K(P)
The correction is honest about what's known and what remains conjectural.