The core module lean/FrcCore/S13.lean — the substrate from first principles, no Mathlib, no axioms (the modules in order: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Transform, Orbit, Sum, Theme/Projective, Theme/Fourier, Theme/Fractional, Theme/Lifts, Theme/Dichotomy, Theme/Rotations, Theme/Heisenberg, Theme/Spectra, Theme/Exclusivity, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Numbers, Theme/Logic, Theme/SecondOrder, Theme/Formation, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Quantum, Theme/Unitary, Theme/Interactions, Theme/Horizon, Theme/Shift, Theme/Lattice, Theme/Drift, Theme/Observation, Theme/Interference, Theme/Composite, Theme/Ladder, Meridian, Fourier, Algebra, Epi, Dimensions, Poly, Quaternion, Causality, Representation, Reductio, Godel, Finitism, Geometry, Complex, Instances, Rh, Entropy, Dirac, Gravity, S13, Qm, Pnp, Keys/Frame, Keys/Extension, Keys/Projective, Keys/Fourier, Keys/Numbers, Keys/Logic, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Keys/Quantum, Keys/Interactions, Keys/Horizon): 37 theorems (0 definitions): 37 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Theme.Pair2import FrcCore.Theme.Projective3import FrcCore.Theme.Drift4import FrcCore.Keys.Gravity5import FrcCore.Keys.Projective6import FrcCore.Keys.Subject78/-!9# 38-s13 — the paper module: every theorem of *The Light Cone of the Minimal Pair* lives in the themes (12 October 2026)1011The finite content of the paper (tree `38-s13-20260801`) is the themes': the resolvable window, the leak rate, the joint12cycle, the tick arithmetic of the flow, the covering parity theorem and the kernel-decided instances of the pair13`(13, 233)` in `Theme/Pair.lean` (`FRC.Pair`, the subject theme); the frame triple and the split fibration in14`Theme/Projective.lean` (`FRC.Shell.Frame.frame_triple`, `unit_split`); the nesting bound in `Theme/Drift.lean`15(`FRC.Drift.nesting_bound`, the gravity theme); the channel, the spinor dichotomy and the Carrier quarter roots in16`Theme/Subject.lean`. Every row of the paper's ledger is a key written by `make_keys.py` from those (`Keys/*.lean`), and17this module carries the rows' declarations `FRC.S13.p38NNN` as aliases of the keys (`make_predicates.py`). No theorem18is stated here twice. Every declaration is checked to depend on no axiom (`check_core_axioms.py`).19-/2021namespace FRC.S132223open FRC.Shell2425262728-- Ledger predicates of 38-s13 (generated by make_predicates.py from docs/38-s13/38-s13-ledger.json; edit the ledger, not this section)29/-- 38:A1 (p38001) — The pair: $\p=13$, $\kap=3$, $\Om=233$, $\dS=58$; $\gen=2$, $\im=5=-\gen^{\kap}$. -/30
theorem 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) :=31 @FRC.Ledger.p3800132/-- 38:A2 (p38002) — 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). -/33theorem 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) :=34 @FRC.Ledger.p3800235/-- 38:A3 (p38003) — The channel at the instance: $\gcd(12,14)=2$, $\gcd(12,28)=4$; $N(\im)=-1$ (Theorem~\ref{th:channel}). -/36theorem 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)) :=37 @FRC.Ledger.p3800338/-- 38:A4 (p38004) — 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}$. -/39theorem 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) :=40 @FRC.Ledger.p3800441/-- 38:A6 (p38006) — The FRC algebra half \cite{algebra}: $\tfrac12=7$, $-\tfrac12=6$; the seam between rows $6$ and $7$. -/42theorem 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) :=43 @FRC.Ledger.p3800644/-- 38:A7 (p38007) — 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}). -/45theorem 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) :=46 @FRC.Ledger.p3800747/-- 38:A8 (p38008) — 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\}$. -/48theorem 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) :=49 @FRC.Ledger.p3800850/-- 38:A9 (p38050) — The two fibrations and the frame triple (Theorem~\ref{th:holography}): $G\cong\Prj^{1}\times\F_\p\times C_{\p-1}$ for every odd $\p$ of the totality, $14\times13\times12$; non-split fibres $C_{\p+1}$ over $\p(\p-1)=156$ with the cone-chart section, split fibres $C_{\p-1}$ over $\p(\p+1)=182$ without; the unit $\im$ is split at every $\p=4\kap+1$. -/51theorem p38050 : (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {ν : FRC.Shell p}, (¬∃ y, y * y = ν) → (∀ (M : FRC.Shell.Frame.M2 p), M.det ≠ (0 : FRC.Shell p) → (M.a ≠ (0 : FRC.Shell p) ∨ M.c ≠ (0 : FRC.Shell p)) ∧ M.act (1 : FRC.Shell p) (0 : FRC.Shell p) = (M.a, M.c) ∧ (FRC.Shell.Frame.boost ν M.a M.c).act (1 : FRC.Shell p) (0 : FRC.Shell p) = (M.a, M.c) ∧ M.a * M.a + -(ν * (M.c * M.c)) ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.M2.smul (M.a * M.a + -(ν * (M.c * M.c))) M = (FRC.Shell.Frame.boost ν M.a M.c).mul (FRC.Shell.Frame.borel (M.a * M.a + -(ν * (M.c * M.c))) (M.a * M.b + -(ν * (M.c * M.d))) M.det)) ∧ (∀ (a b e : FRC.Shell p), (FRC.Shell.Frame.borel a b e).act (1 : FRC.Shell p) (0 : FRC.Shell p) = (a, (0 : FRC.Shell p))) ∧ ∀ (l α1 β1 a1 b1 e1 α2 β2 a2 b2 e2 : FRC.Shell p), l ≠ (0 : FRC.Shell p) → a1 ≠ (0 : FRC.Shell p) → a2 ≠ (0 : FRC.Shell p) → α1 ≠ (0 : FRC.Shell p) ∨ β1 ≠ (0 : FRC.Shell p) → FRC.Shell.Frame.M2.smul l ((FRC.Shell.Frame.boost ν α1 β1).mul (FRC.Shell.Frame.borel a1 b1 e1)) = (FRC.Shell.Frame.boost ν α2 β2).mul (FRC.Shell.Frame.borel a2 b2 e2) → α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) ∧ (∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ {ν : 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], FRC.Nat.isPrime p → ∀ (ν : 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] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (M : FRC.Shell.Frame.M2 p), M.mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul M → M.b = (0 : FRC.Shell p) ∧ M.c = (0 : FRC.Shell p)) ∧ (∀ (a d : FRC.Shell p), (FRC.Shell.Frame.diag a d).mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul (FRC.Shell.Frame.diag a d) ∧ FRC.Shell.Frame.diag a d = FRC.Shell.Frame.borel a (0 : FRC.Shell p) d) ∧ (∀ (l : FRC.Shell p), FRC.Shell.Frame.unit g κ ≠ FRC.Shell.Frame.diag l l) ∧ (∀ (x y : FRC.Shell p), x * x + y * y = (1 : FRC.Shell p) → (FRC.Shell.Frame.diag (x + g ^ κ * y) (x + -(g ^ κ * y))).det = (1 : FRC.Shell p)) ∧ (∀ (M : FRC.Shell.Frame.M2 p), ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a + ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).d = (0 : FRC.Shell p) ∧ ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a * ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a + ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).b * ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).c = -(M.det * M.det)) ∧ (∀ (N : FRC.Shell.Frame.M2 p), N.a + N.d = (0 : FRC.Shell p) → N.a * N.a + N.b * N.c = (-1 : FRC.Shell p) → ∃ M, M.det ≠ (0 : FRC.Shell p) ∧ M.mul (FRC.Shell.Frame.unit g κ) = N.mul M) ∧ (∀ (x y z : FRC.Shell p), x * x + y * y + z * z = (1 : FRC.Shell p) → g ^ κ * x * (g ^ κ * x) + (y + g ^ κ * z) * -(y + -(g ^ κ * z)) = (-1 : FRC.Shell p)) ∧ (∀ (h : FRC.Shell p), ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * h = (1 : FRC.Shell p) → ∀ (a b c : FRC.Shell p), a * a + b * c = (-1 : FRC.Shell p) → -(g ^ κ * a) * -(g ^ κ * a) + h * (b + -c) * (h * (b + -c)) + -(h * (g ^ κ * (b + c))) * -(h * (g ^ κ * (b + c))) = (1 : FRC.Shell p)) ∧ ∀ (N M M' : FRC.Shell.Frame.M2 p), M'.det ≠ (0 : FRC.Shell p) → M.mul (FRC.Shell.Frame.unit g κ) = N.mul M → M'.mul (FRC.Shell.Frame.unit g κ) = N.mul M' → (M'.adj.mul M).mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul (M'.adj.mul M)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {b : FRC.Shell p}, b ≠ (0 : FRC.Shell p) → FRC.Grav.sphereCount p (b * b) = p * (p + (1 : Nat))) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (c : FRC.Shell p), FRC.Grav.nsum (fun x => FRC.Grav.count fun y => FRC.Shell.ofNat x * FRC.Shell.ofNat x + y * y = c) p = p - (1 : Nat) + if c = (0 : FRC.Shell p) then p else (0 : Nat)) ∧ (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) :=52 @FRC.Ledger.p3805053/-- 38:B1 (p38009) — The node field: $72=3\times2\times12$; retarded labels, one chronon of lookback per row. -/54theorem 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 :=55 @FRC.Ledger.p3800956/-- 38:B2 (p38010) — The radial ladder: shells at $R\sin(2a\pi/13)$ [chart]; capacity $4a<\p\Leftrightarrow a\le\kap$. -/57theorem 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) :=58 @FRC.Ledger.p3801059/-- 38:B3 (p38011) — The mounting: $\times3=\gen^{4}$, $120^{\circ}=8$ steps, quarter-blind. -/60theorem 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) :=61 @FRC.Ledger.p3801162/-- 38:B4 (p38012) — The sky chronon: $\chron\bmod24$, the fibre product of $C_{12}$ and $C_{8}$ over $C_{4}$; antipodal at $+12$, closed at $+24$. -/63theorem 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 :=64 @FRC.Ledger.p3801265/-- 38:B5 (p38013) — The recurrence data: $696=\dS\cdot12$, spinor $1392$ [proxy-chart]; the pair registers only the monotone dephasing. -/66theorem 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)) :=67 @FRC.Ledger.p3801368/-- 38:B6 (p38014) — The Hopf representation: node-on-fiber exact; foliation depth $=$ rung ladder; the drawn leaves are the continuum foliation by the unit $\im$, the chart face of the count of A9, distinguishing neither fibration [chart]. -/69theorem p38014 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (M : FRC.Shell.Frame.M2 p), M.mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul M → M.b = (0 : FRC.Shell p) ∧ M.c = (0 : FRC.Shell p)) ∧ (∀ (a d : FRC.Shell p), (FRC.Shell.Frame.diag a d).mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul (FRC.Shell.Frame.diag a d) ∧ FRC.Shell.Frame.diag a d = FRC.Shell.Frame.borel a (0 : FRC.Shell p) d) ∧ (∀ (l : FRC.Shell p), FRC.Shell.Frame.unit g κ ≠ FRC.Shell.Frame.diag l l) ∧ (∀ (x y : FRC.Shell p), x * x + y * y = (1 : FRC.Shell p) → (FRC.Shell.Frame.diag (x + g ^ κ * y) (x + -(g ^ κ * y))).det = (1 : FRC.Shell p)) ∧ (∀ (M : FRC.Shell.Frame.M2 p), ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a + ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).d = (0 : FRC.Shell p) ∧ ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a * ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a + ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).b * ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).c = -(M.det * M.det)) ∧ (∀ (N : FRC.Shell.Frame.M2 p), N.a + N.d = (0 : FRC.Shell p) → N.a * N.a + N.b * N.c = (-1 : FRC.Shell p) → ∃ M, M.det ≠ (0 : FRC.Shell p) ∧ M.mul (FRC.Shell.Frame.unit g κ) = N.mul M) ∧ (∀ (x y z : FRC.Shell p), x * x + y * y + z * z = (1 : FRC.Shell p) → g ^ κ * x * (g ^ κ * x) + (y + g ^ κ * z) * -(y + -(g ^ κ * z)) = (-1 : FRC.Shell p)) ∧ (∀ (h : FRC.Shell p), ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * h = (1 : FRC.Shell p) → ∀ (a b c : FRC.Shell p), a * a + b * c = (-1 : FRC.Shell p) → -(g ^ κ * a) * -(g ^ κ * a) + h * (b + -c) * (h * (b + -c)) + -(h * (g ^ κ * (b + c))) * -(h * (g ^ κ * (b + c))) = (1 : FRC.Shell p)) ∧ ∀ (N M M' : FRC.Shell.Frame.M2 p), M'.det ≠ (0 : FRC.Shell p) → M.mul (FRC.Shell.Frame.unit g κ) = N.mul M → M'.mul (FRC.Shell.Frame.unit g κ) = N.mul M' → (M'.adj.mul M).mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul (M'.adj.mul M)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (c : FRC.Shell p), FRC.Grav.nsum (fun x => FRC.Grav.count fun y => FRC.Shell.ofNat x * FRC.Shell.ofNat x + y * y = c) p = p - (1 : Nat) + if c = (0 : FRC.Shell p) then p else (0 : Nat) :=70 @FRC.Ledger.p3801471/-- 38:B7 (p38015) — 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}). -/72theorem 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) :=73 @FRC.Ledger.p3801574/-- 38:C1 (p38016) — One retarded flow law: $\varphi(k)=-(b_{C}-k)\pi/116$; the Subject draws the gauge-free curl (Theorem~\ref{th:precession}). -/75theorem 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) :=76 @FRC.Ledger.p3801677/-- 38:C3 (p38018) — Ownership: the origin never dressed; rays anchor at the Observer at every clock state. -/78theorem 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) :=79 @FRC.Ledger.p3801880/-- 38:C4 (p38019) — The half-turn exact: odd chart, point reflection; the rim kiss (Theorem~\ref{th:channel}). -/81theorem 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) :=82 @FRC.Ledger.p3801983/-- 38:C5 (p38020) — The $C_{4}$ stations: parity image at $b_{C}=116+k$, home at $b_{C}=k$, gauge-free. -/84theorem 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) :=85 @FRC.Ledger.p3802086/-- 38:C6 (p38021) — The dilation instance $3/58$; the $(53,13)$ kill test (Theorems~\ref{th:precession}, \ref{th:channel}). -/87theorem 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) :=88 @FRC.Ledger.p3802189/-- 38:C7 (p38022) — The two faces of the leak: angular $\kap/\dS$ (the curl), temporal $\kap/(2\dS)$ (the ring, on $C_{464}$); ratio exactly $2$, the double cover. -/90theorem p38022 : (∀ (κ S : Nat), κ * ((2 : Nat) * S) = (2 : Nat) * (κ * S) ∧ (4 : Nat) * κ * ((4 : Nat) * S) = (4 : Nat) * ((4 : Nat) * (κ * S))) ∧ (∀ {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) :=91 @FRC.Ledger.p3802292/-- 38:C10 (p38044) — 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$. -/93theorem 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) :=94 @FRC.Ledger.p3804495/-- 38:C13 (p38053) — The apsidal bound: a nested Subject registers $\kap/\dS=(\p-1)/(\Om-1)<1/(\sqrt\Om+1)$, the nesting condition $\p^{2}<\Om$ itself; on the physical Carrier no Subject registers an observed precession (Mercury's $8.0\times10^{-8}$ per revolution sits $54$ orders above the bound $10^{-61}$ [approx]), and the pair reads per orbit of period $T$ the floor $TH_{0}/2\pi$ (C10, C11; \S\ref{sec:reality}). -/96theorem p38053 : (∀ (q d : Nat), (q + (1 : Nat)) * (q + (1 : Nat)) + d - (q + (1 : Nat)) = q * q + q + d ∧ q * q * ((q + (1 : Nat)) * (q + (1 : Nat)) + d) + d * (q * q + (2 : Nat) * q + d) = (q * q + q + d) * (q * q + q + d) ∧ ((0 : Nat) < d → q * q * ((q + (1 : Nat)) * (q + (1 : Nat)) + d) < (q * q + q + d) * (q * q + q + d)) ∧ ∀ (m : Nat), (q + (1 : Nat)) * (q + (1 : Nat)) = m + q + (1 : Nat) + d → m * m + d * (m + q) = q * q * (m + q + (1 : Nat)) ∧ m * m ≤ q * q * (m + q + (1 : 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 :=97 @FRC.Ledger.p3805398/-- 38:C14 (p38054) — 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$). -/99theorem 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)) :=100 @FRC.Ledger.p38054101/-- 38:D1 (p38025) — The capacity stations: $4d<13$ selects $\{1,2,3,10,11,12\}$; the flow law threads every station at all $232$ clock states. -/102theorem 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) :=103 @FRC.Ledger.p38025104/-- 38:D2 (p38026) — 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). -/105theorem 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) :=106 @FRC.Ledger.p38026107/-- 38:D3 (p38027) — The scale-tower circuit: the period at the FRC algebra half; the radius $R\lvert\sin(2a\pi/13)\rvert$ the declared drawing chart (A10, [approx]). -/108theorem p38027 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → FRC.Shell.ofNat ((4 : Nat) * κ) = (-1 : FRC.Shell p) ∧ FRC.Shell.ofNat ((4 : Nat) * κ) * FRC.Shell.ofNat ((4 : Nat) * κ) = (1 : FRC.Shell p)) ∧ (4 : Nat) * (3 : Nat) = (12 : Nat) ∧ (12 : Nat) = (13 : Nat) - (1 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) ^ (12 : Nat) = (1 : FRC.Shell (13 : Nat)) ∧ (∀ (k : Nat), k < (12 : Nat) → (0 : Nat) < k → (2 : FRC.Shell (13 : Nat)) ^ k ≠ (1 : FRC.Shell (13 : Nat))) ∧ (2 : Nat) * (6 : Nat) < (13 : Nat) ∧ (13 : Nat) < (2 : Nat) * (7 : Nat) :=109 @FRC.Ledger.p38027110/-- 38:D5 (p38029) — Four rays realise the four quarter classes (Theorem~\ref{th:channel}), each a fiber geodesic to the quarter fold $a=13/4$. -/111theorem p38029 : (∀ {p : Nat} [FRC.Pos p] (κ : Nat) (x : FRC.Shell p), x ^ ((4 : Nat) * κ) = (1 : FRC.Shell p) ∧ x ^ ((2 : Nat) * ((4 : Nat) * κ + (2 : Nat))) = (1 : FRC.Shell p) ↔ x ^ (4 : Nat) = (1 : FRC.Shell p)) ∧ (∀ (c : Nat), c < (4 : Nat) → FRC.Pair.count (fun j => j % (4 : Nat) = c) (12 : Nat) = (3 : Nat)) ∧ (9 : Nat) % (4 : Nat) = (1 : Nat) ∧ (6 : Nat) % (4 : Nat) = (2 : Nat) ∧ (2 : FRC.Shell (13 : Nat)) ^ (9 : Nat) = (5 : FRC.Shell (13 : Nat)) ∧ (2 : FRC.Shell (13 : Nat)) ^ (6 : Nat) = (-1 : FRC.Shell (13 : Nat)) ∧ (4 : Nat) * (3 : Nat) < (13 : Nat) ∧ (13 : Nat) < (4 : Nat) * (4 : Nat) :=112 @FRC.Ledger.p38029113/-- 38:D6 (p38030) — The momentum dual $M_{3}$ at winding $5$: stations, tent shells, $C_{26}$ fold; framed-rational passages $13/5$, $52/5$. -/114theorem 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)) :=115 @FRC.Ledger.p38030116/-- 38:D7 (p38031) — The covering: $144$ slots cover $72/72$; multiplicity $1$ odd $/$ $3$ even; $144=36+108$. -/117theorem 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))) :=118 @FRC.Ledger.p38031119/-- 38:D8 (p38032) — The half-cell ramification: $t_{1/2}=13/(2m)$; $M_{0}$'s at the origin. -/120theorem 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) :=121 @FRC.Ledger.p38032122/-- 38:D9 (p38033) — The horizon fold fusions: $5\cdot39\equiv-13\ (104)$; eight ends, four points; $E\leftrightarrow B$. -/123theorem 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) :=124 @FRC.Ledger.p38033125/-- 38:D12 (p38036) — 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). -/126theorem 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)) :=127 @FRC.Ledger.p38036128/-- 38:D13 (p38037) — 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. -/129theorem 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)) :=130 @FRC.Ledger.p38037131/-- 38:X1 (p38046) — \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}). -/132theorem 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) :=133 @FRC.Ledger.p38046134/-- 38:X3 (p38048) — \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)$. -/135theorem 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 :=136 @FRC.Ledger.p38048137/-- 38:X4 (p38051) — \textbf{The shell is holographic}: a Subject's frame datum is one projective direction, one shell cell, one drive phase, and the bulk frame is that boundary datum with nothing left over (Theorem~\ref{th:holography}; the realisation reading and its falsifier, Reading~\ref{th:holography-reading}). -/138theorem p38051 : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν : FRC.Shell p}, (¬∃ y, y * y = ν) → (∀ (M : FRC.Shell.Frame.M2 p), M.det ≠ (0 : FRC.Shell p) → (M.a ≠ (0 : FRC.Shell p) ∨ M.c ≠ (0 : FRC.Shell p)) ∧ M.act (1 : FRC.Shell p) (0 : FRC.Shell p) = (M.a, M.c) ∧ (FRC.Shell.Frame.boost ν M.a M.c).act (1 : FRC.Shell p) (0 : FRC.Shell p) = (M.a, M.c) ∧ M.a * M.a + -(ν * (M.c * M.c)) ≠ (0 : FRC.Shell p) ∧ FRC.Shell.Frame.M2.smul (M.a * M.a + -(ν * (M.c * M.c))) M = (FRC.Shell.Frame.boost ν M.a M.c).mul (FRC.Shell.Frame.borel (M.a * M.a + -(ν * (M.c * M.c))) (M.a * M.b + -(ν * (M.c * M.d))) M.det)) ∧ (∀ (a b e : FRC.Shell p), (FRC.Shell.Frame.borel a b e).act (1 : FRC.Shell p) (0 : FRC.Shell p) = (a, (0 : FRC.Shell p))) ∧ ∀ (l α1 β1 a1 b1 e1 α2 β2 a2 b2 e2 : FRC.Shell p), l ≠ (0 : FRC.Shell p) → a1 ≠ (0 : FRC.Shell p) → a2 ≠ (0 : FRC.Shell p) → α1 ≠ (0 : FRC.Shell p) ∨ β1 ≠ (0 : FRC.Shell p) → FRC.Shell.Frame.M2.smul l ((FRC.Shell.Frame.boost ν α1 β1).mul (FRC.Shell.Frame.borel a1 b1 e1)) = (FRC.Shell.Frame.boost ν α2 β2).mul (FRC.Shell.Frame.borel a2 b2 e2) → α1 * β2 = α2 * β1 ∧ e2 * a1 = e1 * a2 ∧ e2 * b1 = e1 * b2) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → (∀ (M : FRC.Shell.Frame.M2 p), M.mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul M → M.b = (0 : FRC.Shell p) ∧ M.c = (0 : FRC.Shell p)) ∧ (∀ (a d : FRC.Shell p), (FRC.Shell.Frame.diag a d).mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul (FRC.Shell.Frame.diag a d) ∧ FRC.Shell.Frame.diag a d = FRC.Shell.Frame.borel a (0 : FRC.Shell p) d) ∧ (∀ (l : FRC.Shell p), FRC.Shell.Frame.unit g κ ≠ FRC.Shell.Frame.diag l l) ∧ (∀ (x y : FRC.Shell p), x * x + y * y = (1 : FRC.Shell p) → (FRC.Shell.Frame.diag (x + g ^ κ * y) (x + -(g ^ κ * y))).det = (1 : FRC.Shell p)) ∧ (∀ (M : FRC.Shell.Frame.M2 p), ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a + ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).d = (0 : FRC.Shell p) ∧ ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a * ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).a + ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).b * ((M.mul (FRC.Shell.Frame.unit g κ)).mul M.adj).c = -(M.det * M.det)) ∧ (∀ (N : FRC.Shell.Frame.M2 p), N.a + N.d = (0 : FRC.Shell p) → N.a * N.a + N.b * N.c = (-1 : FRC.Shell p) → ∃ M, M.det ≠ (0 : FRC.Shell p) ∧ M.mul (FRC.Shell.Frame.unit g κ) = N.mul M) ∧ (∀ (x y z : FRC.Shell p), x * x + y * y + z * z = (1 : FRC.Shell p) → g ^ κ * x * (g ^ κ * x) + (y + g ^ κ * z) * -(y + -(g ^ κ * z)) = (-1 : FRC.Shell p)) ∧ (∀ (h : FRC.Shell p), ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * h = (1 : FRC.Shell p) → ∀ (a b c : FRC.Shell p), a * a + b * c = (-1 : FRC.Shell p) → -(g ^ κ * a) * -(g ^ κ * a) + h * (b + -c) * (h * (b + -c)) + -(h * (g ^ κ * (b + c))) * -(h * (g ^ κ * (b + c))) = (1 : FRC.Shell p)) ∧ ∀ (N M M' : FRC.Shell.Frame.M2 p), M'.det ≠ (0 : FRC.Shell p) → M.mul (FRC.Shell.Frame.unit g κ) = N.mul M → M'.mul (FRC.Shell.Frame.unit g κ) = N.mul M' → (M'.adj.mul M).mul (FRC.Shell.Frame.unit g κ) = (FRC.Shell.Frame.unit g κ).mul (M'.adj.mul M)) ∧ ∀ {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) :=139 @FRC.Ledger.p38051140-- end ledger predicates141142end FRC.S13143