mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
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.
70 lines
2.9 KiB
Text
70 lines
2.9 KiB
Text
import Mathlib.Data.Nat.GCD.Basic
|
||
import Mathlib.Data.Finset.Basic
|
||
import Mathlib.Tactic
|
||
|
||
open Finset
|
||
|
||
namespace CoreFormalism.CRTSidon
|
||
|
||
/-- A Sidon set: all unordered pairwise sums are distinct. -/
|
||
def IsSidon (A : Finset ℕ) : Prop :=
|
||
∀ ⦃a b c d : ℕ⦄, a ∈ A → b ∈ A → c ∈ A → d ∈ A → a + b = c + d →
|
||
(a = c ∧ b = d) ∨ (a = d ∧ b = c)
|
||
|
||
/-- Pairwise coprime list. -/
|
||
def PairwiseCoprime (ls : List ℕ) : Prop :=
|
||
∀ i j (hi : i < ls.length) (hj : j < ls.length), i < j →
|
||
(ls.get ⟨i, hi⟩).gcd (ls.get ⟨j, hj⟩) = 1
|
||
|
||
/-- CRT Torus Embedding of label a with sum parameter S and moduli L₀::Ls. -/
|
||
def crtEmbed (a S : ℕ) : List ℕ → List ℕ
|
||
| [] => []
|
||
| L₀ :: Ls => (a % L₀) :: (Ls.map fun Lᵢ => (S - a) % Lᵢ)
|
||
|
||
/-- Project the first element of a vector (0 for empty). -/
|
||
def vecFirst (v : List ℕ) : ℕ :=
|
||
match v with
|
||
| [] => 0
|
||
| x :: _ => x
|
||
|
||
/-- Componentwise vector sum. -/
|
||
def vecAdd (v w : List ℕ) : List ℕ :=
|
||
List.zipWith (· + ·) v w
|
||
|
||
lemma vecFirst_crtEmbed (a S L₀ : ℕ) (Ls : List ℕ) (ha : a < L₀) :
|
||
vecFirst (crtEmbed a S (L₀ :: Ls)) = a := by
|
||
simp [crtEmbed, vecFirst, Nat.mod_eq_of_lt ha]
|
||
|
||
lemma vecFirst_vecAdd_crtEmbed (a b S L₀ : ℕ) (Ls : List ℕ) (ha : a < L₀) (hb : b < L₀) :
|
||
vecFirst (vecAdd (crtEmbed a S (L₀ :: Ls)) (crtEmbed b S (L₀ :: Ls))) = a + b := by
|
||
simp [vecAdd, crtEmbed, vecFirst, Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb]
|
||
|
||
/-- Total modulus M = ∏ Lᵢ. -/
|
||
def totalMod (L : List ℕ) : ℕ := L.prod
|
||
|
||
/-- **Main Theorem**: CRT Torus embedding preserves the Sidon property.
|
||
If A is a Sidon set, every label in A is bounded by the identity modulus L₀,
|
||
and S is any sum parameter, then the CRT-embedded vectors are also Sidon
|
||
under componentwise vector addition. -/
|
||
theorem sidon_preserved (A : Finset ℕ) (hSidon : IsSidon A) (S L₀ : ℕ) (Ls : List ℕ)
|
||
(hBound : ∀ a ∈ A, a < L₀) :
|
||
∀ ⦃a b c d : ℕ⦄, a ∈ A → b ∈ A → c ∈ A → d ∈ A →
|
||
vecAdd (crtEmbed a S (L₀ :: Ls)) (crtEmbed b S (L₀ :: Ls)) =
|
||
vecAdd (crtEmbed c S (L₀ :: Ls)) (crtEmbed d S (L₀ :: Ls)) →
|
||
(a = c ∧ b = d) ∨ (a = d ∧ b = c) := by
|
||
intro a b c d ha hb hc hd hvec
|
||
have ha_lt : a < L₀ := hBound a ha
|
||
have hb_lt : b < L₀ := hBound b hb
|
||
have hc_lt : c < L₀ := hBound c hc
|
||
have hd_lt : d < L₀ := hBound d hd
|
||
have hfirst : a + b = c + d := by
|
||
calc
|
||
a + b = vecFirst (vecAdd (crtEmbed a S (L₀ :: Ls)) (crtEmbed b S (L₀ :: Ls))) := by
|
||
symm; exact vecFirst_vecAdd_crtEmbed a b S L₀ Ls ha_lt hb_lt
|
||
_ = vecFirst (vecAdd (crtEmbed c S (L₀ :: Ls)) (crtEmbed d S (L₀ :: Ls))) := by rw [hvec]
|
||
_ = c + d := vecFirst_vecAdd_crtEmbed c d S L₀ Ls hc_lt hd_lt
|
||
rcases hSidon ha hb hc hd hfirst with (⟨hac, hbd⟩ | ⟨had, hbc⟩)
|
||
· exact Or.inl ⟨hac, hbd⟩
|
||
· exact Or.inr ⟨had, hbc⟩
|
||
|
||
end CoreFormalism.CRTSidon
|