Keys/Subject.lean — FrcCore

1import FrcCore.Cycle2import FrcCore.FrameCore3import FrcCore.Theme.Quadratic4import FrcCore.Theme.Projective5import FrcCore.Theme.Field6import FrcCore.Theme.Subject7import FrcCore.Theme.Pair8import FrcCore.Theme.Hopf910/-!11# FrcCore.Keys.Subject — the keyed theorems of the subject 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 subject theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)21/-- p00021 — 00:C1. The frame, Subject-only: $(\chron;0,1,\gen)$, origin, unit and the drive $x\mapsto gx$ (A6). Shell data, capacity-first: $\kap $ primitive, $\p =4\kap +1$, $\im=-\gen^\kap $ (C7), $\pi=2\kap $, $e=\gen^{\,\im}$; $\gen$ the one nonsquare frame datum (C3, C8). Exponents of $\gen$ are taken in $\Zp$, a residue in an exponent standing for its lift $\iota:\F_\p\to\{0,\dots,\p-1\}$. The web closes on every shell: $2\pi\equiv-1$, $\gen^{\,\pi}\equiv-1$, $-\pi=2^{-1}$ (N2). -/22theorem p00021 : ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.ofNat ((2 : Nat) * FRC.Shell.Frame.halfPeriod κ) = (-1 : FRC.Shell p) ∧ g ^ FRC.Shell.Frame.halfPeriod κ = (-1 : FRC.Shell p) ∧ -FRC.Shell.ofNat (FRC.Shell.Frame.halfPeriod κ) * (2 : FRC.Shell p) = (1 : FRC.Shell p) ∧ FRC.Shell.Frame.quarterTurn g κ * FRC.Shell.Frame.quarterTurn g κ = (-1 : FRC.Shell p) ∧ (∃ y, y * y = (0 : FRC.Shell p)) ∧ (∃ y, y * y = (1 : FRC.Shell p)) ∧ ¬∃ y, y * y = g :=23  @FRC.Subject.frame_web24/-- p00028 — 00:C8. For a primitive drive the squares are $\langle \gen^2\rangle$: a residue's quadratic class is its drive-step parity. Registered transport is even, the one-way multiplier $\gen$ odd, so the one-way speed is gauge and the two-way constant invariant. $[c^2]$ is even iff $\dS$ is even, a relation certified by the unit realisation (D7). The Tsirelson $\sqrt2=\zeta_8+\zeta_8^{-1}$ is its two-way symmetrisation. -/25theorem p00028 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (m : Nat), (∃ y, y * y = g ^ m) ↔ m % (2 : Nat) = (0 : Nat)) ∧ (¬∃ y, y * y = g) ∧ (∀ (y : FRC.Shell p), g * y = (1 : FRC.Shell p) → ¬∃ r, r * r = y) ∧ ∃ y, y * y = g * g) ∧ (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {S : Nat}, p = (4 : Nat) * S + (1 : Nat) → ∀ (h : FRC.Shell p), (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → ((∃ c, c * c = h) ↔ S % (2 : Nat) = (0 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {ζ : FRC.Shell p}, ζ ^ (4 : Nat) = (-1 : FRC.Shell p) → (ζ + ζ ^ (7 : Nat)) * (ζ + ζ ^ (7 : Nat)) = (2 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (c : FRC.Shell p) (z : FRC.Extension.Ext p ν), (FRC.Extension.Ext.ofShell c * z).norm = c * c * z.norm :=26  And.intro @FRC.Subject.square_class (And.intro @FRC.Subject.half_class (And.intro @FRC.Shell.Prime.tsirelson (@FRC.Extension.Ext.norm_scale)))27/-- p00034 — 00:C14. \textbf{The quarter-turn is the odd member of the $\pm\sqrt{-1}$ pair}: the two representatives have opposite integer parity (distinct from chronon parity, C8), and $e^{\,\im\pi}:=\gen^{\,2\kap\,\iota(\im)^{2}}\equiv(-1)^{\iota(\im)}$ (the lift $\iota$ of C1), so $e^{\,\im\pi}\equiv-1$ holds exactly on the odd member. The conjugate chart toggles it: the parity names the matter--antimatter gauge (C7), and the selection is generator-independent within the chirality. -/28theorem p00034 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (i : Nat), (g ^ i) ^ (i * ((2 : Nat) * κ)) = if i % (2 : Nat) = (0 : Nat) then (1 : FRC.Shell p) else (-1 : FRC.Shell p)) ∧ (∀ (h : FRC.Shell p), h * h = (-1 : FRC.Shell p) → (h.val % (2 : Nat) = (0 : Nat) ↔ ¬(-h).val % (2 : Nat) = (0 : Nat))) ∧ (∀ (h : FRC.Shell p), h * h = (-1 : FRC.Shell p) → ((g ^ h.val) ^ (h.val * ((2 : Nat) * κ)) = (-1 : FRC.Shell p) ↔ h.val % (2 : Nat) = (1 : Nat))) ∧ (∀ (y : FRC.Shell p), g * y = (1 : FRC.Shell p) → FRC.Shell.Frame p κ y ∧ FRC.Shell.Frame.quarterTurn y κ = -FRC.Shell.Frame.quarterTurn g κ) ∧ ∀ (g' : FRC.Shell p), FRC.Shell.Frame p κ g' → ∃ u, u < p - (1 : Nat) ∧ g ^ u = g' ∧ (u % (4 : Nat) = (1 : Nat) ∨ u % (4 : Nat) = (3 : Nat)) ∧ (u % (4 : Nat) = (1 : Nat) → FRC.Shell.Frame.quarterTurn g' κ = FRC.Shell.Frame.quarterTurn g κ) ∧ (u % (4 : Nat) = (3 : Nat) → FRC.Shell.Frame.quarterTurn g' κ = -FRC.Shell.Frame.quarterTurn g κ) ∧ ((FRC.Shell.Frame.quarterTurn g' κ).val % (2 : Nat) = (FRC.Shell.Frame.quarterTurn g κ).val % (2 : Nat) ↔ u % (4 : Nat) = (1 : Nat))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (i : Nat), (g ^ i) ^ (i * ((2 : Nat) * κ)) = if i % (2 : Nat) = (0 : Nat) then (1 : FRC.Shell p) else (-1 : FRC.Shell p) :=29  And.intro @FRC.Subject.quarter_turn_odd (@FRC.Shell.Frame.euler_identity)30/-- p00040 — 00:C20. \textbf{The mass--energy channel}: the winding sector $C_{\p -1}$ meets the boost base $C_{\p +1}$ in the sign alone and the spinor cover $C_{2(\p +1)}$ in exactly $Q_4$, every $\p =4\kap +1$; the quarter is spinorial, $N(\im)=\im^{2}=-1$: the mass transport crosses the sheet; mass phase $=$ winding rate, one $Q_4$ datum (D2); Carrier instance $78^{58}=89=h$ on $\Om =233$ (38:A4). -/31theorem p00040 : (∀ {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)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (58 : Nat) = (89 : FRC.Shell (233 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat)) :=32  And.intro @FRC.Subject.channel (@FRC.Subject.channel_233)33/-- p00139 — 00:C25. For $w^2=\nu$ a nonsquare, the torsor map $\mathbb{P}^1(\F_\p)\to C_{\p +1}$, $P\mapsto u_P/\bar u_P$ with $u_P$ the unique boost carrying $0$ to $P$, is equivariant and sends the origin to $1$ and the horizon $[1{:}0]$ to $-1=\zeta^{(\p +1)/2}$. Origin and horizon are the sign pair $C_{\p -1}\cap C_{\p +1}$ (C20), exchanged by the torus's unique involution $q\mapsto\nu/q$. On the additive cycle the antipode is the seam $\p/2$ (1:Z1, 1:Z2). -/34theorem p00139 : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Nat.isPrime p → ∀ {κ : Nat}, p = (4 : Nat) * κ + (1 : Nat) → (¬∃ y, y * y = ν) → (∀ (x y : FRC.Shell p), x ≠ (0 : FRC.Shell p) ∨ y ≠ (0 : FRC.Shell p) → (FRC.Subject.dir ν x y).norm ≠ (0 : FRC.Shell p)) ∧ (∀ (v : FRC.Extension.Ext p ν) (x y : FRC.Shell p), v * FRC.Subject.dir ν x y = FRC.Subject.dir ν (v.re * x + ν * (v.im * y)) (v.re * y + v.im * x)) ∧ (∀ (u : FRC.Extension.Ext p ν), u.norm ≠ (0 : FRC.Shell p) → (FRC.Subject.ratio u).norm = (1 : FRC.Shell p)) ∧ (∀ (c : FRC.Shell p) (u : FRC.Extension.Ext p ν), c ≠ (0 : FRC.Shell p) → FRC.Subject.ratio (FRC.Extension.Ext.ofShell c * u) = FRC.Subject.ratio u) ∧ (∀ (u v : FRC.Extension.Ext p ν), FRC.Subject.ratio (v * u) = FRC.Subject.ratio v * FRC.Subject.ratio u) ∧ (∀ (x y x' y' : FRC.Shell p), x ≠ (0 : FRC.Shell p) ∨ y ≠ (0 : FRC.Shell p) → x' ≠ (0 : FRC.Shell p) ∨ y' ≠ (0 : FRC.Shell p) → (FRC.Subject.ratio (FRC.Subject.dir ν x y) = FRC.Subject.ratio (FRC.Subject.dir ν x' y') ↔ x * y' = x' * y)) ∧ (∀ (z : FRC.Extension.Ext p ν), z.norm = (1 : FRC.Shell p) → ∃ x y, (x ≠ (0 : FRC.Shell p) ∨ y ≠ (0 : FRC.Shell p)) ∧ FRC.Subject.ratio (FRC.Subject.dir ν x y) = z) ∧ FRC.Subject.ratio (FRC.Subject.dir ν (0 : FRC.Shell p) (1 : FRC.Shell p)) = (1 : FRC.Extension.Ext p ν) ∧ FRC.Subject.ratio (FRC.Subject.dir ν (1 : FRC.Shell p) (0 : FRC.Shell p)) = (-1 : FRC.Extension.Ext p ν) ∧ (∀ (z : FRC.Extension.Ext p ν), z.norm = (1 : FRC.Shell p) → z * z = (1 : FRC.Extension.Ext p ν) → z = (1 : FRC.Extension.Ext p ν) ∨ z = (-1 : FRC.Extension.Ext p ν)) ∧ (∀ (z : FRC.Extension.Ext p ν), z.im = (0 : FRC.Shell p) → (z.norm = (1 : FRC.Shell p) ↔ z = (1 : FRC.Extension.Ext p ν) ∨ z = (-1 : FRC.Extension.Ext p ν))) ∧ (∀ (v : FRC.Extension.Ext p ν), (v * v).im = (0 : FRC.Shell p) → v.im ≠ (0 : FRC.Shell p) → v.re = (0 : FRC.Shell p)) ∧ (∀ (x y : FRC.Shell p), FRC.Extension.Ext.w * FRC.Subject.dir ν x y = FRC.Subject.dir ν (ν * y) x) ∧ (∀ (s : FRC.Shell p), (2 : FRC.Shell p) * s = (0 : FRC.Shell p) → s = (0 : FRC.Shell p)) ∧ (2 : FRC.Shell p) * FRC.Shell.ofNat ((2 : Nat) * κ + (1 : Nat)) = (1 : FRC.Shell p) ∧ FRC.Shell.ofNat ((2 : Nat) * κ) + FRC.Shell.ofNat ((2 : Nat) * κ + (1 : Nat)) = (0 : 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 ν)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Nat.isPrime p → (¬∃ y, y * y = ν) → ∀ (v : FRC.Extension.Ext p ν) (c x y : FRC.Shell p), v * FRC.Subject.dir ν (0 : FRC.Shell p) (1 : FRC.Shell p) = FRC.Extension.Ext.ofShell c * FRC.Subject.dir ν x y → v = FRC.Extension.Ext.ofShell (c * FRC.Subject.inv ν) * FRC.Subject.dir ν x y :=35  And.intro @FRC.Subject.horizon_antipode (And.intro @FRC.Subject.horizon_generator (@FRC.Subject.boost_unique))36/-- p00150 — 00:C3. The drive fixes a Lorentzian time axis, causal order is algebraic, the split and non-split tori the two signatures. The signature is the square class of the temporal coefficient $\nu=\gen$ (C1); in $\F_\p$, $\nu=2^{-1}\cdot(2\gen)$, both classes fixed by the parity of $\kap$ (8:B3). In the Carrier $c^2=2^{-1}$ is a square (C8, D7), and $\eta_{00}=-c^2$ is a chart artifact. -/37theorem p00150 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (¬∃ y, y * y = g) ∧ (∀ (ν : FRC.Shell p), (∃ t x, t ≠ (0 : FRC.Shell p) ∧ x * x = ν * (t * t)) ↔ ∃ w, w * w = ν) ∧ ∀ (h : FRC.Shell p), (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → h * ((2 : FRC.Shell p) * g) = g ∧ ((∃ r, r * r = h) ↔ κ % (2 : Nat) = (0 : Nat)) ∧ ((∃ r, r * r = (2 : FRC.Shell p) * g) ↔ κ % (2 : Nat) = (1 : Nat))) ∧ ∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {S : Nat}, p = (4 : Nat) * S + (1 : Nat) → ∀ (h : FRC.Shell p), (2 : FRC.Shell p) * h = (1 : FRC.Shell p) → ((∃ c, c * c = h) ↔ S % (2 : Nat) = (0 : Nat)) :=38  And.intro @FRC.Subject.signature (@FRC.Subject.half_class)39/-- p00151 — 00:C16. \textbf{The spinor dichotomy}: $\kap$ odd $\Leftrightarrow$ $C_{\p-1}\cong C_4\times C_\kap$ $\Leftrightarrow$ $v_2(\p-1)=2$ $\Leftrightarrow$ $3\kap r+4s\equiv1\ (\mathrm{mod}\ 4\kap)$ is solvable: the spinor class. Shell and Carrier share the $2$-part $C_{2^m}$, $m=\min(v_2(\p-1),v_2(\Om-1))$, and the shell closes on a cover of degree $2^{v_2(\Om-1)-m}$; the shared order times the cover degree is the Carrier's $2$-part, $8$ exactly when $\dS\equiv2\ (\mathrm{mod}\ 4)$. The midpoint event of a $\kap$-odd shell: 38:C14. -/40theorem p00151 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (κ % (2 : Nat) = (1 : Nat) ↔ (p - (1 : Nat)) % (8 : Nat) ≠ (0 : Nat)) ∧ (κ % (2 : Nat) = (1 : Nat) ↔ ∀ (r s r' s' : Nat), r < (4 : Nat) → s < κ → r' < (4 : Nat) → s' < κ → FRC.Shell.Frame.quarterTurn g κ ^ r * (g ^ (4 : Nat)) ^ s = FRC.Shell.Frame.quarterTurn g κ ^ r' * (g ^ (4 : Nat)) ^ s' → r = r' ∧ s = s') ∧ (κ % (2 : Nat) = (1 : Nat) → ∀ (x : FRC.Shell p), x ≠ (0 : FRC.Shell p) → ∃ r s, r < (4 : Nat) ∧ s < κ ∧ FRC.Shell.Frame.quarterTurn g κ ^ r * (g ^ (4 : Nat)) ^ s = x) ∧ (κ % (2 : Nat) = (1 : Nat) ↔ ∃ r s, r < (4 : Nat) ∧ s < κ ∧ ((3 : Nat) * κ * r + (4 : Nat) * s) % ((4 : Nat) * κ) = (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → κ % (2 : Nat) = (0 : Nat) → ∀ (φ : FRC.Shell p → Nat × Nat), (∀ (x y : FRC.Shell p), x ≠ (0 : FRC.Shell p) → y ≠ (0 : FRC.Shell p) → φ (x * y) = (((φ x).fst + (φ y).fst) % (4 : Nat), ((φ x).snd + (φ y).snd) % κ)) → ¬∀ (x y : FRC.Shell p), x ≠ (0 : FRC.Shell p) → y ≠ (0 : FRC.Shell p) → φ x = φ y → x = y) ∧ (∀ (a b u w m : Nat), u % (2 : Nat) = (1 : Nat) → w % (2 : Nat) = (1 : Nat) → m ≤ a → m ≤ b → m = a ∨ m = b → (2 : Nat) ^ m ∣ (2 : Nat) ^ a * u ∧ (2 : Nat) ^ m ∣ (2 : Nat) ^ b * w ∧ ¬((2 : Nat) ^ (m + (1 : Nat)) ∣ (2 : Nat) ^ a * u ∧ (2 : Nat) ^ (m + (1 : Nat)) ∣ (2 : Nat) ^ b * w) ∧ (2 : Nat) ^ m * (2 : Nat) ^ (b - m) = (2 : Nat) ^ b) ∧ ∀ (S b w : Nat), w % (2 : Nat) = (1 : Nat) → (4 : Nat) * S = (2 : Nat) ^ b * w → ((2 : Nat) ^ b = (8 : Nat) ↔ S % (4 : Nat) = (2 : Nat)) :=41  And.intro @FRC.Subject.spinor (And.intro @FRC.Subject.no_iso (@FRC.Subject.two_part))42/-- p38001 — 38:A1. The pair: $\p=13$, $\kap=3$, $\Om=233$, $\dS=58$; $\gen=2$, $\im=5=-\gen^{\kap}$. -/43theorem p38001 : FRC.Shell.Frame (13 : Nat) (3 : Nat) (2 : FRC.Shell (13 : Nat)) ∧ (13 : Nat) = (4 : Nat) * (3 : Nat) + (1 : Nat) ∧ (233 : Nat) = (4 : Nat) * (58 : Nat) + (1 : Nat) ∧ (12 : Nat) = (4 : Nat) * (3 : Nat) ∧ (58 : Nat) % (4 : Nat) = (2 : Nat) ∧ (58 : Nat) % (3 : Nat) = (1 : Nat) ∧ (13 : Nat) * (13 : Nat) < (233 : Nat) ∧ (5 : FRC.Shell (13 : Nat)) = -(2 : FRC.Shell (13 : Nat)) ^ (3 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (4 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ (3 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (2 : FRC.Shell (13 : Nat)) ∧ (3 : FRC.Shell (13 : Nat)) ^ (3 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) ^ (4 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (12 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (6 : Nat) = (-1 : FRC.Shell (13 : Nat)) ∧ (4 : Nat) * (1 : Nat) = (3 : Nat) * (1 : Nat) + (1 : Nat) :=44  And.intro @FRC.Pair.pair_frame (@FRC.Pair.pair_register)45/-- p38002 — 38:A2. The tower identity: $C_{12}=C_{4}\times C_{3}$, $\gen=3\cdot5=2$; unit exponents exactly at $\kap=3$; general form $4a-\kap b\equiv1\pmod{4\kap}$, solvable for every odd $\kap$ (Theorem~\ref{th:channel} inside the Subject). -/46theorem p38002 : (∀ (κ : Nat), κ % (2 : Nat) = (1 : Nat) → ∃ a b, (4 : Nat) * a = κ * b + (1 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (κ % (2 : Nat) = (1 : Nat) ↔ (p - (1 : Nat)) % (8 : Nat) ≠ (0 : Nat)) ∧ (κ % (2 : Nat) = (1 : Nat) ↔ ∀ (r s r' s' : Nat), r < (4 : Nat) → s < κ → r' < (4 : Nat) → s' < κ → FRC.Shell.Frame.quarterTurn g κ ^ r * (g ^ (4 : Nat)) ^ s = FRC.Shell.Frame.quarterTurn g κ ^ r' * (g ^ (4 : Nat)) ^ s' → r = r' ∧ s = s') ∧ (κ % (2 : Nat) = (1 : Nat) → ∀ (x : FRC.Shell p), x ≠ (0 : FRC.Shell p) → ∃ r s, r < (4 : Nat) ∧ s < κ ∧ FRC.Shell.Frame.quarterTurn g κ ^ r * (g ^ (4 : Nat)) ^ s = x) ∧ (κ % (2 : Nat) = (1 : Nat) ↔ ∃ r s, r < (4 : Nat) ∧ s < κ ∧ ((3 : Nat) * κ * r + (4 : Nat) * s) % ((4 : Nat) * κ) = (1 : Nat))) ∧ ((∀ (a b u w m : Nat), u % (2 : Nat) = (1 : Nat) → w % (2 : Nat) = (1 : Nat) → m ≤ a → m ≤ b → m = a ∨ m = b → (2 : Nat) ^ m ∣ (2 : Nat) ^ a * u ∧ (2 : Nat) ^ m ∣ (2 : Nat) ^ b * w ∧ ¬((2 : Nat) ^ (m + (1 : Nat)) ∣ (2 : Nat) ^ a * u ∧ (2 : Nat) ^ (m + (1 : Nat)) ∣ (2 : Nat) ^ b * w) ∧ (2 : Nat) ^ m * (2 : Nat) ^ (b - m) = (2 : Nat) ^ b) ∧ ∀ (S b w : Nat), w % (2 : Nat) = (1 : Nat) → (4 : Nat) * S = (2 : Nat) ^ b * w → ((2 : Nat) ^ b = (8 : Nat) ↔ S % (4 : Nat) = (2 : Nat))) ∧ (13 : Nat) = (4 : Nat) * (3 : Nat) + (1 : Nat) ∧ (233 : Nat) = (4 : Nat) * (58 : Nat) + (1 : Nat) ∧ (12 : Nat) = (4 : Nat) * (3 : Nat) ∧ (58 : Nat) % (4 : Nat) = (2 : Nat) ∧ (58 : Nat) % (3 : Nat) = (1 : Nat) ∧ (13 : Nat) * (13 : Nat) < (233 : Nat) ∧ (5 : FRC.Shell (13 : Nat)) = -(2 : FRC.Shell (13 : Nat)) ^ (3 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (4 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ (3 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (2 : FRC.Shell (13 : Nat)) ∧ (3 : FRC.Shell (13 : Nat)) ^ (3 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) ^ (4 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (12 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (6 : Nat) = (-1 : FRC.Shell (13 : Nat)) ∧ (4 : Nat) * (1 : Nat) = (3 : Nat) * (1 : Nat) + (1 : Nat) :=47  And.intro @FRC.Pair.tower_solvable (And.intro @FRC.Subject.spinor (And.intro @FRC.Subject.two_part (@FRC.Pair.pair_register)))48/-- p38003 — 38:A3. The channel at the instance: $\gcd(12,14)=2$, $\gcd(12,28)=4$; $N(\im)=-1$ (Theorem~\ref{th:channel}). -/49theorem p38003 : (∀ {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)) ∧ (12 : Nat) % (2 : Nat) = (0 : Nat) ∧ (14 : Nat) % (2 : Nat) = (0 : Nat) ∧ (∀ (d : Nat), d < (15 : Nat) → (2 : Nat) < d → ¬((12 : Nat) % d = (0 : Nat) ∧ (14 : Nat) % d = (0 : Nat))) ∧ (12 : Nat) % (4 : Nat) = (0 : Nat) ∧ (28 : Nat) % (4 : Nat) = (0 : Nat) ∧ (∀ (d : Nat), d < (29 : Nat) → (4 : Nat) < d → ¬((12 : Nat) % d = (0 : Nat) ∧ (28 : Nat) % d = (0 : Nat))) ∧ (5 : FRC.Shell (13 : Nat)) * (5 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) ^ (13 : Nat) = (5 : FRC.Shell (13 : Nat)) :=50  And.intro @FRC.Subject.channel (@FRC.Pair.channel_instance)51/-- p38004 — 38:A4. The Carrier quarter roots, arithmetic: $78^{58}=89=h$, $h^{2}=-1$, $\hbar=144$, $\hbar h=1$, $\hbar+h=\Om$; octant $\zeta_{8}=97$, $\zeta_{8}^{2}=h$; $233=13^{2}+8^{2}$ with $h=13/8$, $\hbar=8/13$ on $\F_{233}$. -/52theorem p38004 : ((78 : FRC.Shell (233 : Nat)) ^ (58 : Nat) = (89 : FRC.Shell (233 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat))) ∧ FRC.Shell.Frame (233 : Nat) (58 : Nat) (78 : FRC.Shell (233 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (58 : Nat) = (89 : FRC.Shell (233 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat)) ∧ (144 : FRC.Shell (233 : Nat)) = (-89 : FRC.Shell (233 : Nat)) ∧ (144 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (1 : FRC.Shell (233 : Nat)) ∧ (144 : FRC.Shell (233 : Nat)) + (89 : FRC.Shell (233 : Nat)) = (0 : FRC.Shell (233 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (116 : Nat) = (-1 : FRC.Shell (233 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (232 : Nat) = (1 : FRC.Shell (233 : Nat)) ∧ (97 : FRC.Shell (233 : Nat)) ^ (2 : Nat) = (89 : FRC.Shell (233 : Nat)) ∧ (97 : FRC.Shell (233 : Nat)) ^ (4 : Nat) = (-1 : FRC.Shell (233 : Nat)) ∧ (97 : FRC.Shell (233 : Nat)) ^ (8 : Nat) = (1 : FRC.Shell (233 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (29 : Nat) = (97 : FRC.Shell (233 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (8 : FRC.Shell (233 : Nat)) = (13 : FRC.Shell (233 : Nat)) ∧ (144 : FRC.Shell (233 : Nat)) * (13 : FRC.Shell (233 : Nat)) = (8 : FRC.Shell (233 : Nat)) ∧ (233 : Nat) = (13 : Nat) * (13 : Nat) + (8 : Nat) * (8 : Nat) ∧ (233 : Nat) = (144 : Nat) + (89 : Nat) ∧ (144 : Nat) = (89 : Nat) + (55 : Nat) ∧ (89 : Nat) = (55 : Nat) + (34 : Nat) ∧ (13 : Nat) = (8 : Nat) + (5 : Nat) :=53  And.intro @FRC.Subject.channel_233 (And.intro @FRC.Pair.carrier_frame (@FRC.Pair.carrier_roots))54/-- p38006 — 38:A6. The FRC algebra half \cite{algebra}: $\tfrac12=7$, $-\tfrac12=6$; the seam between rows $6$ and $7$. -/55theorem p38006 : (∀ {p : Nat} [FRC.Pos p] {S : Nat}, p = (4 : Nat) * S + (1 : Nat) → (2 : FRC.Shell p) * FRC.Shell.ofNat ((2 : Nat) * S + (1 : Nat)) = (1 : FRC.Shell p)) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat)) ∧ (6 : FRC.Shell (13 : Nat)) = (-7 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) * (6 : FRC.Shell (13 : Nat)) = (-1 : FRC.Shell (13 : Nat)) ∧ (6 : Nat) * (2 : Nat) < (13 : Nat) ∧ (13 : Nat) < (7 : Nat) * (2 : Nat) :=56  And.intro @FRC.Shell.Prime.two_mul_chart_half (@FRC.Pair.half_instance)57/-- p38007 — 38:A7. The frame counts: $2184=156\times14=14\times13\times12$; the norm-one sphere is $\SL_{2}$ (its quaternion determinant), the spin cover of $\mathrm{PSL}_{2}$ ($1092$); $\SL_{2}$ obstructs at $-1$ (Theorem~\ref{th:hopf}). The elements counted are the frame moves of the Subject's chart, not registrations of the Carrier (00:C22). -/58theorem p38007 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν : FRC.Shell p}, (¬∃ y, y * y = ν) → (∀ (α β x y : FRC.Shell p), β ≠ (0 : FRC.Shell p) → x ≠ (0 : FRC.Shell p) ∨ y ≠ (0 : FRC.Shell p) → ¬FRC.Shell.Frame.PEq ((FRC.Shell.Frame.boost ν α β).act x y) (x, y)) ∧ (∀ (α β a b e l : FRC.Shell p), FRC.Shell.Frame.boost ν α β = FRC.Shell.Frame.M2.smul l (FRC.Shell.Frame.borel a b e) → β = (0 : FRC.Shell p)) ∧ (∀ (M : FRC.Shell.Frame.M2 p), M.det ≠ (0 : FRC.Shell p) → ∃ N a b e α β, N ≠ (0 : FRC.Shell p) ∧ a * e ≠ (0 : FRC.Shell p) ∧ (α ≠ (0 : FRC.Shell p) ∨ β ≠ (0 : FRC.Shell p)) ∧ FRC.Shell.Frame.M2.smul N M = (FRC.Shell.Frame.borel a b e).mul (FRC.Shell.Frame.boost ν α β)) ∧ (∀ (l a1 b1 e1 α1 β1 a2 b2 e2 α2 β2 : FRC.Shell p), l ≠ (0 : FRC.Shell p) → e2 ≠ (0 : FRC.Shell p) → α1 ≠ (0 : FRC.Shell p) ∨ β1 ≠ (0 : FRC.Shell p) → FRC.Shell.Frame.M2.smul l ((FRC.Shell.Frame.borel a1 b1 e1).mul (FRC.Shell.Frame.boost ν α1 β1)) = (FRC.Shell.Frame.borel a2 b2 e2).mul (FRC.Shell.Frame.boost ν α2 β2) → α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) ∧ (∀ (α β α' β' : FRC.Shell p), α ≠ (0 : FRC.Shell p) ∨ β ≠ (0 : FRC.Shell p) → α' ≠ (0 : FRC.Shell p) ∨ β' ≠ (0 : FRC.Shell p) → ((∃ μ, μ ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.boost ν α' β' = FRC.Shell.Frame.M2.smul μ (FRC.Shell.Frame.boost ν α β)) ↔ α * β' = α' * β)) ∧ FRC.Shell.Frame.natCount (fun x => True) p * FRC.Shell.Frame.natCount (fun b => b ≠ (0 : Nat)) p = p * (p - (1 : Nat)) ∧ FRC.Shell.Frame.boost ν (-1 : FRC.Shell p) (0 : FRC.Shell p) = FRC.Shell.Frame.borel (-1 : FRC.Shell p) (0 : FRC.Shell p) (-1 : FRC.Shell p) ∧ (-1 : FRC.Shell p) * (-1 : FRC.Shell p) + -(ν * ((0 : FRC.Shell p) * (0 : FRC.Shell p))) = (1 : FRC.Shell p) ∧ (-1 : FRC.Shell p) * (-1 : FRC.Shell p) = (1 : FRC.Shell p) ∧ (∀ (α β a b e : FRC.Shell p), FRC.Shell.Frame.boost ν α β = FRC.Shell.Frame.borel a b e → α * α + -(ν * (β * β)) = (1 : FRC.Shell p) → β = (0 : FRC.Shell p) ∧ (α = (1 : FRC.Shell p) ∨ α = (-1 : FRC.Shell p))) ∧ ∀ (M N : FRC.Shell.Frame.M2 p), (FRC.Shell.Frame.M2.smul (-1 : FRC.Shell p) M).mul (FRC.Shell.Frame.M2.smul (-1 : FRC.Shell p) N) = M.mul N) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (ν : FRC.Shell p), (∀ (a b e : FRC.Shell p), a * e ≠ (0 : FRC.Shell p) → ∃ i j, i < p ∧ j < p ∧ i ≠ (0 : Nat) ∧ ∃ l, l ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.M2.smul l (FRC.Shell.Frame.borel a b e) = FRC.Shell.Frame.borel (FRC.Shell.ofNat i) (FRC.Shell.ofNat j) (1 : FRC.Shell p)) ∧ (∀ (i j i' j' : Nat), i < p → j < p → i' < p → j' < p → ∀ (l : FRC.Shell p), FRC.Shell.Frame.M2.smul l (FRC.Shell.Frame.borel (FRC.Shell.ofNat i) (FRC.Shell.ofNat j) (1 : FRC.Shell p)) = FRC.Shell.Frame.borel (FRC.Shell.ofNat i') (FRC.Shell.ofNat j') (1 : FRC.Shell p) → i = i' ∧ j = j') ∧ FRC.Shell.Frame.natCount (fun x => True) p * FRC.Shell.Frame.natCount (fun b => b ≠ (0 : Nat)) p = p * (p - (1 : Nat)) ∧ (∀ (α β : FRC.Shell p), α ≠ (0 : FRC.Shell p) ∨ β ≠ (0 : FRC.Shell p) → (∃ i, i < p ∧ ∃ μ, μ ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.M2.smul μ (FRC.Shell.Frame.boost ν α β) = FRC.Shell.Frame.boost ν (FRC.Shell.ofNat i) (1 : FRC.Shell p)) ∨ ∃ μ, μ ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.M2.smul μ (FRC.Shell.Frame.boost ν α β) = FRC.Shell.Frame.boost ν (1 : FRC.Shell p) (0 : FRC.Shell p)) ∧ (∀ (i i' : Nat), i < p → i' < p → ∀ (μ : FRC.Shell p), FRC.Shell.Frame.M2.smul μ (FRC.Shell.Frame.boost ν (FRC.Shell.ofNat i) (1 : FRC.Shell p)) = FRC.Shell.Frame.boost ν (FRC.Shell.ofNat i') (1 : FRC.Shell p) → i = i') ∧ (∀ (i : Nat) (μ : FRC.Shell p), μ ≠ (0 : FRC.Shell p) → FRC.Shell.Frame.M2.smul μ (FRC.Shell.Frame.boost ν (FRC.Shell.ofNat i) (1 : FRC.Shell p)) ≠ FRC.Shell.Frame.boost ν (1 : FRC.Shell p) (0 : FRC.Shell p)) ∧ (∀ (i : Nat) (μ : FRC.Shell p), FRC.Shell.Frame.M2.smul μ (FRC.Shell.Frame.boost ν (1 : FRC.Shell p) (0 : FRC.Shell p)) ≠ FRC.Shell.Frame.boost ν (FRC.Shell.ofNat i) (1 : FRC.Shell p)) ∧ FRC.Shell.Frame.natCount (fun x => True) p + (1 : Nat) = p + (1 : Nat)) ∧ (∀ {p : Nat} [FRC.Pos p] {r : FRC.Shell p}, r * r = (-1 : FRC.Shell p) → ∀ (x y z w : FRC.Shell p), (FRC.Shell.Frame.quat r x y z w).det = x * x + y * y + z * z + w * w) ∧ (∀ {p : Nat} [FRC.Pos p], FRC.Shell.Frame.Fld p → ∀ {r h : FRC.Shell p}, r * r = (-1 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * h = (1 : FRC.Shell p) → (∀ (M : FRC.Shell.Frame.M2 p), FRC.Shell.Frame.quat r ((M.a + M.d) * h) ((M.a + -M.d) * (-r * h)) ((M.b + -M.c) * h) ((M.b + M.c) * (-r * h)) = M) ∧ ∀ (x y z w x' y' z' w' : FRC.Shell p), FRC.Shell.Frame.quat r x y z w = FRC.Shell.Frame.quat r x' y' z' w' → x = x' ∧ y = y' ∧ z = z' ∧ w = w') ∧ (14 : Nat) * (13 : Nat) * (12 : Nat) = (2184 : Nat) ∧ (2184 : Nat) = (156 : Nat) * (14 : Nat) ∧ (156 : Nat) = (13 : Nat) * (12 : Nat) ∧ (2 : Nat) * (1092 : Nat) = (2184 : Nat) ∧ (13 : Nat) * (13 : Nat) = (169 : Nat) ∧ (182 : Nat) = (13 : Nat) * (14 : Nat) ∧ (2184 : Nat) = (12 : Nat) * (182 : Nat) :=59  And.intro @FRC.Shell.Frame.hopf_section (And.intro @FRC.Shell.Frame.hopf_counts (And.intro @FRC.Shell.Frame.sphere_det (And.intro @FRC.Shell.Frame.quat_bijective (@FRC.Shell.Frame.frame_counts))))60/-- p38008 — 38:A8. The resolvable spectrum (Proposition~\ref{th:window}): symmetric heights, window $|\hat k|\le\kap\Leftrightarrow4|\hat k|<\p$, energy the magnitude with the sign as orientation, pairwise-exact conservation below capacity; instance window $\{0,\pm1,\pm2,\pm3\}$. -/61theorem p38008 : (∀ (κ k : Nat), (4 : Nat) * k < (4 : Nat) * κ + (1 : Nat) ↔ k ≤ κ) ∧ (∀ {κ k₁ k₂ : Nat}, (0 : Nat) < κ → k₁ ≤ κ → k₂ ≤ κ → k₁ + k₂ ≤ (2 : Nat) * κ ∧ (2 : Nat) * κ < (4 : Nat) * κ) ∧ (∀ (k : Nat), k < (13 : Nat) → ((4 : Nat) * k < (13 : Nat) ↔ k ≤ (3 : Nat))) ∧ (∀ (k₁ : Nat), k₁ < (4 : Nat) → ∀ (k₂ : Nat), k₂ < (4 : Nat) → k₁ + k₂ ≤ (6 : Nat)) ∧ (6 : Nat) < (12 : Nat) ∧ (2 : Nat) * (3 : Nat) - (1 : Nat) = (5 : Nat) ∧ (2 : Nat) * (3 : Nat) = (6 : Nat) :=62  And.intro @FRC.Pair.window (And.intro @FRC.Pair.window_sum (@FRC.Pair.window_instance))63/-- p38009 — 38:B1. The node field: $72=3\times2\times12$; retarded labels, one chronon of lookback per row. -/64theorem p38009 : (3 : Nat) * (2 : Nat) * (12 : Nat) = (72 : Nat) ∧ (∀ (k : Nat), k < (13 : Nat) → ∀ (t : Nat), t < (12 : Nat) → FRC.Pair.label k (t + (1 : Nat)) = (2 : FRC.Shell (13 : Nat)) * FRC.Pair.label k t ∧ FRC.Pair.label k (t + (12 : Nat)) = FRC.Pair.label k t) ∧ ∀ (k : Nat), k < (13 : Nat) → FRC.Pair.label k k = FRC.Shell.ofNat k :=65  @FRC.Pair.node_field66/-- p38010 — 38:B2. The radial ladder: shells at $R\sin(2a\pi/13)$ [chart]; capacity $4a<\p\Leftrightarrow a\le\kap$. -/67theorem p38010 : (∀ (κ k : Nat), (4 : Nat) * k < (4 : Nat) * κ + (1 : Nat) ↔ k ≤ κ) ∧ (∀ (k : Nat), k < (13 : Nat) → ((4 : Nat) * k < (13 : Nat) ↔ k ≤ (3 : Nat))) ∧ (∀ (k₁ : Nat), k₁ < (4 : Nat) → ∀ (k₂ : Nat), k₂ < (4 : Nat) → k₁ + k₂ ≤ (6 : Nat)) ∧ (6 : Nat) < (12 : Nat) ∧ (2 : Nat) * (3 : Nat) - (1 : Nat) = (5 : Nat) ∧ (2 : Nat) * (3 : Nat) = (6 : Nat) :=68  And.intro @FRC.Pair.window (@FRC.Pair.window_instance)69/-- p38011 — 38:B3. The mounting: $\times3=\gen^{4}$, $120^{\circ}=8$ steps, quarter-blind. -/70theorem p38011 : (2 : FRC.Shell (13 : Nat)) ^ (4 : Nat) = (3 : FRC.Shell (13 : Nat)) ∧ (3 : FRC.Shell (13 : Nat)) ^ (3 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (3 : FRC.Shell (13 : Nat)) ^ (2 : Nat) = (9 : FRC.Shell (13 : Nat)) ∧ (8 : Nat) * (15 : Nat) = (120 : Nat) ∧ (3 : Nat) * (8 : Nat) = (24 : Nat) ∧ (8 : Nat) % (4 : Nat) = (0 : Nat) ∧ (4 : Nat) % (4 : Nat) = (0 : Nat) ∧ (4 : Nat) % (3 : Nat) = (1 : Nat) ∧ (3 : Nat) * (48 : Nat) + (12 : Nat) = (156 : Nat) ∧ (156 : Nat) = (13 : Nat) * (12 : Nat) :=71  @FRC.Pair.mounting72/-- p38012 — 38:B4. The sky chronon: $\chron\bmod24$, the fibre product of $C_{12}$ and $C_{8}$ over $C_{4}$; antipodal at $+12$, closed at $+24$. -/73theorem p38012 : (FRC.Pair.count (fun n => n / (8 : Nat) % (4 : Nat) = n % (8 : Nat) % (4 : Nat)) (96 : Nat) = (24 : Nat) ∧ (12 : Nat) * (8 : Nat) = (24 : Nat) * (4 : Nat) ∧ (∀ (s : Nat), s < (24 : Nat) → ∀ (t : Nat), t < (24 : Nat) → s % (12 : Nat) = t % (12 : Nat) → s % (8 : Nat) = t % (8 : Nat) → s = t) ∧ (∀ (s : Nat), s < (24 : Nat) → (s + (12 : Nat)) % (24 : Nat) ≠ s ∧ (s + (12 : Nat) + (12 : Nat)) % (24 : Nat) = s) ∧ (232 : Nat) = (8 : Nat) * (29 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] (n : Nat), (0 : Nat) < n → ∀ (f : Nat → FRC.Shell p) (i : Nat), FRC.Cycle.cyc n f (i + n) = FRC.Cycle.cyc n f i :=74  And.intro @FRC.Pair.sky_chronon (@FRC.Cycle.cyc_add_n)75/-- p38013 — 38:B5. The recurrence data: $696=\dS\cdot12$, spinor $1392$ [proxy-chart]; the pair registers only the monotone dephasing. -/76theorem p38013 : (∀ {a m u v ℓ : Nat}, (0 : Nat) < m → ℓ = ((2 : Nat) * a + (1 : Nat)) * ((2 : Nat) * u + (1 : Nat)) → ℓ = m * ((2 : Nat) * v + (1 : Nat)) → (4 : Nat) * ℓ % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) ∧ (4 : Nat) * ℓ % ((8 : Nat) * m) = (4 : Nat) * m ∧ (8 : Nat) * ℓ % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) ∧ (8 : Nat) * ℓ % ((8 : Nat) * m) = (0 : Nat)) ∧ (696 : Nat) % (12 : Nat) = (0 : Nat) ∧ (696 : Nat) % (232 : Nat) = (0 : Nat) ∧ (696 : Nat) = (58 : Nat) * (12 : Nat) ∧ (696 : Nat) = (3 : Nat) * (232 : Nat) ∧ (1392 : Nat) = (2 : Nat) * (696 : Nat) ∧ (∀ (n : Nat), n < (696 : Nat) → (0 : Nat) < n → n % (12 : Nat) = (0 : Nat) → n % (232 : Nat) ≠ (0 : Nat)) ∧ (87 : Nat) = (3 : Nat) * (29 : Nat) ∧ (87 : Nat) = ((2 : Nat) * (1 : Nat) + (1 : Nat)) * ((2 : Nat) * (14 : Nat) + (1 : Nat)) ∧ (87 : Nat) = ((2 : Nat) * (14 : Nat) + (1 : Nat)) * ((2 : Nat) * (1 : Nat) + (1 : Nat)) ∧ (4 : Nat) * (87 : Nat) % (12 : Nat) = (0 : Nat) ∧ (4 : Nat) * (87 : Nat) % (232 : Nat) = (116 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) ^ (348 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (348 : Nat) = (-1 : FRC.Shell (233 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (696 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (696 : Nat) = (1 : FRC.Shell (233 : Nat)) :=77  And.intro @FRC.Pair.joint_cycle (@FRC.Pair.recurrence)78/-- p38015 — 38:B7. The frame leak: halved tick $\pi/232$; $\pi/2$ at the quarter station; continuous wrap on $C_{464}$ (Theorems~\ref{th:flip}, \ref{th:precession}). -/79theorem p38015 : (∀ {a m u v ℓ : Nat}, (0 : Nat) < m → ℓ = ((2 : Nat) * a + (1 : Nat)) * ((2 : Nat) * u + (1 : Nat)) → ℓ = m * ((2 : Nat) * v + (1 : Nat)) → (4 : Nat) * ℓ % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) ∧ (4 : Nat) * ℓ % ((8 : Nat) * m) = (4 : Nat) * m ∧ (8 : Nat) * ℓ % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) ∧ (8 : Nat) * ℓ % ((8 : Nat) * m) = (0 : Nat)) ∧ (∀ (m : Nat), (0 : Nat) < m → ∀ (k : Nat), FRC.Pair.tick ((2 : Nat) * m) k (k + m) = m) ∧ (58 : Nat) * (4 : Nat) = (232 : Nat) ∧ (58 : Nat) * (2 : Nat) = (116 : Nat) ∧ (232 : Nat) * (2 : Nat) = (464 : Nat) ∧ (61 : Nat) * ((12 : Nat) * (232 : Nat)) = (696 : Nat) * ((232 : Nat) + (12 : Nat)) ∧ (12 : Nat) * (232 : Nat) = (4 : Nat) * (696 : Nat) ∧ FRC.Pair.count (fun n => n / (232 : Nat) % (4 : Nat) = n % (232 : Nat) % (4 : Nat)) ((12 : Nat) * (232 : Nat)) = (696 : Nat) ∧ ∀ (t : Nat), t < (696 : Nat) → t % (12 : Nat) = (0 : Nat) → t % (232 : Nat) = (0 : Nat) → t = (0 : Nat) :=80  And.intro @FRC.Pair.joint_cycle (And.intro @FRC.Pair.tick_half (@FRC.Pair.frame_leak))81/-- p38016 — 38:C1. One retarded flow law: $\varphi(k)=-(b_{C}-k)\pi/116$; the Subject draws the gauge-free curl (Theorem~\ref{th:precession}). -/82theorem p38016 : (∀ (n : Nat), (0 : Nat) < n → ∀ (k : Nat), FRC.Pair.tick n k k = (0 : Nat)) ∧ (∀ (k : Nat), k < (232 : Nat) → FRC.Pair.tick (232 : Nat) k k = (0 : Nat) ∧ FRC.Pair.tick (232 : Nat) k ((116 : Nat) + k) = (116 : Nat)) ∧ (∀ (b : Nat), b < (232 : Nat) → ∀ (k : Nat), k < (13 : Nat) → (FRC.Pair.tick (232 : Nat) k b + b) % (232 : Nat) = k) ∧ (116 : Nat) = (232 / 2 : Nat) :=83  And.intro @FRC.Pair.tick_home (@FRC.Pair.flow_stations)84/-- p38018 — 38:C3. Ownership: the origin never dressed; rays anchor at the Observer at every clock state. -/85theorem p38018 : (∀ (d : Nat), d < (13 : Nat) → ((0 : Nat) < d ∧ ((4 : Nat) * d < (13 : Nat) ∨ (4 : Nat) * ((13 : Nat) - d) < (13 : Nat)) ↔ d = (1 : Nat) ∨ d = (2 : Nat) ∨ d = (3 : Nat) ∨ d = (10 : Nat) ∨ d = (11 : Nat) ∨ d = (12 : Nat))) ∧ ∀ (b : Nat), b < (232 : Nat) → (FRC.Pair.tick (232 : Nat) (0 : Nat) b + b) % (232 : Nat) = (0 : Nat) :=86  @FRC.Pair.ownership87/-- p38019 — 38:C4. The half-turn exact: odd chart, point reflection; the rim kiss (Theorem~\ref{th:channel}). -/88theorem p38019 : (∀ (m : Nat), (0 : Nat) < m → ∀ (x : Nat), (x + m + m) % ((2 : Nat) * m) = x % ((2 : Nat) * m) ∧ (x + ((2 : Nat) * m - x % ((2 : Nat) * m))) % ((2 : Nat) * m) = (0 : Nat) ∧ ((2 : Nat) * m - m % ((2 : Nat) * m)) % ((2 : Nat) * m) = m % ((2 : Nat) * m)) ∧ (∀ (x : Nat), x < (464 : Nat) → (x + (232 : Nat) + (232 : Nat)) % (464 : Nat) = x ∧ (x + ((464 : Nat) - x % (464 : Nat))) % (464 : Nat) = (0 : Nat)) ∧ ((464 : Nat) - (232 : Nat) % (464 : Nat)) % (464 : Nat) = (232 : Nat) :=89  And.intro @FRC.Pair.half_turn (@FRC.Pair.half_turn_instance)90/-- p38020 — 38:C5. The $C_{4}$ stations: parity image at $b_{C}=116+k$, home at $b_{C}=k$, gauge-free. -/91theorem p38020 : (∀ (m : Nat), (0 : Nat) < m → ∀ (k : Nat), FRC.Pair.tick ((2 : Nat) * m) k (k + m) = m) ∧ (∀ (k : Nat), k < (232 : Nat) → FRC.Pair.tick (232 : Nat) k k = (0 : Nat) ∧ FRC.Pair.tick (232 : Nat) k ((116 : Nat) + k) = (116 : Nat)) ∧ (∀ (b : Nat), b < (232 : Nat) → ∀ (k : Nat), k < (13 : Nat) → (FRC.Pair.tick (232 : Nat) k b + b) % (232 : Nat) = k) ∧ (116 : Nat) = (232 / 2 : Nat) :=92  And.intro @FRC.Pair.tick_half (@FRC.Pair.flow_stations)93/-- p38021 — 38:C6. The dilation instance $3/58$; the $(53,13)$ kill test (Theorems~\ref{th:precession}, \ref{th:channel}). -/94theorem p38021 : (3 : Nat) * (232 : Nat) = (58 : Nat) * (12 : Nat) ∧ (53 : Nat) = (4 : Nat) * (13 : Nat) + (1 : Nat) ∧ (157 : Nat) = (4 : Nat) * (39 : Nat) + (1 : Nat) ∧ (39 : Nat) % (4 : Nat) = (3 : Nat) ∧ (5 : FRC.Shell (157 : Nat)) ^ (78 : Nat) ≠ (1 : FRC.Shell (157 : Nat)) ∧ (5 : FRC.Shell (157 : Nat)) ^ (52 : Nat) ≠ (1 : FRC.Shell (157 : Nat)) ∧ (5 : FRC.Shell (157 : Nat)) ^ (12 : Nat) ≠ (1 : FRC.Shell (157 : Nat)) ∧ (5 : FRC.Shell (157 : Nat)) ^ (156 : Nat) = (1 : FRC.Shell (157 : Nat)) ∧ (5 : FRC.Shell (157 : Nat)) ^ (13 : Nat) = (22 : FRC.Shell (157 : Nat)) ∧ (13 : Nat) % (3 : Nat) ≠ (0 : Nat) ∧ (22 : FRC.Shell (157 : Nat)) ^ (9 : Nat) = (28 : FRC.Shell (157 : Nat)) ∧ (5 : FRC.Shell (157 : Nat)) ^ (39 : Nat) * (28 : FRC.Shell (157 : Nat)) = (1 : FRC.Shell (157 : Nat)) ∧ (22 : FRC.Shell (157 : Nat)) ^ (4 : Nat) ≠ (1 : FRC.Shell (157 : Nat)) ∧ ((22 : FRC.Shell (157 : Nat)) ^ (4 : Nat)) ^ (3 : Nat) = (1 : FRC.Shell (157 : Nat)) ∧ (117 : Nat) * (13 : Nat) % (156 : Nat) = (117 : Nat) ∧ (5 : FRC.Shell (157 : Nat)) ^ (39 : Nat) = (129 : FRC.Shell (157 : Nat)) ∧ (12 : Nat) * (13 : Nat) = (52 : Nat) * (3 : Nat) ∧ (156 : Nat) % (12 : Nat) = (0 : Nat) ∧ (156 : Nat) % (52 : Nat) = (0 : Nat) ∧ (∀ (n : Nat), n < (156 : Nat) → (0 : Nat) < n → n % (12 : Nat) = (0 : Nat) → n % (52 : Nat) ≠ (0 : Nat)) ∧ (78 : Nat) * (2 : Nat) = (156 : Nat) :=95  @FRC.Pair.kill_test96/-- p38025 — 38:D1. The capacity stations: $4d<13$ selects $\{1,2,3,10,11,12\}$; the flow law threads every station at all $232$ clock states. -/97theorem p38025 : ((∀ (t : Nat), t < (13 : Nat) → (FRC.Pair.isParam (13 : Nat) (3 : Nat) t = true ↔ t = (1 : Nat) ∨ t = (2 : Nat) ∨ t = (3 : Nat) ∨ t = (10 : Nat) ∨ t = (11 : Nat) ∨ t = (12 : Nat))) ∧ FRC.Pair.shellOf (13 : Nat) (1 : Nat) = (0 : Nat) ∧ FRC.Pair.shellOf (13 : Nat) (2 : Nat) = (1 : Nat) ∧ FRC.Pair.shellOf (13 : Nat) (3 : Nat) = (2 : Nat) ∧ FRC.Pair.shellOf (13 : Nat) (10 : Nat) = (2 : Nat) ∧ FRC.Pair.shellOf (13 : Nat) (11 : Nat) = (1 : Nat) ∧ FRC.Pair.shellOf (13 : Nat) (12 : Nat) = (0 : Nat) ∧ FRC.Pair.count (fun t => FRC.Pair.isParam (13 : Nat) (3 : Nat) t = true) (13 : Nat) = (6 : Nat)) ∧ (∀ (κ k : Nat), (4 : Nat) * k < (4 : Nat) * κ + (1 : Nat) ↔ k ≤ κ) ∧ (∀ (k : Nat), k < (232 : Nat) → FRC.Pair.tick (232 : Nat) k k = (0 : Nat) ∧ FRC.Pair.tick (232 : Nat) k ((116 : Nat) + k) = (116 : Nat)) ∧ (∀ (b : Nat), b < (232 : Nat) → ∀ (k : Nat), k < (13 : Nat) → (FRC.Pair.tick (232 : Nat) k b + b) % (232 : Nat) = k) ∧ (116 : Nat) = (232 / 2 : Nat) :=98  And.intro @FRC.Pair.stations (And.intro @FRC.Pair.window (@FRC.Pair.flow_stations))99/-- p38026 — 38:D2. The step law $\tfrac{11\pi}{12}+\tfrac{\pi}{13}+\tfrac{\pi}{232}$ and the leak $\pi/156-\pi/232$ on the space trace: exact rationals of the chart angle, the angle itself the declared chart unit (A10). -/100theorem p38026 : (9048 : Nat) = (12 : Nat) * (754 : Nat) ∧ (11 : Nat) * (754 : Nat) = (8294 : Nat) ∧ (13 : Nat) * (696 : Nat) = (9048 : Nat) ∧ (232 : Nat) * (39 : Nat) = (9048 : Nat) ∧ (156 : Nat) * (58 : Nat) = (9048 : Nat) ∧ (8294 : Nat) + (696 : Nat) + (39 : Nat) = (9029 : Nat) ∧ (9048 : Nat) - ((58 : Nat) - (39 : Nat)) = (9029 : Nat) ∧ (156 : Nat) = (13 : Nat) * (12 : Nat) ∧ (232 : Nat) = (233 : Nat) - (1 : Nat) ∧ (9048 : Nat) % (12 : Nat) = (0 : Nat) ∧ (9048 : Nat) % (13 : Nat) = (0 : Nat) ∧ (9048 : Nat) % (232 : Nat) = (0 : Nat) :=101  @FRC.Pair.step_law102/-- p38030 — 38:D6. The momentum dual $M_{3}$ at winding $5$: stations, tent shells, $C_{26}$ fold; framed-rational passages $13/5$, $52/5$. -/103theorem p38030 : (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) = -(2 : FRC.Shell (13 : Nat)) ^ (3 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (1 : Nat)) = (5 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (2 : Nat)) = (10 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (3 : Nat)) = (11 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (10 : Nat)) = (2 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (11 : Nat)) = (3 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (12 : Nat)) = (8 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (1 : Nat) = (0 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (2 : Nat) = (0 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (3 : Nat) = (1 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (10 : Nat) = (1 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (11 : Nat) = (0 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (12 : Nat) = (0 : Nat) ∧ (∀ (u : Nat), u < (200 : Nat) → FRC.Pair.tent (13 : Nat) (u + (26 : Nat)) = FRC.Pair.tent (13 : Nat) u) ∧ (4 : Nat) * (13 : Nat) ≤ (13 : Nat) * (5 : Nat) ∧ (39 : Nat) * (5 : Nat) ≤ (4 : Nat) * (52 : Nat) ∧ ¬((4 : Nat) * (26 : Nat) ≤ (13 : Nat) * (5 : Nat) ∨ (39 : Nat) * (5 : Nat) ≤ (4 : Nat) * (26 : Nat)) ∧ ¬((4 : Nat) * (39 : Nat) ≤ (13 : Nat) * (5 : Nat) ∨ (39 : Nat) * (5 : Nat) ≤ (4 : Nat) * (39 : Nat)) :=104  @FRC.Pair.momentum_dual105/-- p38031 — 38:D7. The covering: $144$ slots cover $72/72$; multiplicity $1$ odd $/$ $3$ even; $144=36+108$. -/106theorem p38031 : (FRC.Pair.count (fun n => FRC.Pair.isParam (13 : Nat) (3 : Nat) (n % (13 : Nat)) = true) ((12 : Nat) * (2 : Nat) * (13 : Nat)) = (144 : Nat) ∧ (3 : Nat) * (2 : Nat) * (12 : Nat) = (72 : Nat) ∧ (∀ (s : Nat), s < (3 : Nat) → ∀ (e : Nat), e < (2 : Nat) → ∀ (k : Nat), k < (13 : Nat) → (0 : Nat) < k → FRC.Pair.mult (13 : Nat) (3 : Nat) s e k = if k % (2 : Nat) = (0 : Nat) then (3 : Nat) else (1 : Nat)) ∧ (36 : Nat) * (1 : Nat) + (36 : Nat) * (3 : Nat) = (144 : Nat) ∧ (3 : Nat) * (2 : Nat) * (6 : Nat) = (36 : Nat) ∧ ∀ (t : Nat), t < (13 : Nat) → FRC.Pair.isParam (13 : Nat) (3 : Nat) t = true → FRC.Pair.tent (13 : Nat) ((1 : Nat) * t) = t ∧ FRC.Pair.sheet (13 : Nat) (1 : Nat) t = (0 : Nat)) ∧ ∀ {p a k M A B C D : Nat}, FRC.Nat.isPrime p → p % (2 : Nat) = (1 : Nat) → (0 : Nat) < a → a < p → (0 : Nat) < k → k < p → (0 : Nat) < M → M < p → a * M = p * A + k → (p - M) * a = p * B + (p - M) * a % p → M * (p - a) = p * C + M * (p - a) % p → (p - M) * (p - a) = p * D + (p - M) * (p - a) % p → (A + B + (1 : Nat) = a ∧ A + C + (1 : Nat) = M ∧ C + D + (1 : Nat) = p - a ∧ B + D + (1 : Nat) = p - M) ∧ (FRC.Pair.mu A B C D = (3 : Nat) ↔ k % (2 : Nat) = (0 : Nat)) ∧ (FRC.Pair.mu A B C D = (1 : Nat) ∨ FRC.Pair.mu A B C D = (3 : Nat)) ∧ (k % (2 : Nat) = (1 : Nat) → (a % (2 : Nat) = (1 : Nat) ↔ A % (2 : Nat) = (0 : Nat) ∨ B % (2 : Nat) = (1 : Nat))) :=107  And.intro @FRC.Pair.covering_instance (@FRC.Pair.covering_parity)108/-- p38032 — 38:D8. The half-cell ramification: $t_{1/2}=13/(2m)$; $M_{0}$'s at the origin. -/109theorem p38032 : (∀ (m : Nat), m < (13 : Nat) → (2 : Nat) ≤ m → (4 : Nat) * (13 : Nat) ≤ (13 : Nat) * ((2 : Nat) * m)) ∧ ¬(4 : Nat) * (13 : Nat) ≤ (13 : Nat) * (2 : Nat) ∧ ((2 : Nat) * (6 : Nat) < (13 : Nat) ∧ (13 : Nat) < (2 : Nat) * (7 : Nat)) ∧ ∀ (m : Nat), m < (13 : Nat) → (1 : Nat) ≤ m → ((4 : Nat) * (13 : Nat) ≤ (13 : Nat) * m ↔ (4 : Nat) ≤ m) :=110  @FRC.Pair.ramification111/-- p38033 — 38:D9. The horizon fold fusions: $5\cdot39\equiv-13\ (104)$; eight ends, four points; $E\leftrightarrow B$. -/112theorem p38033 : (5 : Nat) * (39 : Nat) + (13 : Nat) = (2 : Nat) * (104 : Nat) ∧ ((5 : Nat) * (39 : Nat) + (13 : Nat)) % (104 : Nat) = (0 : Nat) ∧ (104 : Nat) = (8 : Nat) * (13 : Nat) ∧ (39 : Nat) = (3 : Nat) * (13 : Nat) ∧ (8 : Nat) = (2 : Nat) * (4 : Nat) :=113  @FRC.Pair.fusion114/-- p38036 — 38:D12. The covering parity theorem, closed at every shell (Theorem~\ref{th:covering}, Lemma~\ref{lem:parity}): $\mu\in\{1,3\}$ by the odd four-sum; decider the row parity and position by the eight-case table; completeness a corollary; the carrier the sheet parity: even rows $\gen$-divisible (thrice), odd rows the half-cell obstruction of D8 (once). -/115theorem p38036 : (∀ {p a b q₁ q₂ : Nat}, FRC.Nat.isPrime p → (0 : Nat) < a → a < p → (0 : Nat) < b → b < p → a * b = p * q₁ + a * b % p → (p - a) * b = p * q₂ + (p - a) * b % p → q₁ + q₂ + (1 : Nat) = b) ∧ (∀ (x : Nat), x < (2 : Nat) → ∀ (y : Nat), y < (2 : Nat) → ∀ (z : Nat), z < (2 : Nat) → ∀ (u : Nat), u < (2 : Nat) → ∀ (v : Nat), v < (2 : Nat) → ∀ (t : Nat), t < (2 : Nat) → ∀ (w : Nat), w < (2 : Nat) → (z + w) % (2 : Nat) = x * y % (2 : Nat) → (z + u + (1 : Nat)) % (2 : Nat) = x → (z + v + (1 : Nat)) % (2 : Nat) = y → (v + t + (1 : Nat)) % (2 : Nat) = ((1 : Nat) + x) % (2 : Nat) → (FRC.Pair.mu z u v t = (3 : Nat) ↔ w = (0 : Nat)) ∧ (FRC.Pair.mu z u v t = (1 : Nat) ∨ FRC.Pair.mu z u v t = (3 : Nat)) ∧ (w = (1 : Nat) → (x = (1 : Nat) ↔ z = (0 : Nat) ∨ u = (1 : Nat)))) ∧ (∀ {p a k M A B C D : Nat}, FRC.Nat.isPrime p → p % (2 : Nat) = (1 : Nat) → (0 : Nat) < a → a < p → (0 : Nat) < k → k < p → (0 : Nat) < M → M < p → a * M = p * A + k → (p - M) * a = p * B + (p - M) * a % p → M * (p - a) = p * C + M * (p - a) % p → (p - M) * (p - a) = p * D + (p - M) * (p - a) % p → (A + B + (1 : Nat) = a ∧ A + C + (1 : Nat) = M ∧ C + D + (1 : Nat) = p - a ∧ B + D + (1 : Nat) = p - M) ∧ (FRC.Pair.mu A B C D = (3 : Nat) ↔ k % (2 : Nat) = (0 : Nat)) ∧ (FRC.Pair.mu A B C D = (1 : Nat) ∨ FRC.Pair.mu A B C D = (3 : Nat)) ∧ (k % (2 : Nat) = (1 : Nat) → (a % (2 : Nat) = (1 : Nat) ↔ A % (2 : Nat) = (0 : Nat) ∨ B % (2 : Nat) = (1 : Nat)))) ∧ ((∀ (a : Nat), a < (13 : Nat) → (0 : Nat) < a → ∀ (b : Nat), b < (13 : Nat) → (0 : Nat) < b → a * b / (13 : Nat) + ((13 : Nat) - a) * b / (13 : Nat) + (1 : Nat) = b) ∧ (∀ (a : Nat), a < (4 : Nat) → (0 : Nat) < a → a * FRC.Pair.inv13 a % (13 : Nat) = (1 : Nat)) ∧ ∀ (a : Nat), a < (4 : Nat) → (0 : Nat) < a → ∀ (k : Nat), k < (13 : Nat) → (0 : Nat) < k → FRC.Pair.mu (a * (k * FRC.Pair.inv13 a % (13 : Nat)) / (13 : Nat)) (((13 : Nat) - k * FRC.Pair.inv13 a % (13 : Nat)) * a / (13 : Nat)) (k * FRC.Pair.inv13 a % (13 : Nat) * ((13 : Nat) - a) / (13 : Nat)) (((13 : Nat) - k * FRC.Pair.inv13 a % (13 : Nat)) * ((13 : Nat) - a) / (13 : Nat)) = if k % (2 : Nat) = (0 : Nat) then (3 : Nat) else (1 : Nat)) ∧ ∀ (a : Nat), a < (4 : Nat) → (0 : Nat) < a → ∀ (e : Nat), e < (2 : Nat) → ∀ (k : Nat), k < (13 : Nat) → (0 : Nat) < k → FRC.Pair.mult (13 : Nat) (3 : Nat) (a - (1 : Nat)) e k = FRC.Pair.mu (a * (k * FRC.Pair.inv13 a % (13 : Nat)) / (13 : Nat)) (((13 : Nat) - k * FRC.Pair.inv13 a % (13 : Nat)) * a / (13 : Nat)) (k * FRC.Pair.inv13 a % (13 : Nat) * ((13 : Nat) - a) / (13 : Nat)) (((13 : Nat) - k * FRC.Pair.inv13 a % (13 : Nat)) * ((13 : Nat) - a) / (13 : Nat)) :=116  And.intro @FRC.Pair.reflection_identity (And.intro @FRC.Pair.parity_table (And.intro @FRC.Pair.covering_parity (And.intro @FRC.Pair.parity_instance (@FRC.Pair.mult_eq_mu))))117/-- p38037 — 38:D13. The family law: the one meridian law generalized (\texttt{baseMW}; $M_{0}$, $M_{3}$ its windings $1$, $5$), the covering arithmetic fully certified; the drawn pair is the family's representative, a drawn ten-sibling layer retracted as washing the sky. -/118theorem p38037 : (FRC.Pair.count (fun n => FRC.Pair.isParam (13 : Nat) (3 : Nat) (n % (13 : Nat)) = true) ((12 : Nat) * (2 : Nat) * (13 : Nat)) = (144 : Nat) ∧ (3 : Nat) * (2 : Nat) * (12 : Nat) = (72 : Nat) ∧ (∀ (s : Nat), s < (3 : Nat) → ∀ (e : Nat), e < (2 : Nat) → ∀ (k : Nat), k < (13 : Nat) → (0 : Nat) < k → FRC.Pair.mult (13 : Nat) (3 : Nat) s e k = if k % (2 : Nat) = (0 : Nat) then (3 : Nat) else (1 : Nat)) ∧ (36 : Nat) * (1 : Nat) + (36 : Nat) * (3 : Nat) = (144 : Nat) ∧ (3 : Nat) * (2 : Nat) * (6 : Nat) = (36 : Nat) ∧ ∀ (t : Nat), t < (13 : Nat) → FRC.Pair.isParam (13 : Nat) (3 : Nat) t = true → FRC.Pair.tent (13 : Nat) ((1 : Nat) * t) = t ∧ FRC.Pair.sheet (13 : Nat) (1 : Nat) t = (0 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (5 : FRC.Shell (13 : Nat)) = -(2 : FRC.Shell (13 : Nat)) ^ (3 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (1 : Nat)) = (5 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (2 : Nat)) = (10 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (3 : Nat)) = (11 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (10 : Nat)) = (2 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (11 : Nat)) = (3 : Nat) ∧ FRC.Pair.tent (13 : Nat) ((5 : Nat) * (12 : Nat)) = (8 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (1 : Nat) = (0 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (2 : Nat) = (0 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (3 : Nat) = (1 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (10 : Nat) = (1 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (11 : Nat) = (0 : Nat) ∧ FRC.Pair.sheet (13 : Nat) (5 : Nat) (12 : Nat) = (0 : Nat) ∧ (∀ (u : Nat), u < (200 : Nat) → FRC.Pair.tent (13 : Nat) (u + (26 : Nat)) = FRC.Pair.tent (13 : Nat) u) ∧ (4 : Nat) * (13 : Nat) ≤ (13 : Nat) * (5 : Nat) ∧ (39 : Nat) * (5 : Nat) ≤ (4 : Nat) * (52 : Nat) ∧ ¬((4 : Nat) * (26 : Nat) ≤ (13 : Nat) * (5 : Nat) ∨ (39 : Nat) * (5 : Nat) ≤ (4 : Nat) * (26 : Nat)) ∧ ¬((4 : Nat) * (39 : Nat) ≤ (13 : Nat) * (5 : Nat) ∨ (39 : Nat) * (5 : Nat) ≤ (4 : Nat) * (39 : Nat)) :=119  And.intro @FRC.Pair.covering_instance (@FRC.Pair.momentum_dual)120/-- p38044 — 38:C10. The per-chronon leak rate: $(\kap/\dS)/(\p-1)=1/(4\dS)=1/(\Om-1)$ exactly, $\kap$-free --- one chart tick per chronon (the temporal face on the cover $1/(2(\Om-1))$); at the instance $(3/58)/12=1/232$, at $(5,233)$ $(1/58)/4=1/232$. The per-revolution fraction $\kap/\dS$ (C7) is this rate times the shell period $\p-1$. -/121theorem p38044 : (∀ {p Ω κ S : Nat}, p = (4 : Nat) * κ + (1 : Nat) → Ω = (4 : Nat) * S + (1 : Nat) → κ * ((4 : Nat) * S) = S * (p - (1 : Nat)) ∧ (4 : Nat) * S = Ω - (1 : Nat) ∧ (2 : Nat) * (Ω - (1 : Nat)) = (8 : Nat) * S) ∧ (12 : Nat) * (58 : Nat) = (3 : Nat) * (232 : Nat) ∧ (12 : Nat) * (116 : Nat) = (3 : Nat) * (464 : Nat) ∧ (3 : Nat) * (116 : Nat) = (2 : Nat) * ((3 : Nat) * (58 : Nat)) ∧ (3 : Nat) * ((4 : Nat) * (58 : Nat)) = (58 : Nat) * ((13 : Nat) - (1 : Nat)) ∧ (1 : Nat) * ((4 : Nat) * (58 : Nat)) = (58 : Nat) * ((5 : Nat) - (1 : Nat)) ∧ (4 : Nat) * (58 : Nat) = (233 : Nat) - (1 : Nat) ∧ (3 : Nat) * (58 : Nat) = (174 : Nat) :=122  And.intro @FRC.Pair.leak_rate (@FRC.Pair.two_faces)123/-- p38046 — 38:X1. \textbf{The weakness of gravity} is the $1/\dS$ suppression of the frame leak: one chart tick per chronon, $1/(4\dS)$ of the cycle --- $1/232$ at the instance, of order $10^{-123}$ at physical capacity; the denominator that makes the world look continuous makes gravity look weak (C10, \S\ref{sec:reality}). -/124theorem p38046 : (∀ {p Ω κ S : Nat}, p = (4 : Nat) * κ + (1 : Nat) → Ω = (4 : Nat) * S + (1 : Nat) → κ * ((4 : Nat) * S) = S * (p - (1 : Nat)) ∧ (4 : Nat) * S = Ω - (1 : Nat) ∧ (2 : Nat) * (Ω - (1 : Nat)) = (8 : Nat) * S) ∧ (12 : Nat) * (58 : Nat) = (3 : Nat) * (232 : Nat) ∧ (12 : Nat) * (116 : Nat) = (3 : Nat) * (464 : Nat) ∧ (3 : Nat) * (116 : Nat) = (2 : Nat) * ((3 : Nat) * (58 : Nat)) ∧ (3 : Nat) * ((4 : Nat) * (58 : Nat)) = (58 : Nat) * ((13 : Nat) - (1 : Nat)) ∧ (1 : Nat) * ((4 : Nat) * (58 : Nat)) = (58 : Nat) * ((5 : Nat) - (1 : Nat)) ∧ (4 : Nat) * (58 : Nat) = (233 : Nat) - (1 : Nat) ∧ (3 : Nat) * (58 : Nat) = (174 : Nat) :=125  And.intro @FRC.Pair.leak_rate (@FRC.Pair.two_faces)126/-- p38048 — 38:X3. \textbf{The acceleration floor $a_{0}=cH_{0}/2\pi$ is the drive seen in the chart}: the leak's cyclic rate is the drive's own, one cycle per drive period $\Om-1$ chronons $=2\pi/H_{0}$, and its acceleration face is the floor (C10; C11, the realisation); at the instance $a_{0}=c/(\Om-1)$. -/127theorem p38048 : ∀ {p Ω κ S : Nat}, p = (4 : Nat) * κ + (1 : Nat) → Ω = (4 : Nat) * S + (1 : Nat) → κ * ((4 : Nat) * S) = S * (p - (1 : Nat)) ∧ (4 : Nat) * S = Ω - (1 : Nat) ∧ (2 : Nat) * (Ω - (1 : Nat)) = (8 : Nat) * S :=128  @FRC.Pair.leak_rate129/-- p38054 — 38:C14. The joint cycle (Theorem~\ref{th:precession}): for every $\kap$-odd pair the chart count advances by $(\p-1)/(\Om-1)=\kap/\dS$ of its cycle per shell revolution; the joint cycle closes at $\mathrm{lcm}(\p-1,\Om-1)$ at (home, home), and the exact midpoint is (home, $-1$). -/130theorem p38054 : (∀ {a m u v ℓ : Nat}, (0 : Nat) < m → ℓ = ((2 : Nat) * a + (1 : Nat)) * ((2 : Nat) * u + (1 : Nat)) → ℓ = m * ((2 : Nat) * v + (1 : Nat)) → (4 : Nat) * ℓ % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) ∧ (4 : Nat) * ℓ % ((8 : Nat) * m) = (4 : Nat) * m ∧ (8 : Nat) * ℓ % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) ∧ (8 : Nat) * ℓ % ((8 : Nat) * m) = (0 : Nat)) ∧ (∀ {p Ω : Nat} [FRC.Pos p] [FRC.Pos Ω] {a m : Nat} {g : FRC.Shell p} {h : FRC.Shell Ω}, FRC.Shell.Frame p ((2 : Nat) * a + (1 : Nat)) g → FRC.Shell.Frame Ω ((2 : Nat) * m) h → (0 : Nat) < m → ∀ {u v ℓ : Nat}, ℓ = ((2 : Nat) * a + (1 : Nat)) * ((2 : Nat) * u + (1 : Nat)) → ℓ = m * ((2 : Nat) * v + (1 : Nat)) → g ^ ((4 : Nat) * ℓ) = (1 : FRC.Shell p) ∧ h ^ ((4 : Nat) * ℓ) = (-1 : FRC.Shell Ω) ∧ g ^ ((8 : Nat) * ℓ) = (1 : FRC.Shell p) ∧ h ^ ((8 : Nat) * ℓ) = (1 : FRC.Shell Ω)) ∧ (∀ {p Ω : Nat} [FRC.Pos p] [FRC.Pos Ω] {κ S : Nat} {g : FRC.Shell p} {h : FRC.Shell Ω}, FRC.Shell.Frame p κ g → FRC.Shell.Frame Ω S h → ∀ (n : Nat), g ^ n = (1 : FRC.Shell p) ∧ h ^ n = (1 : FRC.Shell Ω) ↔ n % (p - (1 : Nat)) = (0 : Nat) ∧ n % (Ω - (1 : Nat)) = (0 : Nat)) ∧ (∀ {a m n : Nat}, (0 : Nat) < m → n % ((4 : Nat) * ((2 : Nat) * a + (1 : Nat))) = (0 : Nat) → n % ((8 : Nat) * m) = (0 : Nat) → ∃ k, n = (8 : Nat) * k ∧ k % ((2 : Nat) * a + (1 : Nat)) = (0 : Nat) ∧ k % m = (0 : Nat)) ∧ (∀ {p Ω κ S : Nat}, p = (4 : Nat) * κ + (1 : Nat) → Ω = (4 : Nat) * S + (1 : Nat) → κ * ((4 : Nat) * S) = S * (p - (1 : Nat)) ∧ (4 : Nat) * S = Ω - (1 : Nat) ∧ (2 : Nat) * (Ω - (1 : Nat)) = (8 : Nat) * S) ∧ (696 : Nat) % (12 : Nat) = (0 : Nat) ∧ (696 : Nat) % (232 : Nat) = (0 : Nat) ∧ (696 : Nat) = (58 : Nat) * (12 : Nat) ∧ (696 : Nat) = (3 : Nat) * (232 : Nat) ∧ (1392 : Nat) = (2 : Nat) * (696 : Nat) ∧ (∀ (n : Nat), n < (696 : Nat) → (0 : Nat) < n → n % (12 : Nat) = (0 : Nat) → n % (232 : Nat) ≠ (0 : Nat)) ∧ (87 : Nat) = (3 : Nat) * (29 : Nat) ∧ (87 : Nat) = ((2 : Nat) * (1 : Nat) + (1 : Nat)) * ((2 : Nat) * (14 : Nat) + (1 : Nat)) ∧ (87 : Nat) = ((2 : Nat) * (14 : Nat) + (1 : Nat)) * ((2 : Nat) * (1 : Nat) + (1 : Nat)) ∧ (4 : Nat) * (87 : Nat) % (12 : Nat) = (0 : Nat) ∧ (4 : Nat) * (87 : Nat) % (232 : Nat) = (116 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) ^ (348 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (348 : Nat) = (-1 : FRC.Shell (233 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (696 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (78 : FRC.Shell (233 : Nat)) ^ (696 : Nat) = (1 : FRC.Shell (233 : Nat)) :=131  And.intro @FRC.Pair.joint_cycle (And.intro @FRC.Pair.joint_cycle_frame (And.intro @FRC.Pair.joint_return_iff (And.intro @FRC.Pair.joint_return_eight (And.intro @FRC.Pair.leak_rate (@FRC.Pair.recurrence)))))132-- end keys133134end FRC.Ledger135