import FrcCore.Theme.Extension
import FrcCore.Theme.Tally
import FrcCore.Theme.Field
import FrcCore.Theme.Subject
import FrcCore.Theme.Quantum
import FrcCore.Theme.Observation
import FrcCore.Theme.Interference
import FrcCore.Theme.Composite

/-!
# FrcCore.Keys.Quantum — the keyed theorems of the quantum theme (ledger migration, task LM19)

One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem
that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration
`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).
-/

namespace FRC.Ledger

-- Keys of the quantum theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)
/-- 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). -/
theorem 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) :=
  And.intro @FRC.Quantum.joint_recurrence (And.intro @FRC.Quantum.joint_least (And.intro @FRC.Quantum.pair_offset (@FRC.Quantum.dephasing)))
/-- 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. -/
theorem 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) :=
  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)))))
/-- 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). -/
theorem 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 ν) :=
  And.intro @FRC.Subject.channel (And.intro @FRC.Subject.horizon_generator (@FRC.Observation.torus_conj_inv))
/-- 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. -/
theorem 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 :=
  And.intro @FRC.Observation.power_maps (And.intro @FRC.Observation.roots_of_order (@FRC.Observation.character_is_power_map))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.stationary (@FRC.Observation.stationary_modes)
/-- 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. -/
theorem 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) } :=
  And.intro @FRC.Observation.orthogonality (And.intro @FRC.Observation.parseval (And.intro @FRC.Extension.Tally.fourier_inversion (@FRC.Extension.Tally.dft_det)))
/-- 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$. -/
theorem 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) :=
  @FRC.Observation.selection
/-- p22021 — 22:C5. The L\"uders update is projection, $\Pi^2=d\,\Pi$, so an immediately repeated measurement returns the same outcome. -/
theorem 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)) :=
  @FRC.Observation.lueders
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.frobenius_unique (And.intro @FRC.Observation.torus_conj_inv (@FRC.Observation.exponent_negation))
/-- 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]$. -/
theorem 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) :=
  And.intro @FRC.Observation.pair_count (And.intro @FRC.Observation.pure_winding_weight (And.intro @FRC.Observation.parseval (@FRC.Quantum.dephasing)))
/-- p22024 — 22:C8. Sorkin nullity: $I_k=0$ for every $k\ge3$, exactly, on every channel and outcome, with $I_2$ generically nonzero. -/
theorem 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) :=
  And.intro @FRC.Interference.sorkin_hierarchy (And.intro @FRC.Interference.sorkin_second (@FRC.Interference.sorkin_second_witness))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.reduce_add (And.intro @FRC.Observation.reduce_mul (@FRC.Observation.reduce_wrap))
set_option linter.defProp false in
/-- 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. -/
def 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))))))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.shared_core (@FRC.Observation.no_quarter_turn)
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Interference.hadamard_even (And.intro @FRC.Interference.hadamard_odd (And.intro @FRC.Interference.tally_norm_mono (@FRC.Interference.ceiling_641)))
/-- 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). -/
theorem 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) :=
  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))))
/-- p22032 — 22:C16. Qubits from doublets: the forced readout is $\sigma_x$ through the relation $v^{\,8}=-1$. -/
theorem 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) :=
  And.intro @FRC.Composite.half_turn_sixteen (And.intro @FRC.Composite.doublet_readout (@FRC.Composite.carrier_641))
/-- 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. -/
theorem 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) :=
  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))))
/-- p22034 — 22:C18. The network table is the complex-quantum table, and the Bell-state measurement is the offset readout. -/
theorem 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) :=
  And.intro @FRC.Quantum.pair_offset (@FRC.Composite.cluster_offset)
/-- 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$. -/
theorem 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) :=
  And.intro @FRC.Composite.channel_complementarity (@FRC.Composite.channel_product_at_zero)
/-- p22036 — 22:C20. No spontaneous collapse; the dilation floor dephases with an exact revival $V(n)=1$. -/
theorem 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) :=
  And.intro @FRC.Composite.drive_norm (And.intro @FRC.Composite.revival (@FRC.Quantum.joint_recurrence))
/-- 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. -/
theorem 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 :=
  And.intro @FRC.Composite.branch_phase (And.intro @FRC.Composite.pair_product (And.intro @FRC.Composite.spread_cancels (@FRC.Composite.channel_assembly)))
/-- p22038 — 22:C22. The two scaling laws and the exact equivalence-principle null: coherent $m^2$ against incoherent $m$, $\eta=0$. -/
theorem 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) :=
  And.intro @FRC.Composite.field_linear (And.intro @FRC.Composite.eta_zero (And.intro @FRC.Composite.locked_norm (@FRC.Composite.spread_average)))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Composite.joint_refinement (And.intro @FRC.Composite.order_independence (@FRC.Observation.selection))
/-- 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). -/
theorem 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) :=
  And.intro @FRC.Observation.classicality_index (And.intro @FRC.Observation.selection (@FRC.Composite.carrier_421))
/-- 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]. -/
theorem 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) :=
  And.intro @FRC.Shell.Prime.tsirelson (@FRC.Composite.singlet_square)
/-- 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. -/
theorem 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) :=
  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))))
/-- 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}). -/
theorem 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)) :=
  And.intro @FRC.Observation.transport_trichotomy (@FRC.Observation.transport_cases)
set_option linter.defProp false in
/-- 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). -/
def 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)))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.shared_core (@FRC.Observation.no_quarter_turn)
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.orthogonality (@FRC.Observation.selection)
/-- 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. -/
theorem 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)) :=
  And.intro @FRC.Composite.joint_refinement (And.intro @FRC.Composite.order_independence (@FRC.Observation.lueders))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Observation.classicality_index (And.intro @FRC.Observation.selection (@FRC.Composite.carrier_421))
set_option linter.defProp false in
/-- 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}). -/
def 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)))
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Shell.Prime.tsirelson (@FRC.Composite.singlet_square)
/-- 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. -/
theorem 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 :=
  And.intro @FRC.Interference.sorkin_hierarchy (@FRC.Observation.wrap_quantised)
/-- 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. -/
theorem 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 :=
  And.intro @FRC.Composite.channel_complementarity (And.intro @FRC.Composite.branch_phase (@FRC.Composite.channel_assembly))
/-- 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. -/
theorem 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 :=
  And.intro @FRC.Interference.sorkin_hierarchy (@FRC.Observation.wrap_quantised)
/-- 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. -/
theorem 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) :=
  And.intro @FRC.Shell.Prime.tsirelson (And.intro @FRC.Composite.singlet_square (@FRC.Quantum.pair_offset))
/-- 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. -/
theorem 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 ν) :=
  And.intro @FRC.Subject.channel (And.intro @FRC.Subject.horizon_generator (@FRC.Observation.torus_conj_inv))
/-- 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. -/
theorem 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 :=
  And.intro @FRC.Interference.tally_norm_mono (And.intro @FRC.Interference.ceiling_641 (@FRC.Interference.hadamard_even))
-- end keys

end FRC.Ledger