SilverSight/docs/research/sidon_preservation_creation.md
allaun 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

7.3 KiB
Raw Permalink Blame History

CRT Torus Embedding: Property Preservation and Creation

Part of Open Direction #3 — characterizing moduli that guarantee F(A) satisfies a target property P.


1. Problem

Given A ⊂ reflection-closed under S, and a target property P (Sidon, B_h, Golomb ruler), which moduli (L₁, …, L_k) guarantee that F(A) satisfies P?

The Sidon example shows F can create P from a non-P set, but this depends on modulus choice. We need the general condition.


2. Key Invariant: The Sum Map

For a pair (a, b) in A, the CRT-lifted sum F(a) + F(b) has residues:

Axis Constraint
1 (identity) (a + b) mod L₁
i ≥ 2 (reflection) (2S a b) mod Lᵢ

Two pairs (a,b) and (c,d) produce equal sums modulo M iff:

a + b ≡ c + d   (mod L₁)
a + b ≡ c + d   (mod Lᵢ)   ∀i ≥ 2

By CRT: a + b ≡ c + d (mod M), where M = ∏ Lᵢ.

Therefore:

F(a) + F(b) ≡ F(c) + F(d)  (mod M)   iff   a + b ≡ c + d  (mod M)

3. Three Regimes

Let M = ∏ Lᵢ.

Regime A — M > max(A): injective, wrapping can break collisions

F is injective. Existing sum collisions break when individual CRT lifts wrap M differently (the wrapping criterion).

A1: M > 2·max(A) — no sum alias. All pairwise sums < M, so new collisions cannot form. Wrapping can still break existing collisions. Sidon creation IS possible here (e.g., [7,3] with A={1,2,5,6}).

A2: max(A) < M ≤ 2·max(A) — sum alias possible. Pairs with different sums may satisfy |T₁T₂| = M, creating new collisions. Wrapping + M-diff both active.

Regime B — M ≤ max(A): F not injective (aliasing)

Not useful.

Wrapping works identically in A1 and A2

(L₁, L₂) M Regime Sidon? Why
(3, 4) 12 A2 Wrapping: 19 vs 7
(7, 3) 21 A1 Wrapping: 28 vs 7
(11, 2) 22 A1 Same wrap: both sums = 29

4. B_h Generalization

For h-fold sums: wrapping works at ANY M > max(A). M-differences require M ≤ h·max(A) to be possible (since max h-fold sum = h·max(A)).

Property No sum alias (M > h·maxA) Sum alias possible
Sidon (h=2) M > 2·max(A): wrapping only, no new collisions max(A) < M ≤ 2·max(A)
B_h (general) M > h·max(A): wrapping only max(A) < M ≤ h·max(A)
Golomb (differences) M > max(A)-min(A): wrapping only boundary case

6. Creation Condition: Complete Characterization

6.1 Breaking Existing Collisions (The Wrapping Criterion)

Given a collision a+b = c+d = T in A, the images satisfy:

F(a)+F(b) = T + r₁·M,    r₁ ∈ {0, 1}
F(c)+F(d) = T + r₂·M,    r₂ ∈ {0, 1}

The collision is broken iff r₁ ≠ r₂. (Proof: each F(x) < M, so two sums of two values are < 2M. The wrap indicator r = 1 when F(a)+F(b) ≥ M.)

Verified: 500/500 random tests, k=2..8.

6.2 Preventing New Collisions (The M-Difference Condition)

A new collision arises when pairs (a,b) and (c,d) with distinct original sums T₁ ≠ T₂ satisfy F(a)+F(b) = F(c)+F(d). This occurs iff:

|T₁  T₂| = M  (or a multiple of M)

Since T₁, T₂ ≤ 2·max(A) and M > max(A), the only possible multiple is M.

Proof. F(a)+F(b) ≡ F(c)+F(d) (mod M) forces a+b ≡ c+d (mod M), i.e., T₁ ≡ T₂ (mod M). Since 0 ≤ T₁, T₂ ≤ 2·max(A) < 2M, we have |T₁T₂| ∈ {0, M}. The case 0 is the existing collision (T₁ = T₂). The case M is the new collision.

Verified: 416 new collisions across 5000 random trials — ALL satisfy |T₁T₂| = M. Zero counterexamples.

6.3 Complete Sidon Creation Theorem

Status: Mathematically argued, formalized in Lean only for the preservation direction.

The Lean theorem (CRTSidon.lean) now formalizes both:

  • sidon_preservedpreservation under componentwise vector addition (stronger property)
  • sidon_preserved_modpreservation under CRT-reconstructed modular sums (matches Python)

The creation direction (non-Sidon → Sidon under conditions (a)+(b)) is still unformalized. Empirical verification (500/500 tests, 416 collisions across 5000 trials) is not a proof.

Theorem. For a finite A ⊂ with reflection closure a ↦ Sa, moduli L₁,…,Lₖ coprime, L₁,L₂ ≥ 2, and M = ∏ Lᵢ > max(A):

F(A) is Sidon  ⟺  (a) and (b) both hold:

(a) For every sum collision a+b = c+d in A:
    (F(a)+F(b) ≥ M) ≠ (F(c)+F(d) ≥ M)    [wrapping criterion]

(b) For no distinct sums T₁, T₂ ∈ {a+b : a,b ∈ A, a ≤ b}:
    |T₁  T₂| = M                         [M-difference condition]

Corollary 1 (No sum alias). If M > 2·max(A), condition (b) is vacuous (no sums differ by exactly M). F(A) may still break existing collisions via wrapping. No new collisions can form.

Corollary 2 (Sum alias possible). If max(A) < M ≤ 2·max(A), both conditions must be checked. F(A) is Sidon iff (a) wrapping breaks all existing collisions AND (b) no M-differences create new ones. Both conditions are decidable in O(|A|⁴) time.

Corollary 3 (Complete classification). M > max(A) → wrapping can break existing collisions; M-differences may or may not apply depending on if M ≤ 2·max(A). M ≤ max(A) → F not injective (aliasing).

6.4 Algorithmic Guidance for Modulus Selection

Choose moduli to guarantee Sidon creation:

  1. Compute all pairwise sums Sₐ = {aᵢ + aⱼ : 0 ≤ i ≤ j < |A|}.
  2. Compute differences Dₐ = {|T₁ T₂| : T₁,T₂ ∈ Sₐ, T₁ ≠ T₂}.
  3. Choose M = ∏ Lᵢ such that:
    • M > max(A) (element-level injectivity)
    • M ∉ Dₐ (no new collisions)
  4. For each existing collision in A, verify the wrapping criterion (a). If any pair wraps the same, pick different moduli or accept the collision persists.
  5. If (a) and (b) both hold, F(A) is guaranteed Sidon.

6.5 Modulus Ordering Principle (Tuning Rule)

The identity axis L₁ and reflection axis L₂ are not interchangeable. Larger L₁ = larger minimum gap = more likely Sidon creation.

Empirical rule: Choose L₁ > L₂. For the complex set A = [0,1,3,8,13]:

(L₁, L₂) M Gap Sidon? Insight
(7, 3) 21 ≥7 L₁=7 large identity axis
(11, 2) 22 ≥11 L₁=11 even larger
(8, 3) 24 ≥8 L₁=8
(13, 2) 26 ≥13 L₁=13, max gap
(3, 7) 21 ≥3 L₁=3 too small
(2, 11) 22 ≥2 L₁=2 minimal gap

All 4 successes have L₁ > L₂. All failures with L₁ < L₂ have insufficient gap for this specific set. (When both L₁ ≈ L₂, other factors like the wrapping criterion and M-difference condition dominate.)

Practical rule:

  1. Choose L₁ as large as possible (up to 2·maxA / L₂)
  2. Choose L₂ as the smallest coprime integer that keeps M in (maxA, 2·maxA]
  3. Typically L₂ = 2 (smallest possible) and L₁ = ⌊2·maxA / L₂⌋, adjusted downward for coprimality

This maximizes the gap L₁, which maximizes the chance of breaking existing sum collisions via the wrapping criterion.

Tradeoff: Larger L₁ also means larger M. If M exceeds 2·maxA, the M-difference condition becomes vacuous (no new collisions), but wrapping can still break existing ones. The optimal is L₁ ≈ 1.9·maxA from sweep data (29% success rate).