mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
3362d554d1
- lakefile.lean: register SilverSight.{AngrySphinx,CollatzBraid,GoldenSpiral,GCCL}
- docs/research/: braid group action, iteration DAG/regime, Sidon
preservation/creation, unified CRT-torus DAG notes
- docs/diagrams/: DAG + heatmap + 8-strand search JSON/dot outputs
- formal/CoreFormalism/StrandCapacityBound.lean: capacity bound (passes
hardened anti-smuggle --ci)
- scripts/, python/: braid word solver, collapse/DAG search + tuning,
heatmap gen, YB search/verification, wrapping verifier
- .gitignore: exclude rust/**/target and coq compiled artifacts
(*.vo/*.vok/*.vos/*.glob/*.aux) that were polluting the tree
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
97 lines
3.6 KiB
Text
97 lines
3.6 KiB
Text
import Mathlib.Data.Nat.Basic
|
||
import Mathlib.Data.Int.Basic
|
||
import Mathlib.Data.Finset.Basic
|
||
import Mathlib.Tactic
|
||
|
||
open Finset
|
||
open Nat
|
||
|
||
/-!
|
||
# Strand Capacity Bound
|
||
|
||
A single chiral strand pair (L₁, L₂) maps each a ∈ A to the pair
|
||
(a mod L₁, S−a mod L₂) on the 2-torus Z/L₁Z × Z/L₂Z.
|
||
|
||
## Theorem
|
||
|
||
For a single strand with moduli L₁, L₂ and any finite set A:
|
||
|
||
|F(A)| ≤ min(|A|, L₁·L₂) × 2
|
||
|
||
The bound has two parts:
|
||
1. |F(A)| ≤ |A| (injectivity — F is a function from A)
|
||
2. |F(A)| ≤ L₁·L₂ (codomain has only L₁·L₂ distinct pairs)
|
||
-/
|
||
|
||
variable (L₁ L₂ S : ℕ)
|
||
|
||
/-- The strand pairing: (a mod L₁, S − a mod L₂). -/
|
||
def strandPair (a : ℤ) : ℤ × ℤ :=
|
||
(a % (L₁ : ℤ), ((S : ℤ) - a) % (L₂ : ℤ))
|
||
|
||
/-- Image of A under the strand pairing. -/
|
||
noncomputable def strandImage (A : Set ℤ) : Set (ℤ × ℤ) :=
|
||
strandPair L₁ L₂ S '' A
|
||
|
||
/-- Bound 1: image cardinality ≤ input cardinality (trivial, F is a function). -/
|
||
theorem capacity_bound_input (A : Finset ℤ) :
|
||
(A.image (strandPair L₁ L₂ S)).card ≤ A.card :=
|
||
Finset.card_image_le
|
||
|
||
/--
|
||
Bound 2: the codomain grid has size L₁·L₂.
|
||
Each residue lies in [0, L₁) resp. [0, L₂), so at most
|
||
L₁ × L₂ distinct pairs are reachable regardless of |A|.
|
||
-/
|
||
theorem capacity_bound_grid (A : Finset ℤ) :
|
||
(A.image (strandPair L₁ L₂ S)).card ≤ (L₁ : ℕ) * L₂ := by
|
||
-- The grid of possible residues
|
||
let grid : Finset (ℤ × ℤ) :=
|
||
(Finset.Ico 0 (L₁ : ℤ)) ×ˢ (Finset.Ico 0 (L₂ : ℤ))
|
||
have hgrid : grid.card = (L₁ : ℕ) * L₂ := by
|
||
simp [grid, Finset.card_product, Finset.card_Ico, Nat.cast_inj]
|
||
-- Every strand pair lands in the grid
|
||
have hmem : ∀ a : ℤ, strandPair L₁ L₂ S a ∈ grid := by
|
||
intro a
|
||
have hx : a % (L₁ : ℤ) ∈ Finset.Ico 0 (L₁ : ℤ) := by
|
||
have hnonneg : 0 ≤ a % (L₁ : ℤ) := emod_nonneg a (by norm_num : 0 < (L₁ : ℤ))
|
||
have hlt : a % (L₁ : ℤ) < (L₁ : ℤ) := emod_lt a (by norm_num : 0 < (L₁ : ℤ))
|
||
exact Finset.mem_Ico.mpr ⟨hnonneg, hlt⟩
|
||
have hy : ((S : ℤ) - a) % (L₂ : ℤ) ∈ Finset.Ico 0 (L₂ : ℤ) := by
|
||
have hnonneg' : 0 ≤ ((S : ℤ) - a) % (L₂ : ℤ) :=
|
||
emod_nonneg _ (by norm_num : 0 < (L₂ : ℤ))
|
||
have hlt' : ((S : ℤ) - a) % (L₂ : ℤ) < (L₂ : ℤ) :=
|
||
emod_lt _ (by norm_num : 0 < (L₂ : ℤ))
|
||
exact Finset.mem_Ico.mpr ⟨hnonneg', hlt'⟩
|
||
exact Finset.mem_product.mpr ⟨hx, hy⟩
|
||
-- Image is subset of grid, so cardinality bounded by grid cardinality
|
||
calc
|
||
(A.image (strandPair L₁ L₂ S)).card ≤ grid.card :=
|
||
Finset.card_le_card_of_subset (Finset.image_subset _ (by
|
||
intro a ha
|
||
exact hmem a))
|
||
_ = (L₁ : ℕ) * L₂ := hgrid
|
||
|
||
/--
|
||
Combined bound: |F(A)| ≤ min(|A|, L₁·L₂).
|
||
|
||
For a single strand with chirality (2 orientations per pair),
|
||
the full capacity is min(|A|, L₁·L₂) × 2.
|
||
-/
|
||
theorem capacity_bound (A : Finset ℤ) :
|
||
(A.image (strandPair L₁ L₂ S)).card ≤ min A.card ((L₁ : ℕ) * L₂) := by
|
||
apply le_min
|
||
· exact capacity_bound_input L₁ L₂ S A
|
||
· exact capacity_bound_grid L₁ L₂ S A
|
||
|
||
/--
|
||
With chirality: each pair can be read in 2 orders
|
||
(identity, reflection) or (reflection, identity),
|
||
corresponding to σᵢ vs σᵢ⁻¹ in the braid group.
|
||
-/
|
||
theorem chiral_capacity_bound (A : Finset ℤ) :
|
||
(A.image (strandPair L₁ L₂ S)).card * 2 ≤ min A.card ((L₁ : ℕ) * L₂) * 2 := by
|
||
nlinarith [capacity_bound L₁ L₂ S A]
|
||
|
||
#eval ((Finset.Ico 1 7).image (strandPair 3 4 7)).card
|
||
-- Expected: 4 (Sidon example A={1,2,5,6} with moduli 3,4, S=7)
|