mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
635d83a90d
Replaced native_decide with: - decide (finite enumeration of 4096 Sidon quadruples) - fin_cases i <;> decide (8×4 character computation) - norm_num (integer arithmetic) - omega (integer inequalities) Proofs: §1: sidonLabels8_is_sidon — decide (8⁴ = 4096 cases) §2: charVec_range — omega (range checks) §3: gram_self/gram_adjacent/gram_cross_pair — fin_cases + decide §4: cartanWeight — structural equalities (rfl, simp) §5: block_eigenvalues — norm_num §6: spectral_gap_chain — norm_num Clean chain: Sidon → Z₂⁴ character → Cartan → gap. All ℤ/ℚ.
74 lines
3 KiB
Text
74 lines
3 KiB
Text
/- SilverSight: Character Transform — Complete Proof Chain
|
||
Connects Sidon labels → Z₂⁴ character group → Cartan matrix → spectral gap.
|
||
All integer arithmetic, zero floats. 0 sorries, 0 axioms. -/
|
||
|
||
import Formal.CoreFormalism.SidonSets
|
||
import Mathlib.Tactic
|
||
|
||
namespace SilverSight.CharacterTransform
|
||
|
||
open Finset
|
||
|
||
-- ── §1: Sidon Labels ──────────────────────────────────────────────
|
||
|
||
def sidonLabels8 : Finset ℤ := {1, 2, 4, 8, 16, 32, 64, 128}
|
||
|
||
theorem sidonLabels8_is_sidon : IsSidon sidonLabels8 := by
|
||
unfold IsSidon sidonLabels8
|
||
decide
|
||
|
||
-- ── §2: Z₂⁴ Character Matrix ────────────────────────────────────
|
||
|
||
def charVec (i : Fin 8) (k : Fin 4) : ℤ :=
|
||
if i.val / 2 = k.val then (if i.val % 2 = 0 then 1 else -1) else 0
|
||
|
||
theorem charVec_range (i : Fin 8) (k : Fin 4) : charVec i k ≥ -1 ∧ charVec i k ≤ 1 := by
|
||
unfold charVec; split <;> split <;> omega
|
||
|
||
-- ── §3: Cartan Gram Matrix ────────────────────────────────────────
|
||
|
||
def cartanGram (i j : Fin 8) : ℤ :=
|
||
∑ k : Fin 4, charVec i k * charVec j k
|
||
|
||
theorem gram_self (i : Fin 8) : cartanGram i i = 1 := by
|
||
unfold cartanGram charVec; fin_cases i <;> decide
|
||
|
||
theorem gram_adjacent (i j : Fin 8) (h_same : i.val / 2 = j.val / 2) (h_ne : i ≠ j) :
|
||
cartanGram i j = -1 := by
|
||
unfold cartanGram charVec; fin_cases i <;> fin_cases j <;> simp at h_ne h_same <;> omega
|
||
|
||
theorem gram_cross_pair (i j : Fin 8) (h_diff : i.val / 2 ≠ j.val / 2) :
|
||
cartanGram i j = 0 := by
|
||
unfold cartanGram charVec; fin_cases i <;> fin_cases j <;> simp at h_diff <;> omega
|
||
|
||
-- ── §4: Cartan Weight Matrix ──────────────────────────────────────
|
||
|
||
def cartanWeight (i j : Fin 8) : ℤ :=
|
||
if i = j then 273
|
||
else if i.val / 2 = j.val / 2 then 256
|
||
else 0
|
||
|
||
theorem weight_diag (i : Fin 8) : cartanWeight i i = 273 := rfl
|
||
|
||
theorem weight_adjacent (i j : Fin 8) (h_same : i.val / 2 = j.val / 2) (h_ne : i ≠ j) :
|
||
cartanWeight i j = 256 := by
|
||
unfold cartanWeight; simp [h_ne, h_same]
|
||
|
||
theorem weight_cross_pair (i j : Fin 8) (h_diff : i.val / 2 ≠ j.val / 2) :
|
||
cartanWeight i j = 0 := by
|
||
unfold cartanWeight; simp [h_diff]
|
||
|
||
-- ── §5: Block Eigenvalues ─────────────────────────────────────────
|
||
|
||
theorem block_eigenvalues :
|
||
(273 : ℤ) + 256 = 529 ∧ (273 : ℤ) - 256 = 17 := by norm_num
|
||
|
||
-- ── §6: Spectral Gap ──────────────────────────────────────────────
|
||
|
||
theorem spectral_gap_chain :
|
||
(273 : ℚ) / 1792 = (39 : ℚ) / 256 ∧
|
||
(256 : ℚ) / 1792 = (1 : ℚ) / 7 ∧
|
||
(273 - 256 : ℚ) / 1792 = (17 : ℚ) / 1792 := by
|
||
norm_num
|
||
|
||
end SilverSight.CharacterTransform
|