Keys/Quantum.lean — FrcCore

1import FrcCore.Theme.Extension2import FrcCore.Theme.Tally3import FrcCore.Theme.Field4import FrcCore.Theme.Subject5import FrcCore.Theme.Quantum6import FrcCore.Theme.Observation7import FrcCore.Theme.Interference8import FrcCore.Theme.Composite910/-!11# FrcCore.Keys.Quantum — the keyed theorems of the quantum theme (ledger migration, task LM19)1213One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem14that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration15`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).16-/1718namespace FRC.Ledger1920-- Keys of the quantum theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)21/-- p00191 — 00:F2. \textbf{Multi-body registration}: an unequal-cycle composite returning below $\Om$ (Q20) recurs jointly at the lcm of its parts' registration periods; each pair's conserved offset lives on the $\gcd$ cycle (the quotient $A/\langle v\rangle$), and dephasing over every joint recurrence below $\Om$ is exact, extending the Born-rule count (F1) verbatim to unequal cycles (37-sim: joint recurrence verified, 1400/1400 characters cancel). -/22theorem p00191 : (∀ (n : Nat → Nat), (∀ (j : Nat), (0 : Nat) < n j) → ∀ (m L : Nat), (0 : Nat) < L → FRC.Quantum.Joint n m L → ∃ T, T ≤ L ∧ (0 : Nat) < T ∧ FRC.Quantum.Joint n m T ∧ (∀ (t : Nat), FRC.Quantum.Joint n m t ↔ t % T = (0 : Nat)) ∧ L % T = (0 : Nat)) ∧ (∀ {n : Nat → Nat} {m T : Nat}, (∀ (t : Nat), FRC.Quantum.Joint n m t ↔ t % T = (0 : Nat)) → (0 : Nat) < T → ∀ (t : Nat), (0 : Nat) < t → FRC.Quantum.Joint n m t → T ≤ t) ∧ (∀ {a b T : Nat}, (0 : Nat) < a → (0 : Nat) < b → (0 : Nat) < T → T % a = (0 : Nat) → T % b = (0 : Nat) → (∀ (t : Nat), (0 : Nat) < t → t < T → ¬(t % a = (0 : Nat) ∧ t % b = (0 : Nat))) → ∃ g, g ≤ a ∧ (0 : Nat) < g ∧ g * T = a * b ∧ a % g = (0 : Nat) ∧ b % g = (0 : Nat) ∧ (∀ (e : Nat), (0 : Nat) < e → a % e = (0 : Nat) → b % e = (0 : Nat) → g % e = (0 : Nat)) ∧ ∀ (x y x' y' : Nat), x < a → y < b → x' < a → y' < b → ((∃ t, t < T ∧ (x + t) % a = x' ∧ (y + t) % b = y') ↔ (x + y') % g = (x' + y) % g)) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ (n : Nat → Nat), (∀ (j : Nat), (0 : Nat) < n j) → ∀ (m : Nat) (ζ : Nat → FRC.Shell q), (∀ (j : Nat), j < m → ζ j ^ n j = (1 : FRC.Shell q)) → FRC.Shell.prodRange ζ m ≠ (1 : FRC.Shell q) → ∀ (M : Nat), FRC.Quantum.Joint n m M → FRC.Shell.sumRange (fun t => FRC.Shell.prodRange (fun j => ζ j ^ t) m) M = (0 : FRC.Shell q) :=23  And.intro @FRC.Quantum.joint_recurrence (And.intro @FRC.Quantum.joint_least (And.intro @FRC.Quantum.pair_offset (@FRC.Quantum.dephasing)))24/-- p00194 — 00:F5. \textbf{The graded registration law}: an Object component $\ell^{a}$ registers at depth $d=\mathrm{ord}_{\ell^{a}}(\p)$ --- $1$ absorbed (register, unique image), $2$ observable (odd $\ell$: boost torus, unique home; $2^{a}>4$: off both tori), else beyond-quadratic; the sign always $\{\pm1\}$. Visible iff $\p^{d}<\Om$; the cap is $2$ at saturating and minimal towers; opacity relational --- hydrogen's interior opaque/observable/absorbed at $173/181/197$. Controls: proton whole, $(5,13)$ refused. -/25theorem p00194 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {n : Nat}, (0 : Nat) < n → n ∣ p - (1 : Nat) → ∃ x, x ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Prime.HasOrder x n ∧ ∀ (y : FRC.Shell p), y ^ n = (1 : FRC.Shell p) → ∃ k, k < n ∧ y = x ^ k) ∧ (∀ {p : Nat}, (0 : Nat) < p → (∀ (e : Nat), (0 : Nat) < e → (p - (1 : Nat)) % e = (0 : Nat) → (p + (1 : Nat)) % e = (0 : Nat) → (2 : Nat) % e = (0 : Nat)) ∧ ∀ (l a : Nat), FRC.Nat.isPrime l → l ≠ (2 : Nat) → (p - (1 : Nat)) * (p + (1 : Nat)) % l ^ a = (0 : Nat) → (p - (1 : Nat)) % l ^ a ≠ (0 : Nat) → (p + (1 : Nat)) % l ^ a = (0 : Nat)) ∧ (∀ {κ : Nat}, κ % (2 : Nat) = (1 : Nat) → (4 : Nat) * κ % (4 : Nat) = (0 : Nat) ∧ (4 : Nat) * κ % (8 : Nat) ≠ (0 : Nat) ∧ ((4 : Nat) * κ + (2 : Nat)) % (2 : Nat) = (0 : Nat) ∧ ((4 : Nat) * κ + (2 : Nat)) % (4 : Nat) ≠ (0 : Nat) ∧ ∀ (a : Nat), (3 : Nat) ≤ a → (4 : Nat) * κ % (2 : Nat) ^ a ≠ (0 : Nat) ∧ ((4 : Nat) * κ + (2 : Nat)) % (2 : Nat) ^ a ≠ (0 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p], (2 : Nat) < p → p % (2 : Nat) = (1 : Nat) → (-1 : FRC.Shell p) ^ (p - (1 : Nat)) = (1 : FRC.Shell p) ∧ (-1 : FRC.Shell p) ^ (p + (1 : Nat)) = (1 : FRC.Shell p) ∧ (-1 : FRC.Shell p) * (-1 : FRC.Shell p) = (1 : FRC.Shell p) ∧ (-1 : FRC.Shell p) ≠ (1 : FRC.Shell p)) ∧ ((∀ (p Ω : Nat), (1 : Nat) < p → p * p < Ω → p < Ω) ∧ (∀ (p Ω : Nat), (3 : Nat) ≤ p → Ω ≤ (p + (1 : Nat)) * (p + (1 : Nat)) → Ω < p * p * p) ∧ ((173 : Nat) * (173 : Nat) < (30089 : Nat) ∧ (30089 : Nat) ≤ (174 : Nat) * (174 : Nat)) ∧ (1373 : Nat) * (1373 : Nat) < (2408561 : Nat) ∧ (2408561 : Nat) < (1373 : Nat) * (1373 : Nat) * (1373 : Nat)) ∧ ((173 : Nat) ^ (6 : Nat) % (7 : Nat) = (1 : Nat) ∧ ∀ (d : Nat), (0 : Nat) < d → d < (6 : Nat) → (173 : Nat) ^ d % (7 : Nat) ≠ (1 : Nat)) ∧ ((181 : Nat) ^ (2 : Nat) % (7 : Nat) = (1 : Nat) ∧ (181 : Nat) % (7 : Nat) ≠ (1 : Nat)) ∧ (197 : Nat) % (7 : Nat) = (1 : Nat) ∧ (∀ (v : Nat), v < (173 : Nat) → (FRC.Shell.ofNat v ^ (4 : Nat) = (1 : FRC.Shell (173 : Nat)) ↔ v = (1 : Nat) ∨ v = (80 : Nat) ∨ v = (93 : Nat) ∨ v = (172 : Nat))) ∧ ((172 : Nat) % (3 : Nat) ≠ (0 : Nat) ∧ (174 : Nat) % (3 : Nat) = (0 : Nat)) ∧ ((172 : Nat) % (4 : Nat) = (0 : Nat) ∧ (174 : Nat) % (6 : Nat) = (0 : Nat)) ∧ (13 : Nat) < (5 : Nat) * (5 : Nat) :=26  And.intro @FRC.Quantum.absorbed (And.intro @FRC.Quantum.unique_home (And.intro @FRC.Quantum.two_part_homes (And.intro @FRC.Quantum.sign_both (And.intro @FRC.Quantum.visibility_cap (@FRC.Quantum.registration_instances)))))27/-- p22002 — 22:A2. The Lorentzian split: the quadratic extension $\F_{\p^2}$, the Frobenius involution, the norm-one boost cycle of order $\p+1$, and the spinor double cover (the Dirac layer). -/28theorem p22002 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {h : FRC.Shell p}, h * h = (-1 : FRC.Shell p) → (∀ (x : FRC.Shell p), x ≠ (0 : FRC.Shell p) → (x ^ (p + (1 : Nat)) = (1 : FRC.Shell p) ↔ x = (1 : FRC.Shell p) ∨ x = (-1 : FRC.Shell p))) ∧ (∀ (x : FRC.Shell p), x ≠ (0 : FRC.Shell p) → (x ^ ((2 : Nat) * (p + (1 : Nat))) = (1 : FRC.Shell p) ↔ x = (1 : FRC.Shell p) ∨ x = (-1 : FRC.Shell p) ∨ x = h ∨ x = -h)) ∧ h ^ (p + (1 : Nat)) = (-1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Nat.isPrime p → ∀ {κ : Nat}, p = (4 : Nat) * κ + (1 : Nat) → (¬∃ y, y * y = ν) → ∀ (ζ : FRC.Extension.Ext p ν), ζ.norm = (1 : FRC.Shell p) → ζ ^ (p + (1 : Nat)) = (1 : FRC.Extension.Ext p ν) → (∀ (l : Nat), (0 : Nat) < l → l < p + (1 : Nat) → ζ ^ l ≠ (1 : FRC.Extension.Ext p ν)) → ζ ^ ((2 : Nat) * κ + (1 : Nat)) = (-1 : FRC.Extension.Ext p ν)) ∧ ∀ {q : Nat} [FRC.Pos q] {ν : FRC.Shell q} (z : FRC.Extension.Ext q ν), z.norm = (1 : FRC.Shell q) → z * z.conj = (1 : FRC.Extension.Ext q ν) :=29  And.intro @FRC.Subject.channel (And.intro @FRC.Subject.horizon_generator (@FRC.Observation.torus_conj_inv))30/-- p22017 — 22:C1. Characters are power maps $\psi_k(u)=u^k$, pairwise distinct: the wave function is the cycle read through a winding index. -/31theorem p22017 : (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ζ : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder ζ n → (∀ (u v : FRC.Shell q) (k : Nat), (u * v) ^ k = u ^ k * v ^ k) ∧ ∀ (k k' : Nat), k < n → k' < n → k ≠ k' → ζ ^ k ≠ ζ ^ k') ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {x : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder x n → ∀ (y : FRC.Shell q), y ^ n = (1 : FRC.Shell q) → ∃ k, k < n ∧ y = x ^ k) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ζ : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder ζ n → ∀ (χ : FRC.Shell q → FRC.Shell q), (∀ (a b : Nat), χ (ζ ^ a * ζ ^ b) = χ (ζ ^ a) * χ (ζ ^ b)) → χ (1 : FRC.Shell q) = (1 : FRC.Shell q) → ∃ k, k < n ∧ ∀ (j : Nat), χ (ζ ^ j) = (ζ ^ j) ^ k :=32  And.intro @FRC.Observation.power_maps (And.intro @FRC.Observation.roots_of_order (@FRC.Observation.character_is_power_map))33/-- p22018 — 22:C2. Stationary states are the winding modes: the drive's eigenvalues are distinct and a winding acquires a global phase of weight $k$ per chronon. -/34theorem p22018 : (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {g : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder g n → (∀ (u : FRC.Shell q) (k : Nat), (g * u) ^ k = g ^ k * u ^ k) ∧ ∀ (k k' : Nat), k < n → k' < n → g ^ k = g ^ k' → k = k') ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {g : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder g n → ∀ (ψ : FRC.Shell q → FRC.Shell q) {lam : FRC.Shell q}, (∀ (j : Nat), ψ (g * g ^ j) = lam * ψ (g ^ j)) → (ψ (1 : FRC.Shell q) = (0 : FRC.Shell q) → ∀ (j : Nat), ψ (g ^ j) = (0 : FRC.Shell q)) ∧ (ψ (1 : FRC.Shell q) ≠ (0 : FRC.Shell q) → ∃ k, k < n ∧ lam = g ^ k ∧ ∀ (j : Nat), ψ (g ^ j) = ψ (1 : FRC.Shell q) * (g ^ j) ^ k) :=35  And.intro @FRC.Observation.stationary (@FRC.Observation.stationary_modes)36/-- p22019 — 22:C3. The measurement vectors are a forced orthogonal basis: orthogonality $d\,\delta\delta$, resolution of identity, and Parseval are character theory, and the pointer basis is einselected by the algebra of the frames. -/37theorem p22019 : (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ {r r' : Nat}, r < d → r' < d → FRC.Shell.sumRange (fun j => ω ^ (r * j) * ω ^ ((d - r') * j)) d = if r = r' then FRC.Shell.ofNat d else (0 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (f g : Nat → FRC.Shell q), FRC.Shell.sumRange (fun r => FRC.Shell.sumRange (fun j => f j * ω ^ ((d - r) * j)) d * FRC.Shell.sumRange (fun l => g l * ω ^ (r * l)) d) d = FRC.Shell.ofNat d * FRC.Shell.sumRange (fun j => f j * g j) d) ∧ (∀ (a : Nat), a < (4 : Nat) → ∀ (b : Nat), b < (4 : Nat) → ∀ (c : Nat), c < (4 : Nat) → ∀ (d : Nat), d < (4 : Nat) → ∀ (r : Nat), r < (4 : Nat) → FRC.Extension.Tally.inversion (FRC.Extension.Tally.kernel (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d)) r = { re := (4 : Int) * FRC.Extension.Tally.coeff (Int.ofNat a) (Int.ofNat b) (Int.ofNat c) (Int.ofNat d) r, im := (0 : Int) }) ∧ have M := fun r u => FRC.Extension.Tally.GI.ipow (r * u); have d2 := fun a b c d => a * d + FRC.Extension.Tally.GI.smul (-1 : Int) (b * c); have e := fun r => M r; have det3 := fun f g h => f (1 : Nat) * d2 (g (2 : Nat)) (g (3 : Nat)) (h (2 : Nat)) (h (3 : Nat)) + FRC.Extension.Tally.GI.smul (-1 : Int) (f (2 : Nat) * d2 (g (1 : Nat)) (g (3 : Nat)) (h (1 : Nat)) (h (3 : Nat))) + f (3 : Nat) * d2 (g (1 : Nat)) (g (2 : Nat)) (h (1 : Nat)) (h (2 : Nat)); e (0 : Nat) (0 : Nat) * det3 (e (1 : Nat)) (e (2 : Nat)) (e (3 : Nat)) + FRC.Extension.Tally.GI.smul (-1 : Int) (e (1 : Nat) (0 : Nat) * det3 (e (0 : Nat)) (e (2 : Nat)) (e (3 : Nat))) + e (2 : Nat) (0 : Nat) * det3 (e (0 : Nat)) (e (1 : Nat)) (e (3 : Nat)) + FRC.Extension.Tally.GI.smul (-1 : Int) (e (3 : Nat) (0 : Nat) * det3 (e (0 : Nat)) (e (1 : Nat)) (e (2 : Nat))) = { re := (0 : Int), im := (-16 : Int) } :=38  And.intro @FRC.Observation.orthogonality (And.intro @FRC.Observation.parseval (And.intro @FRC.Extension.Tally.fourier_inversion (@FRC.Extension.Tally.dft_det)))39/-- p22020 — 22:C4. The selection rule: a pointer channel couples to an Object mode only when their core phases agree, $r\equiv k\pmod d$. -/40theorem p22020 : ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (k : Nat) {r : Nat}, r < d → FRC.Shell.sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d = if k % d = r then FRC.Shell.ofNat d else (0 : FRC.Shell q) :=41  @FRC.Observation.selection42/-- p22021 — 22:C5. The L\"uders update is projection, $\Pi^2=d\,\Pi$, so an immediately repeated measurement returns the same outcome. -/43theorem p22021 : ∀ {q : Nat} [FRC.Pos q] {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ {r : Nat}, r < d → ∀ (j m : Nat), FRC.Shell.sumRange (fun l => ω ^ (r * j) * ω ^ ((d - r) * l) * (ω ^ (r * l) * ω ^ ((d - r) * m))) d = FRC.Shell.ofNat d * (ω ^ (r * j) * ω ^ ((d - r) * m)) :=44  @FRC.Observation.lueders45/-- p22022 — 22:C6. Conjugation is cycle inversion, forced in each setting: the Frobenius on the boost cycle (the only non-trivial automorphism over $\F_\p$), exponent negation on the phase cycle, and on the ledger the complex conjugation, the automorphism that reduces to inversion. -/46theorem p22022 : (∀ {q : Nat} [FRC.Pos q] {ν : FRC.Shell q}, FRC.Nat.isPrime q → (¬∃ y, y * y = ν) → ∀ (σ : FRC.Extension.Ext q ν → FRC.Extension.Ext q ν), (∀ (c : FRC.Shell q), σ (FRC.Extension.Ext.ofShell c) = FRC.Extension.Ext.ofShell c) → (∀ (z z' : FRC.Extension.Ext q ν), σ (z + z') = σ z + σ z') → (∀ (z z' : FRC.Extension.Ext q ν), σ (z * z') = σ z * σ z') → (∀ (z : FRC.Extension.Ext q ν), σ z = z) ∨ ∀ (z : FRC.Extension.Ext q ν), σ z = z.conj) ∧ (∀ {q : Nat} [FRC.Pos q] {ν : FRC.Shell q} (z : FRC.Extension.Ext q ν), z.norm = (1 : FRC.Shell q) → z * z.conj = (1 : FRC.Extension.Ext q ν)) ∧ ∀ {q : Nat} [FRC.Pos q] {ζ : FRC.Shell q} {n : Nat}, ζ ^ n = (1 : FRC.Shell q) → ∀ {k : Nat}, k ≤ n → ζ ^ k * ζ ^ (n - k) = (1 : FRC.Shell q) :=47  And.intro @FRC.Observation.frobenius_unique (And.intro @FRC.Observation.torus_conj_inv (@FRC.Observation.exponent_negation))48/-- p22023 — 22:C7. Squared amplitudes are coincidence counts (the pair-count identity), realized tallies on $\Z[\im]$ for stationary core-valued states of definite drive eigenvalue; a distinct-eigenvalue superposition registers the integral drive-frequency count; for a pure winding the weights are $d^2[r\equiv k]$. -/49theorem p22023 : (∀ {q : Nat} [FRC.Pos q] (ψ ψbar : Nat → FRC.Shell q) (d : Nat), FRC.Shell.sumRange ψ d * FRC.Shell.sumRange ψbar d = FRC.Shell.sumRange (fun j => FRC.Shell.sumRange (fun l => ψ j * ψbar l) d) d) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (k : Nat) {r : Nat}, r < d → FRC.Shell.sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d * FRC.Shell.sumRange (fun l => ω ^ (r * l) * ω ^ ((d - k % d) * l)) d = if k % d = r then FRC.Shell.ofNat (d * d) else (0 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (f g : Nat → FRC.Shell q), FRC.Shell.sumRange (fun r => FRC.Shell.sumRange (fun j => f j * ω ^ ((d - r) * j)) d * FRC.Shell.sumRange (fun l => g l * ω ^ (r * l)) d) d = FRC.Shell.ofNat d * FRC.Shell.sumRange (fun j => f j * g j) d) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ (n : Nat → Nat), (∀ (j : Nat), (0 : Nat) < n j) → ∀ (m : Nat) (ζ : Nat → FRC.Shell q), (∀ (j : Nat), j < m → ζ j ^ n j = (1 : FRC.Shell q)) → FRC.Shell.prodRange ζ m ≠ (1 : FRC.Shell q) → ∀ (M : Nat), FRC.Quantum.Joint n m M → FRC.Shell.sumRange (fun t => FRC.Shell.prodRange (fun j => ζ j ^ t) m) M = (0 : FRC.Shell q) :=50  And.intro @FRC.Observation.pair_count (And.intro @FRC.Observation.pure_winding_weight (And.intro @FRC.Observation.parseval (@FRC.Quantum.dephasing)))51/-- p22024 — 22:C8. Sorkin nullity: $I_k=0$ for every $k\ge3$, exactly, on every channel and outcome, with $I_2$ generically nonzero. -/52theorem p22024 : (∀ {q : Nat} [FRC.Pos q] {c : FRC.Shell q → FRC.Shell q}, FRC.Interference.Additive c → ∀ (a : Nat → FRC.Shell q) (k : Nat) (x : FRC.Shell q), FRC.Interference.mixedDiff a (FRC.Interference.weight c) (k + (3 : Nat)) x = (0 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q] {c : FRC.Shell q → FRC.Shell q}, FRC.Interference.Additive c → ∀ (a : Nat → FRC.Shell q) (x : FRC.Shell q), FRC.Interference.mixedDiff a (FRC.Interference.weight c) (2 : Nat) x = a (1 : Nat) * c (a (0 : Nat)) + a (0 : Nat) * c (a (1 : Nat))) ∧ ∀ {q : Nat} [FRC.Pos q], (2 : Nat) < q → FRC.Interference.mixedDiff (fun x => (1 : FRC.Shell q)) (FRC.Interference.weight fun x => x) (2 : Nat) (0 : FRC.Shell q) ≠ (0 : FRC.Shell q) :=53  And.intro @FRC.Interference.sorkin_hierarchy (And.intro @FRC.Interference.sorkin_second (@FRC.Interference.sorkin_second_witness))54/-- p22025 — 22:C9. Reduction: the Carrier-chart amplitude is the mod-$\Omega$ shadow of the ledger ($\zeta\mapsto v$), exact as algebra and silent about magnitude. -/55theorem p22025 : (∀ {q : Nat} [FRC.Pos q] (v : FRC.Shell q) (c c' : Nat → Nat) (n : Nat), FRC.Observation.shadow v (fun e => c e + c' e) n = FRC.Observation.shadow v c n + FRC.Observation.shadow v c' n) ∧ (∀ {q : Nat} [FRC.Pos q] {v : FRC.Shell q} {n : Nat}, (0 : Nat) < n → v ^ n = (1 : FRC.Shell q) → ∀ (c c' : Nat → Nat), FRC.Observation.shadow v (FRC.Observation.conv c c' n) n = FRC.Observation.shadow v c n * FRC.Observation.shadow v c' n) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Shell.ofNat q = (0 : FRC.Shell q) :=56  And.intro @FRC.Observation.reduce_add (And.intro @FRC.Observation.reduce_mul (@FRC.Observation.reduce_wrap))57set_option linter.defProp false in58/-- p22026 — 22:C10. The counting Born rule on sub-horizon states over the universal core $\Qf$: the weight is the unique window lift of its shadow and the probability a framed-rational ratio of coincidence counts, the frequency along the drive completed in finitely many chronons; the two probability strata and their $\Qf$ coincidence; on a single Object the theorem's weights are uniform over the fibres (Remark~\ref{rem:borndomain}), every non-uniform statistic passing through C11. -/59def p22026 := And.intro @FRC.Extension.two_way_tally (And.intro @FRC.Extension.core_weights (And.intro @FRC.Extension.root_two_two_way (And.intro @FRC.Extension.framed_readout (And.intro @FRC.Observation.window_lift (And.intro @FRC.Observation.pure_winding_weight (@FRC.Quantum.joint_recurrence))))))60/-- p22029 — 22:C13. Complex amplitudes are forced: the generic shared core of two framed shells is $\Qf$, so the minimal ledger is $\Z[\im]$; shells of cardinality $\equiv3\pmod4$ (arising from no capacity) give a real-amplitude theory. -/61theorem p22029 : (∀ {q : Nat} [FRC.Pos q] {κ κ' a b : Nat}, κ * a = κ' * b + (1 : Nat) → ∀ (x : FRC.Shell q), x ^ ((4 : Nat) * κ) = (1 : FRC.Shell q) → x ^ ((4 : Nat) * κ') = (1 : FRC.Shell q) → x ^ (4 : Nat) = (1 : FRC.Shell q) ∧ ∀ (y : FRC.Shell q), y ^ (4 : Nat) = (1 : FRC.Shell q) → y ^ ((4 : Nat) * κ) = (1 : FRC.Shell q) ∧ y ^ ((4 : Nat) * κ') = (1 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → q % (4 : Nat) = (3 : Nat) → ¬∃ x, x * x = (-1 : FRC.Shell q) :=62  And.intro @FRC.Observation.shared_core (@FRC.Observation.no_quarter_turn)63/-- p22030 — 22:C14. The granularity ceiling: the representable coherent-splitting depth is the largest $k$ with $d\,T(k)<\Omega$, $T(k)=2^{k+[k\text{ odd}]}$ the minimal tally norm, and resolution finer than $1/\Omega$ lies outside the derived Born regime. -/64theorem p22030 : (∀ {q : Nat} [FRC.Pos q] {i : FRC.Shell q}, i * i = (-1 : FRC.Shell q) → ∀ (m : Nat), ((1 : FRC.Shell q) + i) ^ ((2 : Nat) * m) = FRC.Shell.ofNat ((2 : Nat) ^ m) * i ^ m) ∧ (∀ {q : Nat} [FRC.Pos q] {i : FRC.Shell q}, i * i = (-1 : FRC.Shell q) → ∀ (m : Nat), ((1 : FRC.Shell q) + i) ^ ((2 : Nat) * m + (1 : Nat)) = FRC.Shell.ofNat ((2 : Nat) ^ m) * i ^ m * ((1 : FRC.Shell q) + i)) ∧ (∀ {k k' : Nat}, k ≤ k' → FRC.Interference.tallyNorm k ≤ FRC.Interference.tallyNorm k') ∧ (∀ (k : Nat), FRC.Interference.tallyNorm k < (641 : Nat) ↔ k ≤ (8 : Nat)) ∧ ∀ (k : Nat), (8 : Nat) * FRC.Interference.tallyNorm k < (641 : Nat) ↔ k ≤ (6 : Nat) :=65  And.intro @FRC.Interference.hadamard_even (And.intro @FRC.Interference.hadamard_odd (And.intro @FRC.Interference.tally_norm_mono (@FRC.Interference.ceiling_641)))66/-- p22031 — 22:C15. The composite ledger and the conserved offset: synchronised orbits are the Bell states, the $m$-body locked cluster carries the offset as a conserved, drive-confined label (its ensemble diagonality a declared preparation clause). -/67theorem p22031 : (∀ {N : Nat}, (0 : Nat) < N → ∀ (t : Nat) (x : Nat → Nat) (j : Nat), (x j + (x (0 : Nat) + t) % N) % N = ((x j + t) % N + x (0 : Nat)) % N) ∧ (∀ {N m : Nat}, (0 : Nat) < N → (0 : Nat) < m → ∀ (x y : Nat → Nat), (∀ (j : Nat), j < m → y j < N) → ((∃ t, t < N ∧ ∀ (j : Nat), j < m → (x j + t) % N = y j) ↔ ∀ (j : Nat), j < m → (x j + y (0 : Nat)) % N = (y j + x (0 : Nat)) % N)) ∧ (∀ {q : Nat} [FRC.Pos q] (m : Nat) {χ χbar : FRC.Shell q}, χ * χbar = (1 : FRC.Shell q) → FRC.Shell.sumRange (fun x => χ) m = FRC.Shell.ofNat m * χ ∧ FRC.Shell.sumRange (fun x => χ) m * FRC.Shell.sumRange (fun x => χbar) m = FRC.Shell.ofNat (m * m)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ζ η : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder ζ n → ζ ≠ (1 : FRC.Shell q) → FRC.Shell.Prime.HasOrder η n → η ≠ (1 : FRC.Shell q) → ζ * η = (1 : FRC.Shell q) → ∀ (m : Nat), FRC.Composite.tsum n (fun v => FRC.Shell.sumRange (fun i => ζ ^ v i) m * FRC.Shell.sumRange (fun j => η ^ v j) m) m = FRC.Shell.ofNat m * FRC.Shell.ofNat (n ^ m)) ∧ ∀ {a b T : Nat}, (0 : Nat) < a → (0 : Nat) < b → (0 : Nat) < T → T % a = (0 : Nat) → T % b = (0 : Nat) → (∀ (t : Nat), (0 : Nat) < t → t < T → ¬(t % a = (0 : Nat) ∧ t % b = (0 : Nat))) → ∃ g, g ≤ a ∧ (0 : Nat) < g ∧ g * T = a * b ∧ a % g = (0 : Nat) ∧ b % g = (0 : Nat) ∧ (∀ (e : Nat), (0 : Nat) < e → a % e = (0 : Nat) → b % e = (0 : Nat) → g % e = (0 : Nat)) ∧ ∀ (x y x' y' : Nat), x < a → y < b → x' < a → y' < b → ((∃ t, t < T ∧ (x + t) % a = x' ∧ (y + t) % b = y') ↔ (x + y') % g = (x' + y) % g) :=68  And.intro @FRC.Composite.offset_invariant (And.intro @FRC.Composite.cluster_offset (And.intro @FRC.Composite.locked_norm (And.intro @FRC.Composite.spread_average (@FRC.Quantum.pair_offset))))69/-- p22032 — 22:C16. Qubits from doublets: the forced readout is $\sigma_x$ through the relation $v^{\,8}=-1$. -/70theorem p22032 : (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {v : FRC.Shell q}, FRC.Shell.Prime.HasOrder v (16 : Nat) → v ^ (8 : Nat) = (-1 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {v : FRC.Shell q}, FRC.Shell.Prime.HasOrder v (16 : Nat) → ∀ (k s : Nat) (lam : FRC.Shell q), FRC.Shell.sumRange (fun j => ((v ^ s * (v ^ (2 : Nat)) ^ j) ^ k + lam * (v ^ s * (v ^ (2 : Nat)) ^ j) ^ (k + (8 : Nat))) * (v ^ (2 : Nat)) ^ (((8 : Nat) - k % (8 : Nat)) * j)) (8 : Nat) = FRC.Shell.ofNat (8 : Nat) * (v ^ (s * k) * ((1 : FRC.Shell q) + lam * (v ^ (8 : Nat)) ^ s))) ∧ (641 : Nat) = (4 : Nat) * (160 : Nat) + (1 : Nat) ∧ FRC.Shell.Prime.HasOrder (3 : FRC.Shell (641 : Nat)) (640 : Nat) ∧ (3 : FRC.Shell (641 : Nat)) ^ (40 : Nat) = (601 : FRC.Shell (641 : Nat)) ∧ FRC.Shell.Prime.HasOrder (601 : FRC.Shell (641 : Nat)) (16 : Nat) ∧ (601 : FRC.Shell (641 : Nat)) ^ (8 : Nat) = (-1 : FRC.Shell (641 : Nat)) ∧ (3 : FRC.Shell (641 : Nat)) ^ (8 : Nat) = (151 : FRC.Shell (641 : Nat)) ∧ FRC.Shell.Prime.HasOrder (151 : FRC.Shell (641 : Nat)) (80 : Nat) ∧ (3 : FRC.Shell (641 : Nat)) ^ (80 : Nat) = (318 : FRC.Shell (641 : Nat)) ∧ (318 : FRC.Shell (641 : Nat)) ^ (4 : Nat) = (-1 : FRC.Shell (641 : Nat)) ∧ ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat)) * ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat)) = (2 : FRC.Shell (641 : Nat)) ∧ (2 : FRC.Shell (641 : Nat)) * ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat)) * ((2 : FRC.Shell (641 : Nat)) * ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat))) = (8 : FRC.Shell (641 : Nat)) ∧ (40 : Nat) % (8 : Nat) = (0 : Nat) ∧ (16 : Nat) % (8 : Nat) = (0 : Nat) ∧ ∀ (e : Nat), e < (41 : Nat) → (40 : Nat) % e = (0 : Nat) → (16 : Nat) % e = (0 : Nat) → (8 : Nat) % e = (0 : Nat) :=71  And.intro @FRC.Composite.half_turn_sixteen (And.intro @FRC.Composite.doublet_readout (@FRC.Composite.carrier_641))72/-- p22033 — 22:C17. Exact Tsirelson saturation: the singlet law $E(\Delta)=\cos(\pi\Delta/40)$ [chart], $S=2(\zeta_8+\zeta_8^{-1})$, $S^2=8$, the exhaustive $80^3$ sweep never exceeding it [chart]; no-signalling and the composite reduction commute. -/73theorem p22033 : (∀ {p : Nat} [FRC.Pos p] {ζ : FRC.Shell p}, ζ ^ (4 : Nat) = (-1 : FRC.Shell p) → (ζ + ζ ^ (7 : Nat)) * (ζ + ζ ^ (7 : Nat)) = (2 : FRC.Shell p)) ∧ (∀ {q : Nat} [FRC.Pos q] {ζ : FRC.Shell q}, ζ ^ (4 : Nat) = (-1 : FRC.Shell q) → (2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat)) * ((2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat))) = (8 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q] (c E : FRC.Shell q), c * ((1 : FRC.Shell q) + E) + c * ((1 : FRC.Shell q) + -E) = c * (2 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q] {v : FRC.Shell q} {n : Nat}, (0 : Nat) < n → v ^ n = (1 : FRC.Shell q) → ∀ (c c' : Nat → Nat), FRC.Observation.shadow v (FRC.Observation.conv c c' n) n = FRC.Observation.shadow v c n * FRC.Observation.shadow v c' n) ∧ (641 : Nat) = (4 : Nat) * (160 : Nat) + (1 : Nat) ∧ FRC.Shell.Prime.HasOrder (3 : FRC.Shell (641 : Nat)) (640 : Nat) ∧ (3 : FRC.Shell (641 : Nat)) ^ (40 : Nat) = (601 : FRC.Shell (641 : Nat)) ∧ FRC.Shell.Prime.HasOrder (601 : FRC.Shell (641 : Nat)) (16 : Nat) ∧ (601 : FRC.Shell (641 : Nat)) ^ (8 : Nat) = (-1 : FRC.Shell (641 : Nat)) ∧ (3 : FRC.Shell (641 : Nat)) ^ (8 : Nat) = (151 : FRC.Shell (641 : Nat)) ∧ FRC.Shell.Prime.HasOrder (151 : FRC.Shell (641 : Nat)) (80 : Nat) ∧ (3 : FRC.Shell (641 : Nat)) ^ (80 : Nat) = (318 : FRC.Shell (641 : Nat)) ∧ (318 : FRC.Shell (641 : Nat)) ^ (4 : Nat) = (-1 : FRC.Shell (641 : Nat)) ∧ ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat)) * ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat)) = (2 : FRC.Shell (641 : Nat)) ∧ (2 : FRC.Shell (641 : Nat)) * ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat)) * ((2 : FRC.Shell (641 : Nat)) * ((318 : FRC.Shell (641 : Nat)) + (318 : FRC.Shell (641 : Nat)) ^ (7 : Nat))) = (8 : FRC.Shell (641 : Nat)) ∧ (40 : Nat) % (8 : Nat) = (0 : Nat) ∧ (16 : Nat) % (8 : Nat) = (0 : Nat) ∧ ∀ (e : Nat), e < (41 : Nat) → (40 : Nat) % e = (0 : Nat) → (16 : Nat) % e = (0 : Nat) → (8 : Nat) % e = (0 : Nat) :=74  And.intro @FRC.Shell.Prime.tsirelson (And.intro @FRC.Composite.singlet_square (And.intro @FRC.Composite.no_signalling (And.intro @FRC.Observation.reduce_mul (@FRC.Composite.carrier_641))))75/-- p22034 — 22:C18. The network table is the complex-quantum table, and the Bell-state measurement is the offset readout. -/76theorem p22034 : (∀ {a b T : Nat}, (0 : Nat) < a → (0 : Nat) < b → (0 : Nat) < T → T % a = (0 : Nat) → T % b = (0 : Nat) → (∀ (t : Nat), (0 : Nat) < t → t < T → ¬(t % a = (0 : Nat) ∧ t % b = (0 : Nat))) → ∃ g, g ≤ a ∧ (0 : Nat) < g ∧ g * T = a * b ∧ a % g = (0 : Nat) ∧ b % g = (0 : Nat) ∧ (∀ (e : Nat), (0 : Nat) < e → a % e = (0 : Nat) → b % e = (0 : Nat) → g % e = (0 : Nat)) ∧ ∀ (x y x' y' : Nat), x < a → y < b → x' < a → y' < b → ((∃ t, t < T ∧ (x + t) % a = x' ∧ (y + t) % b = y') ↔ (x + y') % g = (x' + y) % g)) ∧ ∀ {N m : Nat}, (0 : Nat) < N → (0 : Nat) < m → ∀ (x y : Nat → Nat), (∀ (j : Nat), j < m → y j < N) → ((∃ t, t < N ∧ ∀ (j : Nat), j < m → (x j + t) % N = y j) ↔ ∀ (j : Nat), j < m → (x j + y (0 : Nat)) % N = (y j + x (0 : Nat)) % N) :=77  And.intro @FRC.Quantum.pair_offset (@FRC.Composite.cluster_offset)78/-- p22035 — 22:C19. The gravitational channel entangles exactly, $C^2=\sin^2(\varphi/2)$ [chart], with the pure-channel complementarity $V^2+C^2=1$. -/79theorem p22035 : (∀ {q : Nat} [FRC.Pos q] {h x y i : FRC.Shell q}, h * (2 : FRC.Shell q) = (1 : FRC.Shell q) → x * y = (1 : FRC.Shell q) → i * i = (-1 : FRC.Shell q) → h * (x + y) * (h * (x + y)) + h * (x + -y) * -i * (h * (x + -y) * -i) = (1 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q] (h x i : FRC.Shell q), h * (x + -x) * -i = (0 : FRC.Shell q) :=80  And.intro @FRC.Composite.channel_complementarity (@FRC.Composite.channel_product_at_zero)81/-- p22036 — 22:C20. No spontaneous collapse; the dilation floor dephases with an exact revival $V(n)=1$. -/82theorem p22036 : (∀ {q : Nat} [FRC.Pos q] {u ub : FRC.Shell q}, u * ub = (1 : FRC.Shell q) → ∀ (a ab : FRC.Shell q), u * a * (ub * ab) = a * ab) ∧ (∀ {q : Nat} [FRC.Pos q] {ζ : FRC.Shell q} {n : Nat}, ζ ^ n = (1 : FRC.Shell q) → ∀ (p : Nat → FRC.Shell q) (M : Nat), FRC.Shell.sumRange (fun E => p E * ζ ^ (E * n)) M = FRC.Shell.sumRange p M) ∧ ∀ (n : Nat → Nat), (∀ (j : Nat), (0 : Nat) < n j) → ∀ (m L : Nat), (0 : Nat) < L → FRC.Quantum.Joint n m L → ∃ T, T ≤ L ∧ (0 : Nat) < T ∧ FRC.Quantum.Joint n m T ∧ (∀ (t : Nat), FRC.Quantum.Joint n m t ↔ t % T = (0 : Nat)) ∧ L % T = (0 : Nat) :=83  And.intro @FRC.Composite.drive_norm (And.intro @FRC.Composite.revival (@FRC.Quantum.joint_recurrence))84/-- p22037 — 22:C21. The coherent-fraction channel: force by full masses, entanglement by coherent fractions; the identification reciprocal synchronisation (B8), and the fully incoherent channel is separable at generic (nondegenerate) geometry. -/85theorem p22037 : (∀ {q : Nat} [FRC.Pos q] (ζ : FRC.Shell q) (a mc : Nat), FRC.Shell.prodRange (fun x => ζ ^ a) mc = ζ ^ (mc * a)) ∧ (∀ {q : Nat} [FRC.Pos q] (ζ : FRC.Shell q) (a m1 m2 : Nat), (ζ ^ (m1 * a)) ^ m2 = ζ ^ (m1 * m2 * a)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ζ : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder ζ n → ζ ≠ (1 : FRC.Shell q) → FRC.Shell.sumRange (fun θ => ζ ^ θ) n = (0 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q] (ζ : FRC.Shell q) (p : Nat → FRC.Shell q) (n c : Nat), FRC.Shell.sumRange (fun θ => p θ * ζ ^ (θ + c)) n = FRC.Shell.sumRange (fun θ => p θ * ζ ^ θ) n * ζ ^ c :=86  And.intro @FRC.Composite.branch_phase (And.intro @FRC.Composite.pair_product (And.intro @FRC.Composite.spread_cancels (@FRC.Composite.channel_assembly)))87/-- p22038 — 22:C22. The two scaling laws and the exact equivalence-principle null: coherent $m^2$ against incoherent $m$, $\eta=0$. -/88theorem p22038 : (∀ {q : Nat} [FRC.Pos q] (m : Nat) (u : FRC.Shell q), FRC.Shell.sumRange (fun x => u) m = FRC.Shell.ofNat m * u) ∧ (∀ {q : Nat} [FRC.Pos q] (mt w g : FRC.Shell q), mt * w = (1 : FRC.Shell q) → mt * g * w = g) ∧ (∀ {q : Nat} [FRC.Pos q] (m : Nat) {χ χbar : FRC.Shell q}, χ * χbar = (1 : FRC.Shell q) → FRC.Shell.sumRange (fun x => χ) m = FRC.Shell.ofNat m * χ ∧ FRC.Shell.sumRange (fun x => χ) m * FRC.Shell.sumRange (fun x => χbar) m = FRC.Shell.ofNat (m * m)) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ζ η : FRC.Shell q} {n : Nat}, FRC.Shell.Prime.HasOrder ζ n → ζ ≠ (1 : FRC.Shell q) → FRC.Shell.Prime.HasOrder η n → η ≠ (1 : FRC.Shell q) → ζ * η = (1 : FRC.Shell q) → ∀ (m : Nat), FRC.Composite.tsum n (fun v => FRC.Shell.sumRange (fun i => ζ ^ v i) m * FRC.Shell.sumRange (fun j => η ^ v j) m) m = FRC.Shell.ofNat m * FRC.Shell.ofNat (n ^ m) :=89  And.intro @FRC.Composite.field_linear (And.intro @FRC.Composite.eta_zero (And.intro @FRC.Composite.locked_norm (@FRC.Composite.spread_average)))90/-- p22039 — 22:C23. Inter-Subject consistency: two distinct Subjects reading one Object agree on the shared core $\Qf$ , order-independent joint refinement, the same core character by the selection rule, and order-independence on the shared cell. -/91theorem p22039 : (∀ (α β : Nat), (0 : Nat) < α → (0 : Nat) < β → ∃ T, T ≤ α * β ∧ (0 : Nat) < T ∧ ∀ (x : Nat), x % α = (0 : Nat) ∧ x % β = (0 : Nat) ↔ x % T = (0 : Nat)) ∧ (∀ {a b e r r' k : Nat}, (0 : Nat) < e → (0 : Nat) < a → (0 : Nat) < b → a % e = (0 : Nat) → b % e = (0 : Nat) → r % a = k % a → r' % b = k % b → r % e = r' % e) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (k : Nat) {r : Nat}, r < d → FRC.Shell.sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d = if k % d = r then FRC.Shell.ofNat d else (0 : FRC.Shell q) :=92  And.intro @FRC.Composite.joint_refinement (And.intro @FRC.Composite.order_independence (@FRC.Observation.selection))93/-- p22040 — 22:C24. Carrier-chart classicality: to the host of a hosted Carrier every observation is total absorption (for the physical Carrier, a limit no reader instantiates); quantumness is the subgroup index $[\PhiO:\core]>1$, and classicality is the divisibility of the observer's frame --- one outcome per fixed channel, with the channel index still carrying the winding information (absorption is not the absence of information transfer). -/94theorem p22040 : (∀ {d k : Nat}, (0 : Nat) < d → (k = (1 : Nat) ↔ d * k = d) ∧ ((1 : Nat) < k ↔ d < d * k)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (k : Nat) {r : Nat}, r < d → FRC.Shell.sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d = if k % d = r then FRC.Shell.ofNat d else (0 : FRC.Shell q)) ∧ (421 : Nat) = (4 : Nat) * (105 : Nat) + (1 : Nat) ∧ FRC.Shell.Prime.HasOrder (2 : FRC.Shell (421 : Nat)) (420 : Nat) ∧ (2 : FRC.Shell (421 : Nat)) ^ (315 : Nat) = (392 : FRC.Shell (421 : Nat)) ∧ (392 : FRC.Shell (421 : Nat)) * (392 : FRC.Shell (421 : Nat)) = (-1 : FRC.Shell (421 : Nat)) ∧ ((60 : Nat) % (4 : Nat) = (0 : Nat) ∧ (28 : Nat) % (4 : Nat) = (0 : Nat) ∧ ∀ (e : Nat), e < (61 : Nat) → (60 : Nat) % e = (0 : Nat) → (28 : Nat) % e = (0 : Nat) → (4 : Nat) % e = (0 : Nat)) ∧ (28 : Nat) = (4 : Nat) * (7 : Nat) ∧ ((60 : Nat) % (12 : Nat) = (0 : Nat) ∧ (12 : Nat) % (12 : Nat) = (0 : Nat) ∧ ∀ (e : Nat), e < (61 : Nat) → (60 : Nat) % e = (0 : Nat) → (12 : Nat) % e = (0 : Nat) → (12 : Nat) % e = (0 : Nat)) ∧ (12 : Nat) = (12 : Nat) * (1 : Nat) :=95  And.intro @FRC.Observation.classicality_index (And.intro @FRC.Observation.selection (@FRC.Composite.carrier_421))96/-- p22041 — 22:C25. The measurement problem dissolved: Kochen--Specker poses no separate threat because values exist only as Subject-relative quotient phases, carried together with the Tsirelson strength $2\sqrt2$ [chart]. -/97theorem p22041 : (∀ {p : Nat} [FRC.Pos p] {ζ : FRC.Shell p}, ζ ^ (4 : Nat) = (-1 : FRC.Shell p) → (ζ + ζ ^ (7 : Nat)) * (ζ + ζ ^ (7 : Nat)) = (2 : FRC.Shell p)) ∧ ∀ {q : Nat} [FRC.Pos q] {ζ : FRC.Shell q}, ζ ^ (4 : Nat) = (-1 : FRC.Shell q) → (2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat)) * ((2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat))) = (8 : FRC.Shell q) :=98  And.intro @FRC.Shell.Prime.tsirelson (@FRC.Composite.singlet_square)99/-- p22042 — 22:C26. The unequal-cycle composite gate: joint recurrence $T'=\operatorname{lcm}_j(n_j/\gcd(s_j,n_j))$, conserved data the quotient $A/\langle s\rangle$ (unit-winding pair: the gcd cycle, generically $\Qf$), and the counting Born rule verbatim with $T'$ as the recurrence; all orbit-nontrivial characters cancel. -/100theorem p22042 : (∀ (n : Nat → Nat), (∀ (j : Nat), (0 : Nat) < n j) → ∀ (m L : Nat), (0 : Nat) < L → FRC.Quantum.Joint n m L → ∃ T, T ≤ L ∧ (0 : Nat) < T ∧ FRC.Quantum.Joint n m T ∧ (∀ (t : Nat), FRC.Quantum.Joint n m t ↔ t % T = (0 : Nat)) ∧ L % T = (0 : Nat)) ∧ (∀ {n : Nat → Nat} {m T : Nat}, (∀ (t : Nat), FRC.Quantum.Joint n m t ↔ t % T = (0 : Nat)) → (0 : Nat) < T → ∀ (t : Nat), (0 : Nat) < t → FRC.Quantum.Joint n m t → T ≤ t) ∧ (∀ {a b T : Nat}, (0 : Nat) < a → (0 : Nat) < b → (0 : Nat) < T → T % a = (0 : Nat) → T % b = (0 : Nat) → (∀ (t : Nat), (0 : Nat) < t → t < T → ¬(t % a = (0 : Nat) ∧ t % b = (0 : Nat))) → ∃ g, g ≤ a ∧ (0 : Nat) < g ∧ g * T = a * b ∧ a % g = (0 : Nat) ∧ b % g = (0 : Nat) ∧ (∀ (e : Nat), (0 : Nat) < e → a % e = (0 : Nat) → b % e = (0 : Nat) → g % e = (0 : Nat)) ∧ ∀ (x y x' y' : Nat), x < a → y < b → x' < a → y' < b → ((∃ t, t < T ∧ (x + t) % a = x' ∧ (y + t) % b = y') ↔ (x + y') % g = (x' + y) % g)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ (n : Nat → Nat), (∀ (j : Nat), (0 : Nat) < n j) → ∀ (m : Nat) (ζ : Nat → FRC.Shell q), (∀ (j : Nat), j < m → ζ j ^ n j = (1 : FRC.Shell q)) → FRC.Shell.prodRange ζ m ≠ (1 : FRC.Shell q) → ∀ (M : Nat), FRC.Quantum.Joint n m M → FRC.Shell.sumRange (fun t => FRC.Shell.prodRange (fun j => ζ j ^ t) m) M = (0 : FRC.Shell q)) ∧ ∀ {n s d n' s' u v : Nat}, (0 : Nat) < d → (0 : Nat) < n' → n = d * n' → s = d * s' → s' * u = n' * v + (1 : Nat) → ∀ (t : Nat), s * t % n = (0 : Nat) ↔ t % n' = (0 : Nat) :=101  And.intro @FRC.Quantum.joint_recurrence (And.intro @FRC.Quantum.joint_least (And.intro @FRC.Quantum.pair_offset (And.intro @FRC.Quantum.dephasing (@FRC.Composite.winding_period))))102/-- p22043 — 22:C27. Quarter-turn transport: the ambient quarter-turn aliases onto an embedded label iff $\kap\equiv\pm\kap_n\pmod n$, the capacity residue mod~$4$ the coarsest invariant; the constants web is read per register (Remark~\ref{rem:conceptual}). -/103theorem p22043 : (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ζ : FRC.Shell q} {m κ t : Nat}, FRC.Shell.Prime.HasOrder ζ ((4 : Nat) * m) → κ = m * t → (ζ ^ ((3 : Nat) * κ) = ζ ^ ((3 : Nat) * m) ↔ κ % ((4 : Nat) * m) = m) ∧ (ζ ^ ((3 : Nat) * κ) = ζ ^ m ↔ (κ + m) % ((4 : Nat) * m) = (0 : Nat)) ∧ (ζ ^ ((3 : Nat) * κ) * ζ ^ ((3 : Nat) * κ) = (1 : FRC.Shell q) ↔ κ % ((2 : Nat) * m) = (0 : Nat))) ∧ (∀ (κ : Nat), κ < (40 : Nat) → ((3 : Nat) * κ % (40 : Nat) = (3 : Nat) * (10 : Nat) % (40 : Nat) ↔ κ % (40 : Nat) = (10 : Nat) % (40 : Nat)) ∧ ((3 : Nat) * κ % (40 : Nat) = (10 : Nat) % (40 : Nat) ↔ (κ + (10 : Nat)) % (40 : Nat) = (0 : Nat)) ∧ ((3 : Nat) * κ * (2 : Nat) % (40 : Nat) = (0 : Nat) ↔ κ % (20 : Nat) = (0 : Nat))) ∧ (∀ (κ : Nat), κ < (4 : Nat) → ((3 : Nat) * κ % (4 : Nat) = (3 : Nat) % (4 : Nat) ↔ κ % (4 : Nat) = (1 : Nat)) ∧ ((3 : Nat) * κ % (4 : Nat) = (1 : Nat) % (4 : Nat) ↔ κ % (4 : Nat) = (3 : Nat)) ∧ ((3 : Nat) * κ * (2 : Nat) % (4 : Nat) = (0 : Nat) ↔ κ % (2 : Nat) = (0 : Nat))) ∧ ∀ (t : Nat), t < (4 : Nat) → ((3 : Nat) * ((3 : Nat) * t) % (12 : Nat) = (9 : Nat) % (12 : Nat) ↔ (3 : Nat) * t % (12 : Nat) = (3 : Nat)) :=104  And.intro @FRC.Observation.transport_trichotomy (@FRC.Observation.transport_cases)105set_option linter.defProp false in106/-- p22044 — 22:X1. \textbf{The Born rule} is a coincidence count, the unique window lift of its carrier shadow, not a postulated quadratic functional --- on its stationary domain, where the weights are uniform over the fibres; non-uniform statistics are read through the engineered-core readout (C11). -/107def p22044 := And.intro @FRC.Observation.window_lift (And.intro @FRC.Observation.pair_count (And.intro @FRC.Observation.pure_winding_weight (@FRC.Extension.two_way_tally)))108/-- p22045 — 22:X2. \textbf{The complexity of amplitudes} is the arithmetic of the shared quarter-turn core, the canonical complex sector $\Z[\im]$; a shell without the internal quarter-turn gives a real-amplitude theory instead. -/109theorem p22045 : (∀ {q : Nat} [FRC.Pos q] {κ κ' a b : Nat}, κ * a = κ' * b + (1 : Nat) → ∀ (x : FRC.Shell q), x ^ ((4 : Nat) * κ) = (1 : FRC.Shell q) → x ^ ((4 : Nat) * κ') = (1 : FRC.Shell q) → x ^ (4 : Nat) = (1 : FRC.Shell q) ∧ ∀ (y : FRC.Shell q), y ^ (4 : Nat) = (1 : FRC.Shell q) → y ^ ((4 : Nat) * κ) = (1 : FRC.Shell q) ∧ y ^ ((4 : Nat) * κ') = (1 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → q % (4 : Nat) = (3 : Nat) → ¬∃ x, x * x = (-1 : FRC.Shell q) :=110  And.intro @FRC.Observation.shared_core (@FRC.Observation.no_quarter_turn)111/-- p22046 — 22:X3. \textbf{The preferred basis} is the Subject's own phase anatomy, einselected by the algebra of the frames rather than by a model of the environment. -/112theorem p22046 : (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ {r r' : Nat}, r < d → r' < d → FRC.Shell.sumRange (fun j => ω ^ (r * j) * ω ^ ((d - r') * j)) d = if r = r' then FRC.Shell.ofNat d else (0 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (k : Nat) {r : Nat}, r < d → FRC.Shell.sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d = if k % d = r then FRC.Shell.ofNat d else (0 : FRC.Shell q) :=113  And.intro @FRC.Observation.orthogonality (@FRC.Observation.selection)114/-- p22047 — 22:X4. \textbf{The dynamical measurement problem} dissolves: collapse is the re-metrisation of a relational chart, no disturbance propagates, and distinct Subjects never disagree on what they share. -/115theorem p22047 : (∀ (α β : Nat), (0 : Nat) < α → (0 : Nat) < β → ∃ T, T ≤ α * β ∧ (0 : Nat) < T ∧ ∀ (x : Nat), x % α = (0 : Nat) ∧ x % β = (0 : Nat) ↔ x % T = (0 : Nat)) ∧ (∀ {a b e r r' k : Nat}, (0 : Nat) < e → (0 : Nat) < a → (0 : Nat) < b → a % e = (0 : Nat) → b % e = (0 : Nat) → r % a = k % a → r' % b = k % b → r % e = r' % e) ∧ ∀ {q : Nat} [FRC.Pos q] {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ {r : Nat}, r < d → ∀ (j m : Nat), FRC.Shell.sumRange (fun l => ω ^ (r * j) * ω ^ ((d - r) * l) * (ω ^ (r * l) * ω ^ ((d - r) * m))) d = FRC.Shell.ofNat d * (ω ^ (r * j) * ω ^ ((d - r) * m)) :=116  And.intro @FRC.Composite.joint_refinement (And.intro @FRC.Composite.order_independence (@FRC.Observation.lueders))117/-- p22048 — 22:X5. \textbf{The classical limit} has a mechanism, containment, the divisibility of the observer's frame, exact arithmetic rather than an appeal to a limit. -/118theorem p22048 : (∀ {d k : Nat}, (0 : Nat) < d → (k = (1 : Nat) ↔ d * k = d) ∧ ((1 : Nat) < k ↔ d < d * k)) ∧ (∀ {q : Nat} [FRC.Pos q], FRC.Nat.isPrime q → ∀ {ω : FRC.Shell q} {d : Nat}, FRC.Shell.Prime.HasOrder ω d → ∀ (k : Nat) {r : Nat}, r < d → FRC.Shell.sumRange (fun j => ω ^ (k * j) * ω ^ ((d - r) * j)) d = if k % d = r then FRC.Shell.ofNat d else (0 : FRC.Shell q)) ∧ (421 : Nat) = (4 : Nat) * (105 : Nat) + (1 : Nat) ∧ FRC.Shell.Prime.HasOrder (2 : FRC.Shell (421 : Nat)) (420 : Nat) ∧ (2 : FRC.Shell (421 : Nat)) ^ (315 : Nat) = (392 : FRC.Shell (421 : Nat)) ∧ (392 : FRC.Shell (421 : Nat)) * (392 : FRC.Shell (421 : Nat)) = (-1 : FRC.Shell (421 : Nat)) ∧ ((60 : Nat) % (4 : Nat) = (0 : Nat) ∧ (28 : Nat) % (4 : Nat) = (0 : Nat) ∧ ∀ (e : Nat), e < (61 : Nat) → (60 : Nat) % e = (0 : Nat) → (28 : Nat) % e = (0 : Nat) → (4 : Nat) % e = (0 : Nat)) ∧ (28 : Nat) = (4 : Nat) * (7 : Nat) ∧ ((60 : Nat) % (12 : Nat) = (0 : Nat) ∧ (12 : Nat) % (12 : Nat) = (0 : Nat) ∧ ∀ (e : Nat), e < (61 : Nat) → (60 : Nat) % e = (0 : Nat) → (12 : Nat) % e = (0 : Nat) → (12 : Nat) % e = (0 : Nat)) ∧ (12 : Nat) = (12 : Nat) * (1 : Nat) :=119  And.intro @FRC.Observation.classicality_index (And.intro @FRC.Observation.selection (@FRC.Composite.carrier_421))120set_option linter.defProp false in121/-- p22049 — 22:X6. \textbf{Native probability over a finite substrate}: the unordered-field obstruction is cleared by keeping counts in the observer's ledger: a finite-relational provenance theorem for the Born calculus, in which the substrate determines the tally ring, the measurement family, and the readout (calibrated against the counting and cyclotomic precedents in Section~\ref{sec:discussion}). -/122def p22049 := And.intro @FRC.Observation.window_lift (And.intro @FRC.Extension.Tally.tally_criterion (And.intro @FRC.Extension.Tally.channel_selectivity (@FRC.Extension.framed_readout)))123/-- p22050 — 22:X7. \textbf{The Tsirelson boundary} is attained as a ring identity, $S=2(\zeta_8+\zeta_8^{-1})=2\sqrt2$ [chart], so a relational finite substrate carries full quantum correlation strength, not merely quantum vocabulary. -/124theorem p22050 : (∀ {p : Nat} [FRC.Pos p] {ζ : FRC.Shell p}, ζ ^ (4 : Nat) = (-1 : FRC.Shell p) → (ζ + ζ ^ (7 : Nat)) * (ζ + ζ ^ (7 : Nat)) = (2 : FRC.Shell p)) ∧ ∀ {q : Nat} [FRC.Pos q] {ζ : FRC.Shell q}, ζ ^ (4 : Nat) = (-1 : FRC.Shell q) → (2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat)) * ((2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat))) = (8 : FRC.Shell q) :=125  And.intro @FRC.Shell.Prime.tsirelson (@FRC.Composite.singlet_square)126/-- p22051 — 22:X8. \textbf{Higher-order interference} is forbidden exactly: the Sorkin hierarchy is zero with a forbidden neighbourhood, not a small number to be measured down. -/127theorem p22051 : (∀ {q : Nat} [FRC.Pos q] {c : FRC.Shell q → FRC.Shell q}, FRC.Interference.Additive c → ∀ (a : Nat → FRC.Shell q) (k : Nat) (x : FRC.Shell q), FRC.Interference.mixedDiff a (FRC.Interference.weight c) (k + (3 : Nat)) x = (0 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q] (a : Nat), FRC.Shell.ofNat a = (0 : FRC.Shell q) ↔ ∃ k, a = q * k :=128  And.intro @FRC.Interference.sorkin_hierarchy (@FRC.Observation.wrap_quantised)129/-- p22052 — 22:P1. Gravitationally induced entanglement at exactly the Newtonian rate [chart], $V^2+C^2=1$ on the pure channel: equal force but unequal entanglement --- a source gravitates by its full mass while the systematic conditional phase, the calibrated discriminator, is carried by the coherent sectors alone, the fully incoherent channel separable at generic (nondegenerate) geometry. The one dated forward prediction. -/130theorem p22052 : (∀ {q : Nat} [FRC.Pos q] {h x y i : FRC.Shell q}, h * (2 : FRC.Shell q) = (1 : FRC.Shell q) → x * y = (1 : FRC.Shell q) → i * i = (-1 : FRC.Shell q) → h * (x + y) * (h * (x + y)) + h * (x + -y) * -i * (h * (x + -y) * -i) = (1 : FRC.Shell q)) ∧ (∀ {q : Nat} [FRC.Pos q] (ζ : FRC.Shell q) (a mc : Nat), FRC.Shell.prodRange (fun x => ζ ^ a) mc = ζ ^ (mc * a)) ∧ ∀ {q : Nat} [FRC.Pos q] (ζ : FRC.Shell q) (p : Nat → FRC.Shell q) (n c : Nat), FRC.Shell.sumRange (fun θ => p θ * ζ ^ (θ + c)) n = FRC.Shell.sumRange (fun θ => p θ * ζ ^ θ) n * ζ ^ c :=131  And.intro @FRC.Composite.channel_complementarity (And.intro @FRC.Composite.branch_phase (@FRC.Composite.channel_assembly))132/-- p22053 — 22:P2. Third-order interference exactly zero at every accessible scale, any wrap quantised to a multiple of $\Omega$: a single confirmed small $I_3\neq0$ falsifies outright. -/133theorem p22053 : (∀ {q : Nat} [FRC.Pos q] {c : FRC.Shell q → FRC.Shell q}, FRC.Interference.Additive c → ∀ (a : Nat → FRC.Shell q) (k : Nat) (x : FRC.Shell q), FRC.Interference.mixedDiff a (FRC.Interference.weight c) (k + (3 : Nat)) x = (0 : FRC.Shell q)) ∧ ∀ {q : Nat} [FRC.Pos q] (a : Nat), FRC.Shell.ofNat a = (0 : FRC.Shell q) ↔ ∃ k, a = q * k :=134  And.intro @FRC.Interference.sorkin_hierarchy (@FRC.Observation.wrap_quantised)135/-- p22054 — 22:P3. The Tsirelson value $S=2\sqrt2$ exact [chart] and the network behaviour of complex (not real) quantum theory: vacuum dispersion, $S\neq2\sqrt2$, or non-quantum network behaviour each falsify. -/136theorem p22054 : (∀ {p : Nat} [FRC.Pos p] {ζ : FRC.Shell p}, ζ ^ (4 : Nat) = (-1 : FRC.Shell p) → (ζ + ζ ^ (7 : Nat)) * (ζ + ζ ^ (7 : Nat)) = (2 : FRC.Shell p)) ∧ (∀ {q : Nat} [FRC.Pos q] {ζ : FRC.Shell q}, ζ ^ (4 : Nat) = (-1 : FRC.Shell q) → (2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat)) * ((2 : FRC.Shell q) * (ζ + ζ ^ (7 : Nat))) = (8 : FRC.Shell q)) ∧ ∀ {a b T : Nat}, (0 : Nat) < a → (0 : Nat) < b → (0 : Nat) < T → T % a = (0 : Nat) → T % b = (0 : Nat) → (∀ (t : Nat), (0 : Nat) < t → t < T → ¬(t % a = (0 : Nat) ∧ t % b = (0 : Nat))) → ∃ g, g ≤ a ∧ (0 : Nat) < g ∧ g * T = a * b ∧ a % g = (0 : Nat) ∧ b % g = (0 : Nat) ∧ (∀ (e : Nat), (0 : Nat) < e → a % e = (0 : Nat) → b % e = (0 : Nat) → g % e = (0 : Nat)) ∧ ∀ (x y x' y' : Nat), x < a → y < b → x' < a → y' < b → ((∃ t, t < T ∧ (x + t) % a = x' ∧ (y + t) % b = y') ↔ (x + y') % g = (x' + y) % g) :=137  And.intro @FRC.Shell.Prime.tsirelson (And.intro @FRC.Composite.singlet_square (@FRC.Quantum.pair_offset))138/-- p22055 — 22:P4. No vacuum dispersion at any sub-horizon order (the finite double cover accumulates nothing): the gamma-ray-burst time-of-flight bounds leave the framework untouched. -/139theorem p22055 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {h : FRC.Shell p}, h * h = (-1 : FRC.Shell p) → (∀ (x : FRC.Shell p), x ≠ (0 : FRC.Shell p) → (x ^ (p + (1 : Nat)) = (1 : FRC.Shell p) ↔ x = (1 : FRC.Shell p) ∨ x = (-1 : FRC.Shell p))) ∧ (∀ (x : FRC.Shell p), x ≠ (0 : FRC.Shell p) → (x ^ ((2 : Nat) * (p + (1 : Nat))) = (1 : FRC.Shell p) ↔ x = (1 : FRC.Shell p) ∨ x = (-1 : FRC.Shell p) ∨ x = h ∨ x = -h)) ∧ h ^ (p + (1 : Nat)) = (-1 : FRC.Shell p)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Nat.isPrime p → ∀ {κ : Nat}, p = (4 : Nat) * κ + (1 : Nat) → (¬∃ y, y * y = ν) → ∀ (ζ : FRC.Extension.Ext p ν), ζ.norm = (1 : FRC.Shell p) → ζ ^ (p + (1 : Nat)) = (1 : FRC.Extension.Ext p ν) → (∀ (l : Nat), (0 : Nat) < l → l < p + (1 : Nat) → ζ ^ l ≠ (1 : FRC.Extension.Ext p ν)) → ζ ^ ((2 : Nat) * κ + (1 : Nat)) = (-1 : FRC.Extension.Ext p ν)) ∧ ∀ {q : Nat} [FRC.Pos q] {ν : FRC.Shell q} (z : FRC.Extension.Ext q ν), z.norm = (1 : FRC.Shell q) → z * z.conj = (1 : FRC.Extension.Ext q ν) :=140  And.intro @FRC.Subject.channel (And.intro @FRC.Subject.horizon_generator (@FRC.Observation.torus_conj_inv))141/-- p22056 — 22:P5. Quantum computation succeeds as standard quantum mechanics prescribes at every accessible depth; the first deviation, if any, is quantised at the unit-core ceiling $k^*=408$ ($204$ for $\sqrt\Omega$) [chart], not gradual. -/142theorem p22056 : (∀ {k k' : Nat}, k ≤ k' → FRC.Interference.tallyNorm k ≤ FRC.Interference.tallyNorm k') ∧ ((∀ (k : Nat), FRC.Interference.tallyNorm k < (641 : Nat) ↔ k ≤ (8 : Nat)) ∧ ∀ (k : Nat), (8 : Nat) * FRC.Interference.tallyNorm k < (641 : Nat) ↔ k ≤ (6 : Nat)) ∧ ∀ {q : Nat} [FRC.Pos q] {i : FRC.Shell q}, i * i = (-1 : FRC.Shell q) → ∀ (m : Nat), ((1 : FRC.Shell q) + i) ^ ((2 : Nat) * m) = FRC.Shell.ofNat ((2 : Nat) ^ m) * i ^ m :=143  And.intro @FRC.Interference.tally_norm_mono (And.intro @FRC.Interference.ceiling_641 (@FRC.Interference.hadamard_even))144-- end keys145146end FRC.Ledger147