Theme/Calibration.lean — FrcCore

1import FrcCore.Nat2import FrcCore.Theme.Field34/-!5# FrcCore.Theme.Calibration — the calibration of the coherent fraction (22:C30, 22:C31)6(the quantum theme; 22-quantum, the calibration construction of 30 October 2026)78Two sources of `m₁`, `m₂` cells, `c₁`, `c₂` of them on their synchronised orbits. Under the eighth realisation's clause9(a locked pair carries one step phase per coupling step in every branch, at any relative phase offset; a pair with a10spread cell carries, in place of the step phase, the cell's winding offset times it) the systematic conditional phase of a11pair run counts the locked–locked pairs, `c₁ c₂` step phases per coupling step against the `m₁ m₂` of the full-mass rate. The normalised rate is the framed rational `ρ = c₁ c₂ / (m₁ m₂)`, written12here as the pair `(c₁ c₂, m₁ m₂)` with equality by cross-multiplication (`feq`). The file decides, on counts alone:1314* `reference_rate`: against a spread-free reference (`c = m`) the normalised rate is the source's own fraction;15* `recover_sq`: for three sources the product of two normalised rates over the third returns the square of a fraction,16  `ρ_ij ρ_ik / ρ_jk = (c_i / m_i)²`;17* `quad_consistency`: `ρ_ij ρ_kl = ρ_ik ρ_jl` for four sources, the rank-one structure of the rate table;18* `unit_table`: spread-free sources give the unit entry, the standard-theory case.1920For the pairwise spread characteristic (22:C31), the ensemble average of a product of factors drawn independently is the21product of the averages: `dsum_eq` is that identity for finite weighted tables, `Σᵢ Σⱼ (pᵢ qⱼ)(gᵢ hⱼ) = (Σᵢ pᵢ gᵢ)(Σⱼ qⱼ hⱼ)`,22the product rule whose cyclotomic instance the ledger file evaluates in `ℤ[ζ_n]`. No axioms.23-/2425namespace FRC.Calibration2627/-- A framed rational as a pair (numerator, denominator); two pairs are equal as fractions when they cross-multiply. -/28def feq (a b : Nat × Nat) : Prop := a.1 * b.2 = b.1 * a.22930/-- 22:C30 — the normalised systematic rate of the pair run of sources `(c_i, m_i)` and `(c_j, m_j)`: the locked–locked31pairs over all pairs, `c_i c_j / (m_i m_j)`, the product of the two coherent fractions. -/32def rho (ci mi cj mj : Nat) : Nat × Nat := (ci * cj, mi * mj)3334/-- The product of two fractions. -/35def fmul (a b : Nat × Nat) : Nat × Nat := (a.1 * b.1, a.2 * b.2)3637/-- `(a b)(c d) = (a c)(b d)`: the one rearrangement every identity below uses. -/38theorem mul4 (a b c d : Nat) : (a * b) * (c * d) = (a * c) * (b * d) := by39  rw [FRC.Nat.mul_assoc, FRC.Nat.mul_left_comm b c d, ← FRC.Nat.mul_assoc]4041/-- 22:C30 — the rate law: the normalised rate is the product of the fractions, by definition of the count. -/42theorem rho_eq (ci mi cj mj : Nat) : rho ci mi cj mj = fmul (ci, mi) (cj, mj) := rfl4344/-- 22:C30 — against a spread-free reference (`c = m`) the normalised rate of the pair run is the source's own45fraction: `(c_i m) / (m_i m) = c_i / m_i`. -/46theorem reference_rate (ci mi m : Nat) : feq (rho ci mi m m) (ci, mi) := by47  show (ci * m) * mi = ci * (mi * m)48  rw [FRC.Nat.mul_assoc, Nat.mul_comm m mi]4950/-- 22:C30 — recovery from three pair runs: `ρ_ij ρ_ik = ρ_jk (c_i/m_i)²` as fractions, so the square of each fraction51is the product of its two rates over the third. -/52theorem recover_sq (ci mi cj mj ck mk : Nat) :53    feq (fmul (rho ci mi cj mj) (rho ci mi ck mk)) (fmul (rho cj mj ck mk) (ci * ci, mi * mi)) := by54  show ((ci * cj) * (ci * ck)) * ((mj * mk) * (mi * mi)) = ((cj * ck) * (ci * ci)) * ((mi * mj) * (mi * mk))55  rw [mul4 ci cj ci ck, mul4 mj mk mi mi, Nat.mul_comm mj mi, Nat.mul_comm mk mi, Nat.mul_comm (cj * ck) (ci * ci)]5657/-- 22:C30 — the rank-one table: `ρ_ij ρ_kl = ρ_ik ρ_jl` for four sources, every quadruple a consistency test of the law. -/58theorem quad_consistency (ci mi cj mj ck mk cl ml : Nat) :59    feq (fmul (rho ci mi cj mj) (rho ck mk cl ml)) (fmul (rho ci mi ck mk) (rho cj mj cl ml)) := by60  show ((ci * cj) * (ck * cl)) * ((mi * mk) * (mj * ml)) = ((ci * ck) * (cj * cl)) * ((mi * mj) * (mk * ml))61  rw [mul4 ci cj ck cl, mul4 mi mk mj ml]6263/-- 22:C30 — two spread-free sources give the unit entry: the standard theory is the table of ones. -/64theorem unit_table (m m' : Nat) : feq (rho m m m' m') (1, 1) := by65  show (m * m') * 1 = 1 * (m * m')66  rw [Nat.mul_one, Nat.one_mul]6768/-- The weighted sum `Σᵢ pᵢ gᵢ` of two tables (the ensemble average of `g` under the weights `p`, up to the total weight). -/69def wsum : List Nat → List Nat → Nat70  | [], _ => 071  | _ :: _, [] => 072  | p :: ps, g :: gs => p * g + wsum ps gs7374/-- One row of the double sum: `Σⱼ (p qⱼ)(g hⱼ)`. -/75def rowsum (p g : Nat) : List Nat → List Nat → Nat76  | [], _ => 077  | _ :: _, [] => 078  | q :: qs, h :: hs => (p * q) * (g * h) + rowsum p g qs hs7980/-- The double sum `Σᵢ Σⱼ (pᵢ qⱼ)(gᵢ hⱼ)`: the average of the product of two independent factors over the product ensemble. -/81def dsum : List Nat → List Nat → List Nat → List Nat → Nat82  | [], _, _, _ => 083  | _ :: _, [], _, _ => 084  | p :: ps, g :: gs, q, h => rowsum p g q h + dsum ps gs q h8586theorem rowsum_eq (p g : Nat) : ∀ (q h : List Nat), rowsum p g q h = (p * g) * wsum q h87  | [], h => by88    show 0 = (p * g) * 089    rw [Nat.mul_zero]90  | _ :: _, [] => by91    show 0 = (p * g) * 092    rw [Nat.mul_zero]93  | q :: qs, h :: hs => by94    show (p * q) * (g * h) + rowsum p g qs hs = (p * g) * (q * h + wsum qs hs)95    rw [rowsum_eq p g qs hs, Nat.left_distrib, mul4 p q g h]9697/-- 22:C31 — the product rule for independent ensembles: the double sum of the products of two weighted tables is the98product of their sums, `Σᵢ Σⱼ (pᵢ qⱼ)(gᵢ hⱼ) = (Σᵢ pᵢ gᵢ)(Σⱼ qⱼ hⱼ)`; the pairwise spread characteristic of two99independently prepared sources is the product of their own characteristics. -/100theorem dsum_eq : ∀ (p g q h : List Nat), dsum p g q h = wsum p g * wsum q h101  | [], _, q, h => by102    show 0 = 0 * wsum q h103    rw [Nat.zero_mul]104  | _ :: _, [], q, h => by105    show 0 = 0 * wsum q h106    rw [Nat.zero_mul]107  | p :: ps, g :: gs, q, h => by108    show rowsum p g q h + dsum ps gs q h = (p * g + wsum ps gs) * wsum q h109    rw [rowsum_eq, dsum_eq ps gs q h, FRC.Nat.add_mul]110111/-! ## Spread laws: the domain of the normalised rate and entanglement under spread (22:C33, 22:C34) -/112113section spread114open FRC.Shell115variable {q : Nat} [Pos q]116117/-- 22:C33 (ii) — a completely spread cell at a nontrivial character: on a prime shell the complete sum of a character of118order dividing `n` vanishes, `Σ_{ξ<n} w^ξ = 0` for `w^n = 1`, `w ≠ 1` (the telescoping geometric sum, then no zero divisors).119With `w = ζ^{mΔ}` this is the vanishing of the uniform law's characteristic at every nontrivial argument. -/120theorem complete_spread_zero (hq : FRC.Nat.isPrime q) (w : Shell q) (n : Nat) (hn : w ^ n = 1) (hw : w ≠ 1) :121    sumRange (fun ξ => w ^ ξ) n = 0 := by122  have hg := geom_sum_mul w n123  rw [hn, add_neg] at hg124  match Prime.mul_eq_zero hq hg with125  | .inl h => exact h126  | .inr h => exact absurd (Prime.eq_of_sub_eq_zero h) hw127128/-- 22:C33 (iv) — the two-point law `(δ₀ + δ₅)/2` on the cycle of order 12 vanishes at the argument 6: for `ζ` of order 12129on a prime shell, `ζ^6` squares to one and is not one, so it is `−1`, and `1 + ζ^{30} = 1 + ζ^6 = 0`. -/130theorem two_point_zero (hq : FRC.Nat.isPrime q) (ζ : Shell q) (h12 : ζ ^ 12 = 1) (h6 : ζ ^ 6 ≠ 1) : 1 + ζ ^ 30 = 0 := by131  have e30 : ζ ^ 30 = ζ ^ 6 := by132    rw [show (30 : Nat) = 12 * 2 + 6 from rfl, pow_add, pow_mul, h12, one_pow, one_mul]133  have hsq : ζ ^ 6 * ζ ^ 6 = 1 := by rw [← pow_add]; exact h12134  have hprod : (ζ ^ 6 + -1) * (ζ ^ 6 + 1) = 0 := by135    rw [right_distrib, left_distrib, left_distrib, hsq, mul_one, neg_one_mul, neg_one_mul, add_assoc,136      ← add_assoc (ζ ^ 6), add_neg, zero_add, add_neg]137  rw [e30]138  match Prime.mul_eq_zero hq hprod with139  | .inl h => exact absurd (Prime.eq_of_sub_eq_zero h) h6140  | .inr h => rw [add_comm]; exact h141142end spread143144/-! ### The complete-spread states of the four separation classes (22:C34), decided on their integer forms -/145146/-- The `i`-th element of a list, or the default past its end (structural, without the library's `getD`). -/147def nth {α : Type} (d : α) : List α → Nat → α148  | [], _ => d149  | x :: _, 0 => x150  | _ :: xs, i + 1 => nth d xs i151152/-- The entry `(i, j)` of an integer matrix given as rows. -/153def ent (M : List (List Int)) (i j : Nat) : Int := nth 0 (nth [] M i) j154155/-- The principal 2-minor on rows and columns `i, j`. -/156def pmin2 (M : List (List Int)) (i j : Nat) : Int := ent M i i * ent M j j - ent M i j * ent M j i157158/-- The principal 3-minor on `i, j, k` (the rule of Sarrus). -/159def pmin3 (M : List (List Int)) (i j k : Nat) : Int :=160  ent M i i * (ent M j j * ent M k k - ent M j k * ent M k j)161  - ent M i j * (ent M j i * ent M k k - ent M j k * ent M k i)162  + ent M i k * (ent M j i * ent M k j - ent M j j * ent M k i)163164/-- The determinant of a 4 × 4 matrix, by Laplace expansion along the first row. -/165def det4 (M : List (List Int)) : Int :=166  ent M 0 0 * pmin3 M 1 2 3 - ent M 0 1 * cof M 1 2 3 1 + ent M 0 2 * cof M 1 2 3 2 - ent M 0 3 * cof M 1 2 3 3167where168  /-- The 3 × 3 minor on rows `a b c` with the column `d` removed from `0 1 2 3`. -/169  cof (M : List (List Int)) (a b c d : Nat) : Int :=170    let cols := [0, 1, 2, 3].filter (· ≠ d)171    let sub := [a, b, c].map (fun r => cols.map (fun col => ent M r col))172    pmin3 sub 0 1 2173174/-- Nonnegativity of an integer, by its constructor. -/175def nonneg : Int → Bool176  | Int.ofNat _ => true177  | Int.negSucc _ => false178179/-- Positive semidefiniteness of a symmetric 4 × 4 integer matrix: every principal minor is nonnegative. -/180def psd4 (M : List (List Int)) : Bool :=181  [0, 1, 2, 3].all (fun i => nonneg (ent M i i)) &&182  [(0, 1), (0, 2), (0, 3), (1, 2), (1, 3), (2, 3)].all (fun p => nonneg (pmin2 M p.1 p.2)) &&183  [(0, 1, 2), (0, 1, 3), (0, 2, 3), (1, 2, 3)].all (fun t => nonneg (pmin3 M t.1 t.2.1 t.2.2)) &&184  nonneg (det4 M)185186/-- Four times the partial transpose of the complete-spread state: four distinct separations. -/187def ptDistinct : List (List Int) := [[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 1, 0], [0, 0, 0, 1]]188/-- One pair of separations equal (`r_LL = r_RR`, the linear layouts). -/189def ptOnePair : List (List Int) := [[1, 0, 0, 0], [0, 1, 1, 0], [0, 1, 1, 0], [0, 0, 0, 1]]190/-- Two pairs equal (`r_LL = r_RR` and `r_LR = r_RL`). -/191def ptTwoPairs : List (List Int) := [[1, 0, 0, 1], [0, 1, 1, 0], [0, 1, 1, 0], [1, 0, 0, 1]]192/-- Three separations equal (`r_LL = r_LR = r_RL`). -/193def ptThreeEqual : List (List Int) := [[1, 1, 1, 1], [1, 1, 0, 0], [1, 0, 1, 0], [1, 0, 0, 1]]194195/-- 22:C34 (i) — the three nondegenerate classes are positive under partial transposition, hence separable (Peres–Horodecki196for two qubits): every principal minor of the three integer forms is nonnegative. -/197theorem pt_psd_classes : psd4 ptDistinct = true ∧ psd4 ptOnePair = true ∧ psd4 ptTwoPairs = true := ⟨rfl, rfl, rfl⟩198199/-- 22:C34 (ii) — three equal separations: the partial transpose has a negative determinant, `−2` on the integer form,200so an eigenvalue is negative and the complete-spread state is entangled. -/201theorem three_equal_npt : det4 ptThreeEqual = -2 := rfl202203/-- The position of `x` in a list, if present. -/204def posOf (x : Nat) : List Nat → Nat → Option Nat205  | [], _ => none206  | y :: ys, i => if y = x then some i else posOf x ys (i + 1)207208/-- The relabelling of a list of separation labels by first occurrence. -/209def canon : List Nat → List Nat → List Nat210  | [], _ => []211  | x :: xs, seen =>212    match posOf x seen 0 with213    | some i => i :: canon xs seen214    | none => seen.length :: canon xs (seen ++ [x])215216/-- Insertion into a decreasing list. -/217def insertDesc (x : Nat) : List Nat → List Nat218  | [] => [x]219  | y :: ys => if y ≤ x then x :: y :: ys else y :: insertDesc x ys220221/-- Insertion sort, decreasing. -/222def sortDesc : List Nat → List Nat223  | [] => []224  | x :: xs => insertDesc x (sortDesc xs)225226/-- The block sizes of a canonical labelling, in decreasing order. -/227def blockSizes (l : List Nat) : List Nat :=228  sortDesc ((List.range l.length).filterMap (fun v => let c := l.count v; if c = 0 then none else some c))229230/-- The labellings of the four branches by separation, relabelled by first occurrence (every map from four branches to231four labels), and the nondegenerate ones among them: no three separations equal. -/232def labellings : List (List Nat) :=233  (List.range 4).flatMap fun a => (List.range 4).flatMap fun b => (List.range 4).flatMap fun c => (List.range 4).map fun d =>234    canon [a, b, c, d] []235236def nondegenerate : List (List Nat) := labellings.filter (fun l => l.all (fun v => l.count v < 3))237238/-- 22:C34 (i) — the nondegenerate geometries fall into exactly three classes by block sizes, four distinct, one pair239equal and two pairs equal: every nondegenerate labelling has one of the three block-size patterns, and each pattern occurs. -/240theorem nondegenerate_classes :241    (nondegenerate.all (fun l => [[1, 1, 1, 1], [2, 1, 1], [2, 2]].contains (blockSizes l)) &&242     [[1, 1, 1, 1], [2, 1, 1], [2, 2]].all (fun s => (nondegenerate.map blockSizes).contains s)) = true := by decide243244end FRC.Calibration245