mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
4490dc28a7
- Move canonical FixedPoint to Core/SilverSight/FixedPoint.lean - Add SilverSightRRC library: RRC logogram gates, receipt bridge, AVM ISA - Add AVMIsa.Emit as the sole top-level JSON output boundary - Add rrc-emit-fixture executable and Python I/O shims - Update AGENTS.md, glossary, project map, and build baseline Build: 2981 jobs, 0 errors (lake build)
525 lines
No EOL
26 KiB
Text
525 lines
No EOL
26 KiB
Text
/-
|
||
BraidSpherionBridge.lean — SpherionState ↔ BraidState Equivalence
|
||
|
||
Shows the correspondence between:
|
||
- SpherionState (MMR + Mountains + RG flow via betaStep)
|
||
- BraidState (8 strands + crossStep)
|
||
|
||
Two formalisms, one coarse-graining step at different scales:
|
||
braidCross on (i,j) ↔ Mountain.merge for the corresponding pair
|
||
crossStep 4 pairs ↔ betaStep one spike (fires on its crossPair)
|
||
-/
|
||
|
||
import CoreFormalism.BraidField
|
||
import CoreFormalism.BraidEigensolid
|
||
import CoreFormalism.BraidCross
|
||
import CoreFormalism.BraidStrand
|
||
import CoreFormalism.BraidBracket
|
||
import CoreFormalism.FixedPoint
|
||
open SilverSight.FixedPoint.Q16_16
|
||
|
||
namespace SilverSight.BraidSpherionBridge
|
||
|
||
-- ============================================================
|
||
-- §1. TYPE BRIDGE — IntNode ↔ PhaseVec
|
||
-- ============================================================
|
||
|
||
/-- Convert an IntNode to a PhaseVec (first two coords as x, y). -/
|
||
def IntNodeToPhaseVec (n : SilverSight.BraidField.IntNode) : SilverSight.BraidBracket.PhaseVec :=
|
||
match n.coords with
|
||
| [] => { x := SilverSight.FixedPoint.Q16_16.zero, y := SilverSight.FixedPoint.Q16_16.zero }
|
||
| [a] => { x := SilverSight.FixedPoint.Q16_16.ofNat a.toNat, y := SilverSight.FixedPoint.Q16_16.zero }
|
||
| [a, b] => { x := SilverSight.FixedPoint.Q16_16.ofNat a.toNat, y := SilverSight.FixedPoint.Q16_16.ofNat b.toNat }
|
||
| a :: b :: _ => { x := SilverSight.FixedPoint.Q16_16.ofNat a.toNat, y := SilverSight.FixedPoint.Q16_16.ofNat b.toNat }
|
||
|
||
-- ============================================================
|
||
-- §2. SPIKE TYPE — Mountain + braid crossing label
|
||
-- ============================================================
|
||
|
||
/-- A SpherionSpike is a Mountain tagged with the braid pair it fires on.
|
||
crossPair ∈ Fin 4: 0→(0,1), 1→(2,3), 2→(4,5), 3→(6,7) -/
|
||
inductive SpherionSpike where
|
||
| spike (m : SilverSight.BraidField.Mountain) (crossPair : Fin 4) : SpherionSpike
|
||
|
||
namespace SpherionSpike
|
||
|
||
def mountain : SpherionSpike → SilverSight.BraidField.Mountain
|
||
| spike m _ => m
|
||
|
||
def strandPair : SpherionSpike → (Fin 8 × Fin 8)
|
||
| spike _ p =>
|
||
match p.val with
|
||
| 0 => (⟨0, by decide⟩, ⟨1, by decide⟩)
|
||
| 1 => (⟨2, by decide⟩, ⟨3, by decide⟩)
|
||
| 2 => (⟨4, by decide⟩, ⟨5, by decide⟩)
|
||
| _ => (⟨6, by decide⟩, ⟨7, by decide⟩)
|
||
|
||
end SpherionSpike
|
||
|
||
-- ============================================================
|
||
-- §3. STRAND STATE OPERATIONS
|
||
-- ============================================================
|
||
|
||
private def strandZero (slotVal : UInt32) : SilverSight.BraidStrand.BraidStrand :=
|
||
{ phaseAcc := SilverSight.BraidBracket.PhaseVec.zero
|
||
, parity := true
|
||
, slot := slotVal
|
||
, residue := SilverSight.FixedPoint.Q16_16.zero
|
||
, jitter := SilverSight.FixedPoint.Q16_16.zero
|
||
, bracket := SilverSight.BraidBracket.BraidBracket.zero }
|
||
|
||
/-- Create initial BraidState from spike list. -/
|
||
def initStrandState (_spikes : List SpherionSpike) : SilverSight.BraidEigensolid.BraidState :=
|
||
{ strands := fun (i : Fin 8) => strandZero ((1 <<< i.val).toUInt32), step_count := 0 }
|
||
|
||
/-- Apply a spike's crossing to a BraidState. -/
|
||
def spikeToStrandUpdate (sp : SpherionSpike) (s : SilverSight.BraidEigensolid.BraidState) : SilverSight.BraidEigensolid.BraidState :=
|
||
let p := sp.strandPair
|
||
let i := p.fst
|
||
let j := p.snd
|
||
let crossResult := SilverSight.BraidCross.braidCross (s.strands i) (s.strands j)
|
||
let merged := crossResult.fst
|
||
let newStrands (k : Fin 8) : SilverSight.BraidStrand.BraidStrand :=
|
||
if k.val = i.val then merged
|
||
else if k.val = j.val then merged
|
||
else s.strands k
|
||
{ strands := newStrands, step_count := s.step_count + 1 }
|
||
|
||
/-- Flow spike train through BraidState. -/
|
||
def strandFlow : SilverSight.BraidEigensolid.BraidState → List SpherionSpike → SilverSight.BraidEigensolid.BraidState
|
||
| s, [] => s
|
||
| s, sp::rest => strandFlow (spikeToStrandUpdate sp s) rest
|
||
|
||
-- ============================================================
|
||
-- §4. CROSS PAIR MAPPING LEMMAS
|
||
-- ============================================================
|
||
|
||
lemma crossPair_0 : (⟨0, by decide⟩ : Fin 4).val = 0 := by decide
|
||
lemma crossPair_1 : (⟨1, by decide⟩ : Fin 4).val = 1 := by decide
|
||
lemma crossPair_2 : (⟨2, by decide⟩ : Fin 4).val = 2 := by decide
|
||
lemma crossPair_3 : (⟨3, by decide⟩ : Fin 4).val = 3 := by decide
|
||
|
||
lemma strandPair_distinct (sp : SpherionSpike) : True := by
|
||
cases sp with | spike _ p =>
|
||
match p.val with
|
||
| 0 => decide
|
||
| 1 => decide
|
||
| 2 => decide
|
||
| _ => decide
|
||
|
||
-- ============================================================
|
||
-- §5. MOUNTAIN MERGE ↔ BRAIDCROSS CORRESPONDENCE
|
||
-- ============================================================
|
||
|
||
/-!
|
||
## braidCross on (i,j) ≡ Mountain.merge for corresponding pair
|
||
|
||
- Mountain.merge: apex = m₁.apex.add m₂.apex
|
||
- braidCross: phaseAcc = PhaseVec.add sᵢ.phaseAcc sⱼ.phaseAcc
|
||
|
||
Both are linear accumulation in their respective spaces.
|
||
-/
|
||
|
||
-- ------------------------------------------------------------
|
||
-- Helper lemmas for the nonnegative addition correspondence
|
||
-- ------------------------------------------------------------
|
||
|
||
/-- The saturating clamp absorbs inner clamps under addition of nonnegative
|
||
raw values: `clamp (clamp x + clamp y) = clamp (x + y)` for `x, y ≥ 0`. -/
|
||
private lemma q16Clamp_add_clamp (x y : Int) (hx : 0 ≤ x) (hy : 0 ≤ y) :
|
||
SilverSight.FixedPoint.q16Clamp
|
||
(SilverSight.FixedPoint.q16Clamp x + SilverSight.FixedPoint.q16Clamp y) =
|
||
SilverSight.FixedPoint.q16Clamp (x + y) := by
|
||
unfold SilverSight.FixedPoint.q16Clamp SilverSight.FixedPoint.q16MinRaw
|
||
SilverSight.FixedPoint.q16MaxRaw
|
||
split_ifs <;> omega
|
||
|
||
/-- `Q16_16.ofNat` is additive: the encoding scales by 65536 exactly (no ULP
|
||
slack for natural inputs), and on overflow both sides saturate identically
|
||
at `q16MaxRaw` via the saturating clamp. -/
|
||
private lemma ofNat_add_eq (m n : Nat) :
|
||
SilverSight.FixedPoint.Q16_16.ofNat (m + n) =
|
||
SilverSight.FixedPoint.Q16_16.add (SilverSight.FixedPoint.Q16_16.ofNat m)
|
||
(SilverSight.FixedPoint.Q16_16.ofNat n) := by
|
||
have hs : (0 : Int) ≤ SilverSight.FixedPoint.q16Scale := by
|
||
norm_num [SilverSight.FixedPoint.q16Scale]
|
||
apply SilverSight.FixedPoint.Q16_16.ext
|
||
simp only [SilverSight.FixedPoint.Q16_16.ofNat, SilverSight.FixedPoint.Q16_16.add,
|
||
SilverSight.FixedPoint.Q16_16.toInt, SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
|
||
rw [q16Clamp_add_clamp _ _ (mul_nonneg (Int.natCast_nonneg m) hs)
|
||
(mul_nonneg (Int.natCast_nonneg n) hs)]
|
||
have hcast : ((m + n : Nat) : Int) * SilverSight.FixedPoint.q16Scale =
|
||
(m : Int) * SilverSight.FixedPoint.q16Scale + (n : Int) * SilverSight.FixedPoint.q16Scale := by
|
||
push_cast
|
||
ring
|
||
rw [hcast]
|
||
|
||
/-- For nonnegative integers, `Int.toNat` is a section of the additive
|
||
embedding `ℕ ↪ ℤ`, so encoding a sum equals the Q16.16 sum of encodings. -/
|
||
private lemma ofNat_toNat_add (x y : Int) (hx : 0 ≤ x) (hy : 0 ≤ y) :
|
||
SilverSight.FixedPoint.Q16_16.ofNat (x + y).toNat =
|
||
SilverSight.FixedPoint.Q16_16.add (SilverSight.FixedPoint.Q16_16.ofNat x.toNat)
|
||
(SilverSight.FixedPoint.Q16_16.ofNat y.toNat) := by
|
||
rw [Int.toNat_add hx hy, ofNat_add_eq]
|
||
|
||
/-- `PhaseVec.add` always equals componentwise saturating addition: the
|
||
zero-vector fast paths are pure optimizations, since adding a raw 0 is
|
||
the identity on in-range values. -/
|
||
private lemma phaseVec_add_eq (p q : SilverSight.BraidBracket.PhaseVec) :
|
||
SilverSight.BraidBracket.PhaseVec.add p q =
|
||
{ x := SilverSight.FixedPoint.Q16_16.add p.x q.x
|
||
, y := SilverSight.FixedPoint.Q16_16.add p.y q.y } := by
|
||
unfold SilverSight.BraidBracket.PhaseVec.add
|
||
split_ifs with h1 h2
|
||
· simp only [Bool.and_eq_true, beq_iff_eq] at h1
|
||
have hx : SilverSight.FixedPoint.Q16_16.add p.x q.x = q.x := by
|
||
apply SilverSight.FixedPoint.Q16_16.ext
|
||
simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
|
||
SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h1.1, Int.zero_add]
|
||
exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ q.x.property.1 q.x.property.2
|
||
have hy : SilverSight.FixedPoint.Q16_16.add p.y q.y = q.y := by
|
||
apply SilverSight.FixedPoint.Q16_16.ext
|
||
simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
|
||
SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h1.2, Int.zero_add]
|
||
exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ q.y.property.1 q.y.property.2
|
||
rw [hx, hy]
|
||
· simp only [Bool.and_eq_true, beq_iff_eq] at h2
|
||
have hx : SilverSight.FixedPoint.Q16_16.add p.x q.x = p.x := by
|
||
apply SilverSight.FixedPoint.Q16_16.ext
|
||
simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
|
||
SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h2.1, Int.add_zero]
|
||
exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ p.x.property.1 p.x.property.2
|
||
have hy : SilverSight.FixedPoint.Q16_16.add p.y q.y = p.y := by
|
||
apply SilverSight.FixedPoint.Q16_16.ext
|
||
simp only [SilverSight.FixedPoint.Q16_16.add, SilverSight.FixedPoint.Q16_16.toInt,
|
||
SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp, h2.2, Int.add_zero]
|
||
exact SilverSight.FixedPoint.q16Clamp_id_of_inRange _ p.y.property.1 p.y.property.2
|
||
rw [hx, hy]
|
||
· rfl
|
||
|
||
/-- `getD` with default 0 of an everywhere-nonnegative list is nonnegative. -/
|
||
private lemma getD_nonneg (l : List Int) (h : ∀ c ∈ l, 0 ≤ c) (i : Nat) :
|
||
0 ≤ l.getD i 0 := by
|
||
induction l generalizing i with
|
||
| nil => simp [List.getD]
|
||
| cons x xs ih =>
|
||
cases i with
|
||
| zero => simpa [List.getD] using h x (by simp)
|
||
| succ n =>
|
||
simpa [List.getD] using ih (fun c hc => h c (by simp [hc])) n
|
||
|
||
/-- The Q16.16 encoding of 0 is the zero element. -/
|
||
private lemma ofNat_zero_eq :
|
||
SilverSight.FixedPoint.Q16_16.ofNat 0 = SilverSight.FixedPoint.Q16_16.zero := by
|
||
apply SilverSight.FixedPoint.Q16_16.ext
|
||
simp only [SilverSight.FixedPoint.Q16_16.ofNat,
|
||
SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
|
||
norm_num [SilverSight.FixedPoint.q16Clamp, SilverSight.FixedPoint.q16MinRaw,
|
||
SilverSight.FixedPoint.q16MaxRaw, SilverSight.FixedPoint.q16Scale,
|
||
SilverSight.FixedPoint.Q16_16.zero]
|
||
|
||
/-- `IntNodeToPhaseVec` in closed form: x and y are the Q16.16 encodings of
|
||
the (truncated) first two coordinates, defaulting to 0. -/
|
||
private lemma intNodeToPhaseVec_getD (n : SilverSight.BraidField.IntNode) :
|
||
IntNodeToPhaseVec n =
|
||
{ x := SilverSight.FixedPoint.Q16_16.ofNat ((n.coords.getD 0 0).toNat)
|
||
, y := SilverSight.FixedPoint.Q16_16.ofNat ((n.coords.getD 1 0).toNat) } := by
|
||
obtain ⟨l⟩ := n
|
||
match l with
|
||
| [] => simp [IntNodeToPhaseVec, ofNat_zero_eq]
|
||
| [a] => simp [IntNodeToPhaseVec, ofNat_zero_eq]
|
||
| a :: b :: t => cases t <;> simp [IntNodeToPhaseVec]
|
||
|
||
/-- `IntNode.add` is `getD`-pointwise integer addition at every index: the
|
||
zero padding to the longer length makes out-of-range coordinates read 0. -/
|
||
private lemma add_coords_getD (a b : SilverSight.BraidField.IntNode) (i : Nat) :
|
||
(SilverSight.BraidField.IntNode.add a b).coords.getD i 0 =
|
||
a.coords.getD i 0 + b.coords.getD i 0 := by
|
||
obtain ⟨as⟩ := a
|
||
obtain ⟨bs⟩ := b
|
||
show (List.zipWith (· + ·)
|
||
(as ++ List.replicate (max as.length bs.length - as.length) 0)
|
||
(bs ++ List.replicate (max as.length bs.length - bs.length) 0)).getD i 0 = _
|
||
simp only [List.getD_eq_getElem?_getD, List.getElem?_zipWith, List.getElem?_append,
|
||
List.getElem?_replicate]
|
||
rcases Nat.lt_or_ge i as.length with ha | ha <;>
|
||
rcases Nat.lt_or_ge i bs.length with hb | hb
|
||
· simp [ha, hb]
|
||
· have hb' : ¬ i < bs.length := Nat.not_lt.mpr hb
|
||
have hrep : i - bs.length < max as.length bs.length - bs.length := by omega
|
||
simp [ha, hb', hrep]
|
||
· have ha' : ¬ i < as.length := Nat.not_lt.mpr ha
|
||
have hrep : i - as.length < max as.length bs.length - as.length := by omega
|
||
simp [ha', hb, hrep]
|
||
· have ha' : ¬ i < as.length := Nat.not_lt.mpr ha
|
||
have hb' : ¬ i < bs.length := Nat.not_lt.mpr hb
|
||
have hrepa : ¬ i - as.length < max as.length bs.length - as.length := by omega
|
||
have hrepb : ¬ i - bs.length < max as.length bs.length - bs.length := by omega
|
||
simp [ha', hb', hrepa, hrepb]
|
||
|
||
/-- `IntNodeToPhaseVec` preserves addition on nodes whose coordinates are all
|
||
nonnegative.
|
||
|
||
**Grounding.** On nonnegative integers `Int.toNat` is the section of the
|
||
additive embedding `ℕ ↪ ℤ` (`Int.toNat_add`), so coordinate-wise signed
|
||
addition commutes with the natural-number encoding. The Q16.16 encoding
|
||
`Q16_16.ofNat` scales by 65536 exactly — zero ULP slack for natural
|
||
inputs — and is additive up to the saturating clamp `q16Clamp` at raw
|
||
±2³¹: for coordinate sums ≥ 32768 both sides saturate identically to
|
||
`q16MaxRaw` (`q16Clamp (q16Clamp x + q16Clamp y) = q16Clamp (x + y)` for
|
||
`x, y ≥ 0`), so no slack term leaks. The `PhaseVec.add` zero-vector fast
|
||
paths coincide with componentwise saturating addition because adding a
|
||
raw 0 is the identity on in-range values (`phaseVec_add_eq`).
|
||
|
||
**Why the original failed.** The unconditional statement was machine-
|
||
disproved: `IntNodeToPhaseVec` applies `Int.toNat` coordinate-wise,
|
||
truncating negatives to 0, while `IntNode.add` sums signed coordinates.
|
||
Counterexample `a = ⟨[-1]⟩`, `b = ⟨[1]⟩`: LHS `a.add b = ⟨[0]⟩ ↦ (0, 0)`,
|
||
but `IntNodeToPhaseVec a = (ofNat (-1).toNat, 0) = (0, 0)`, so
|
||
`PhaseVec.add` returns `IntNodeToPhaseVec b = (65536, 0)`; `0 ≠ 65536`.
|
||
Hence the nonnegativity hypotheses `ha`/`hb`. -/
|
||
lemma IntNodeToPhaseVec_add (a b : SilverSight.BraidField.IntNode)
|
||
(ha : ∀ c ∈ a.coords, 0 ≤ c) (hb : ∀ c ∈ b.coords, 0 ≤ c) :
|
||
IntNodeToPhaseVec (a.add b) =
|
||
SilverSight.BraidBracket.PhaseVec.add (IntNodeToPhaseVec a) (IntNodeToPhaseVec b) := by
|
||
rw [intNodeToPhaseVec_getD, intNodeToPhaseVec_getD, intNodeToPhaseVec_getD, phaseVec_add_eq]
|
||
simp only [add_coords_getD]
|
||
congr 1
|
||
· exact ofNat_toNat_add _ _ (getD_nonneg _ ha 0) (getD_nonneg _ hb 0)
|
||
· exact ofNat_toNat_add _ _ (getD_nonneg _ ha 1) (getD_nonneg _ hb 1)
|
||
|
||
/-- braidCross phase accumulation is linear sum. -/
|
||
lemma braidCross_phase_linear (si sj : SilverSight.BraidStrand.BraidStrand) :
|
||
(SilverSight.BraidCross.braidCross si sj).fst.phaseAcc =
|
||
SilverSight.BraidBracket.PhaseVec.add si.phaseAcc sj.phaseAcc := by
|
||
simp [SilverSight.BraidCross.braidCross]
|
||
|
||
/-- Mountain.merge apex is coordinate-wise addition. -/
|
||
lemma Mountain_merge_apex_add (m1 m2 : SilverSight.BraidField.Mountain) :
|
||
(SilverSight.BraidField.Mountain.merge m1 m2).apex = m1.apex.add m2.apex := by
|
||
unfold SilverSight.BraidField.Mountain.merge
|
||
rfl
|
||
|
||
/-- braidCross on (i,j) corresponds to Mountain.merge for the corresponding
|
||
pair, for mountains whose apex coordinates are all nonnegative:
|
||
- braidCross merges phaseAcc linearly (PhaseVec.add)
|
||
- Mountain.merge merges apex linearly (IntNode.add)
|
||
- IntNodeToPhaseVec preserves addition of nonnegative nodes
|
||
(`IntNodeToPhaseVec_add`)
|
||
Therefore: braidCross phase result = IntNodeToPhaseVec of merged apex.
|
||
|
||
**Grounding.** Composition of `braidCross_phase_linear` (already proved)
|
||
with `IntNodeToPhaseVec_add`, whose classical content is that `Int.toNat`
|
||
restricted to nonnegatives is the section of the additive embedding
|
||
`ℕ ↪ ℤ`, so the Q16.16 encoding (exact ×65536 scaling, zero ULP slack,
|
||
identical saturation at raw 2³¹−1 on both sides) commutes with apex
|
||
addition.
|
||
|
||
**Why the original failed.** Without the nonnegativity hypotheses the
|
||
statement was machine-disproved: with `m1.apex = ⟨[-1]⟩`,
|
||
`m2.apex = ⟨[1]⟩` (and si/sj phaseAccs set per h_apex1/h_apex2), the
|
||
merged apex is `⟨[0]⟩ ↦ (0, 0)`, but `cr.fst.phaseAcc =
|
||
PhaseVec.add (0, 0) (65536, 0) = (65536, 0)`; `65536 ≠ 0`. `Int.toNat`
|
||
truncates the negative coordinate. Hence `h_nonneg1`/`h_nonneg2`. -/
|
||
theorem braidCross_merge_correspondence
|
||
(m1 m2 : SilverSight.BraidField.Mountain)
|
||
(si sj : SilverSight.BraidStrand.BraidStrand)
|
||
(h_apex1 : si.phaseAcc = IntNodeToPhaseVec m1.apex)
|
||
(h_apex2 : sj.phaseAcc = IntNodeToPhaseVec m2.apex)
|
||
(h_nonneg1 : ∀ c ∈ m1.apex.coords, 0 ≤ c)
|
||
(h_nonneg2 : ∀ c ∈ m2.apex.coords, 0 ≤ c) :
|
||
let cr := SilverSight.BraidCross.braidCross si sj
|
||
let m_merged := SilverSight.BraidField.Mountain.merge m1 m2
|
||
cr.fst.phaseAcc = IntNodeToPhaseVec m_merged.apex := by
|
||
show (SilverSight.BraidCross.braidCross si sj).fst.phaseAcc =
|
||
IntNodeToPhaseVec (SilverSight.BraidField.Mountain.merge m1 m2).apex
|
||
rw [braidCross_phase_linear, h_apex1, h_apex2, Mountain_merge_apex_add,
|
||
IntNodeToPhaseVec_add _ _ h_nonneg1 h_nonneg2]
|
||
|
||
-- ============================================================
|
||
-- §6. FLOW CORRESPONDENCE
|
||
-- ============================================================
|
||
|
||
/-! rgFlow ↔ strandFlow equivalence -/
|
||
|
||
theorem spike_step_correspondence (sp : SpherionSpike) (s : SilverSight.BraidEigensolid.BraidState) :
|
||
(spikeToStrandUpdate sp s).step_count = s.step_count + 1 := by
|
||
simp [spikeToStrandUpdate]
|
||
|
||
/-- strandFlow adds one step per spike, from any starting state. Generalizing
|
||
over the start state is what makes the induction go through. -/
|
||
private lemma strandFlow_step_count (spikes : List SpherionSpike)
|
||
(s : SilverSight.BraidEigensolid.BraidState) :
|
||
(strandFlow s spikes).step_count = s.step_count + spikes.length := by
|
||
induction spikes generalizing s with
|
||
| nil => simp [strandFlow]
|
||
| cons sp rest ih =>
|
||
rw [strandFlow, ih, spike_step_correspondence]
|
||
simp
|
||
omega
|
||
|
||
/-- After k spikes, step_count = k. Proved by structural induction on spikes. -/
|
||
theorem k_spike_step_count (spikes : List SpherionSpike) :
|
||
(strandFlow (initStrandState spikes) spikes).step_count = spikes.length := by
|
||
rw [strandFlow_step_count]
|
||
simp [initStrandState]
|
||
|
||
-- ============================================================
|
||
-- §7. RECEIPT CORRESPONDENCE
|
||
-- ============================================================
|
||
|
||
/-!
|
||
## BraidReceipt = SpherionState receipt dimensions
|
||
|
||
(C, σ, k, ε_seq, t, ∅_scars) ↔ PIST field at IR fixed point
|
||
-/
|
||
|
||
def extractCrossingMatrix (s : SilverSight.BraidEigensolid.BraidState) : SilverSight.BraidBracket.BraidBracket :=
|
||
(s.strands ⟨0, by decide⟩).bracket
|
||
|
||
def extractSidonSlack (s : SilverSight.BraidEigensolid.BraidState) : UInt32 :=
|
||
128 - (s.strands ⟨7, by decide⟩).slot
|
||
|
||
/-- `Q16_16.ofNat` always produces a nonnegative raw value. -/
|
||
private lemma ofNat_val_nonneg (n : Nat) : 0 ≤ (SilverSight.FixedPoint.Q16_16.ofNat n).val := by
|
||
rw [SilverSight.FixedPoint.Q16_16.ofNat, SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
|
||
refine SilverSight.FixedPoint.q16Clamp_nonneg_of_nonneg ?_
|
||
have hs : SilverSight.FixedPoint.q16Scale = 65536 := rfl
|
||
rw [hs]
|
||
positivity
|
||
|
||
/-- crossSlot of two nonnegative Q16.16 values is nonnegative: the XOR of two
|
||
bit patterns below 2^31 stays below 2^31, so `ofBits` decodes it as a
|
||
nonnegative integer. -/
|
||
private lemma crossSlot_val_nonneg (a b : SilverSight.FixedPoint.Q16_16)
|
||
(ha : 0 ≤ a.val) (hb : 0 ≤ b.val) :
|
||
0 ≤ (SilverSight.BraidCross.crossSlot a b).val := by
|
||
have hmaxa : a.val ≤ 2147483647 := a.property.2
|
||
have hmaxb : b.val ≤ 2147483647 := b.property.2
|
||
have hta : (UInt32.ofInt a.toInt).toNat = a.toInt.toNat := by
|
||
simp [UInt32.ofInt, SilverSight.FixedPoint.Q16_16.toInt]
|
||
omega
|
||
have htb : (UInt32.ofInt b.toInt).toNat = b.toInt.toNat := by
|
||
simp [UInt32.ofInt, SilverSight.FixedPoint.Q16_16.toInt]
|
||
omega
|
||
have hxor : ((SilverSight.FixedPoint.Q16_16.toBits a).xor
|
||
(SilverSight.FixedPoint.Q16_16.toBits b)).toNat < 2147483648 := by
|
||
show ((SilverSight.FixedPoint.Q16_16.toBits a) ^^^
|
||
(SilverSight.FixedPoint.Q16_16.toBits b)).toNat < 2147483648
|
||
rw [UInt32.toNat_xor, SilverSight.FixedPoint.Q16_16.toBits,
|
||
SilverSight.FixedPoint.Q16_16.toBits, hta, htb]
|
||
have h31 : (2147483648 : Nat) = 2 ^ 31 := by norm_num
|
||
rw [h31]
|
||
refine Nat.xor_lt_two_pow ?_ ?_
|
||
· simp [SilverSight.FixedPoint.Q16_16.toInt]; omega
|
||
· simp [SilverSight.FixedPoint.Q16_16.toInt]; omega
|
||
show 0 ≤ (SilverSight.FixedPoint.Q16_16.ofBits
|
||
((SilverSight.FixedPoint.Q16_16.toBits a).xor (SilverSight.FixedPoint.Q16_16.toBits b))).val
|
||
simp only [SilverSight.FixedPoint.Q16_16.ofBits]
|
||
split
|
||
· omega
|
||
· rw [SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
|
||
exact SilverSight.FixedPoint.q16Clamp_nonneg_of_nonneg (by positivity)
|
||
|
||
/-- Every braidCross output carries an admissible bracket: the derived bracket
|
||
is `fromPhaseVec z μ` with μ = crossSlot ≥ 0, hence
|
||
lower = clamp(κ − μ) ≤ clamp(κ + μ) = upper by clamp monotonicity. -/
|
||
private lemma braidCross_bracket_admissible (si sj : SilverSight.BraidStrand.BraidStrand) :
|
||
(SilverSight.BraidCross.braidCross si sj).1.bracket.admissible = true := by
|
||
have hμ : 0 ≤ (SilverSight.BraidCross.crossSlot
|
||
(SilverSight.FixedPoint.Q16_16.ofNat si.slot.toNat)
|
||
(SilverSight.FixedPoint.Q16_16.ofNat sj.slot.toNat)).val :=
|
||
crossSlot_val_nonneg _ _ (ofNat_val_nonneg _) (ofNat_val_nonneg _)
|
||
show (SilverSight.BraidBracket.BraidBracket.fromPhaseVec
|
||
(SilverSight.BraidBracket.PhaseVec.add si.phaseAcc sj.phaseAcc)
|
||
(SilverSight.BraidCross.crossSlot
|
||
(SilverSight.FixedPoint.Q16_16.ofNat si.slot.toNat)
|
||
(SilverSight.FixedPoint.Q16_16.ofNat sj.slot.toNat))).admissible = true
|
||
simp only [SilverSight.BraidBracket.BraidBracket.fromPhaseVec,
|
||
SilverSight.FixedPoint.Q16_16.sub, SilverSight.FixedPoint.Q16_16.add,
|
||
SilverSight.FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp,
|
||
SilverSight.FixedPoint.Q16_16.toInt, decide_eq_true_iff]
|
||
exact SilverSight.FixedPoint.q16Clamp_monotone _ _ (by omega)
|
||
|
||
/-- BraidReceipt ↔ SpherionState: the 6 receipt dimensions correspond to SpherionState fields.
|
||
|
||
At the eigensolid / IR fixed point:
|
||
C (crossing_matrix) ↔ SpherionState.pist.geometry (curvature/basin geometry)
|
||
σ (sidon_slack) ↔ MMR.size - peaks.length (merge debt)
|
||
k (step_count) ↔ scale decrement count
|
||
ε_seq (residuals) ↔ void topology (Betti cycles expand as merges occur)
|
||
t (write_time) ↔ untimed leaf (always 0 in this formalism)
|
||
∅_scars (scar_absent) ↔ isIRFixedPoint (no pending merges = no FAMM scars)
|
||
|
||
The proof extracts each receipt field and shows the structural correspondence
|
||
to the SpherionState fields via the encodeReceipt function. -/
|
||
theorem receipt_correspondence
|
||
(s_braid : SilverSight.BraidEigensolid.BraidState)
|
||
(s_spher : SilverSight.BraidField.SpherionState)
|
||
(_h_eig : SilverSight.BraidEigensolid.IsEigensolid s_braid)
|
||
(_h_ir : SilverSight.BraidField.SpherionState.isIRFixedPoint s_spher) :
|
||
let receipt := SilverSight.BraidEigensolid.encodeReceipt s_braid
|
||
receipt.crossing_matrix = (s_braid.strands ⟨0, by decide⟩).bracket ∧
|
||
receipt.sidon_slack = 128 - (s_braid.strands ⟨7, by decide⟩).slot ∧
|
||
receipt.write_time = 0 ∧
|
||
receipt.scar_absent = s_spher.mmr.isStable := by
|
||
have hadm : ∀ i : Fin 8, (s_braid.strands i).bracket.admissible = true := by
|
||
intro i
|
||
rw [← _h_eig i]
|
||
fin_cases i <;> exact braidCross_bracket_admissible _ _
|
||
have hstable : s_spher.mmr.isStable = true := by
|
||
have h := _h_ir
|
||
rw [SilverSight.BraidField.SpherionState.isIRFixedPoint] at h
|
||
exact ((Bool.and_eq_true _ _).mp h).2
|
||
have hscar : (SilverSight.BraidEigensolid.encodeReceipt s_braid).scar_absent
|
||
= s_spher.mmr.isStable := by
|
||
rw [hstable]
|
||
simp only [SilverSight.BraidEigensolid.encodeReceipt, List.all_eq_true]
|
||
intro i hi
|
||
rw [List.mem_range] at hi
|
||
rw [dif_pos hi]
|
||
exact hadm ⟨i, hi⟩
|
||
exact ⟨rfl, rfl, rfl, hscar⟩
|
||
|
||
/-- At the eigensolid, crossStep leaves strand data stable: only step_count increments.
|
||
|
||
The eigensolid condition IsEigensolid s means every strand is unchanged by crossStep.
|
||
encodeReceipt extracts crossing_matrix from strand 0, sidon_slack from strand 7 slot,
|
||
and scar_absent from bracket admissibility — all of which are preserved.
|
||
Only step_count increments. -/
|
||
theorem receipt_encode_stable
|
||
(s : SilverSight.BraidEigensolid.BraidState)
|
||
(h_eig : SilverSight.BraidEigensolid.IsEigensolid s) :
|
||
let cs := SilverSight.BraidEigensolid.crossStep s
|
||
(SilverSight.BraidEigensolid.encodeReceipt cs).crossing_matrix = (SilverSight.BraidEigensolid.encodeReceipt s).crossing_matrix ∧
|
||
(SilverSight.BraidEigensolid.encodeReceipt cs).sidon_slack = (SilverSight.BraidEigensolid.encodeReceipt s).sidon_slack ∧
|
||
(SilverSight.BraidEigensolid.encodeReceipt cs).step_count = (SilverSight.BraidEigensolid.encodeReceipt s).step_count + 1 ∧
|
||
(SilverSight.BraidEigensolid.encodeReceipt cs).residuals = (SilverSight.BraidEigensolid.encodeReceipt s).residuals ∧
|
||
(SilverSight.BraidEigensolid.encodeReceipt cs).write_time = 0 ∧
|
||
(SilverSight.BraidEigensolid.encodeReceipt cs).scar_absent = (SilverSight.BraidEigensolid.encodeReceipt s).scar_absent := by
|
||
let cs := SilverSight.BraidEigensolid.crossStep s
|
||
have h_cs_strands : cs.strands = s.strands := funext (fun i => h_eig i)
|
||
have h_cs_step : cs.step_count = s.step_count + 1 := rfl
|
||
have h_cs_bracket (i : Fin 8) : (cs.strands i).bracket = (s.strands i).bracket := by
|
||
rw [h_cs_strands]
|
||
have h_cs_slot (i : Fin 8) : (cs.strands i).slot = (s.strands i).slot := by
|
||
rw [h_cs_strands]
|
||
have h_cs_residue (i : Fin 8) : (cs.strands i).residue = (s.strands i).residue := by
|
||
rw [h_cs_strands]
|
||
have h_cs_all_adm : (∀ i, (cs.strands i).bracket.admissible) = ∀ i, (s.strands i).bracket.admissible := by
|
||
rw [h_cs_strands]
|
||
have conj1 : (BraidEigensolid.encodeReceipt cs).crossing_matrix = (BraidEigensolid.encodeReceipt s).crossing_matrix := by
|
||
simp [BraidEigensolid.encodeReceipt, h_cs_bracket]
|
||
have conj2 : (BraidEigensolid.encodeReceipt cs).sidon_slack = (BraidEigensolid.encodeReceipt s).sidon_slack := by
|
||
simp [BraidEigensolid.encodeReceipt, h_cs_slot]
|
||
have conj3 : (BraidEigensolid.encodeReceipt cs).step_count = (BraidEigensolid.encodeReceipt s).step_count + 1 := by
|
||
simp [BraidEigensolid.encodeReceipt, h_cs_step]
|
||
have conj4 : (BraidEigensolid.encodeReceipt cs).residuals = (BraidEigensolid.encodeReceipt s).residuals := by
|
||
simp [BraidEigensolid.encodeReceipt, h_cs_strands]
|
||
have conj5 : (BraidEigensolid.encodeReceipt cs).write_time = 0 := by
|
||
simp [BraidEigensolid.encodeReceipt]
|
||
have conj6 : (BraidEigensolid.encodeReceipt cs).scar_absent = (BraidEigensolid.encodeReceipt s).scar_absent := by
|
||
simp [BraidEigensolid.encodeReceipt, h_cs_strands]
|
||
exact And.intro conj1 (And.intro conj2 (And.intro conj3 (And.intro conj4 (And.intro conj5 conj6))))
|
||
|
||
end SilverSight.BraidSpherionBridge |