The core module lean/FrcCore/Spacetime.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 39 modules: Nat, Pigeonhole, Shell, Series, Cycle, Ring, FrameCore, Frame, Parity, Theme/Projective, Theme/Lorentz, Theme/Register, Theme/Quadratic, Theme/Extension, Theme/Tally, Theme/Logic, Theme/Field, Theme/Foundation, Theme/Drive, Theme/Carrier, Theme/Subject, Theme/Pair, Theme/Hopf, Theme/Symbol, Theme/Gravity, Theme/Shift, Theme/Lattice, Theme/Drift, Poly, Keys/Extension, Keys/Projective, Keys/Foundation, Keys/Carrier, Keys/Subject, Keys/Gravity, Theme/Spin, Theme/Domain, Keys/Domain, Theme/Causal: 50 theorems (0 definitions): 50 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.Lorentz2import FrcCore.Theme.Hopf3import FrcCore.Theme.Pair4import FrcCore.Keys.Extension5import FrcCore.Keys.Foundation6import FrcCore.Keys.Gravity7import FrcCore.Keys.Projective8import FrcCore.Keys.Subject9import FrcCore.Keys.Carrier10import FrcCore.Keys.Domain1112/-!13# 7-spacetime — the paper module: every theorem of *Emergent Lorentzian Space-Time over Finite Holographic Substrate* lives in the themes (31 October 2026)1415The finite content of the paper (tree `7-spacetime-20261027`) is the themes': the register square, the congruence of16`SL₂(𝔽_{p²})` with its kernel `±I`, the cone, the two four-dimensional classes, the similitude, the fibration's17stabiliser, the drive and the lift, the horizon and the three exclusions of the arrow, the leak's order in18`Theme/Lorentz.lean` (`FRC.Lorentz`, the projective theme); the unitary form `SU₂ = SL₂` and the adjoint action in19`Theme/Spin.lean` (`FRC.Spin`); the Hopf section, the counts and the frame triple in `Theme/Projective.lean` and20`Theme/Hopf.lean`; the leak rate and the joint cycle of the pair in `Theme/Pair.lean` (`FRC.Pair`, the subject theme).21Every row of the paper's ledger is a key written by `make_keys.py` from those (`Keys/*.lean`), and this module carries22the rows' declarations `FRC.Spacetime.<name>` (named by their rows' declared names, the key in each docstring) as aliases of the keys (`make_predicates.py`). No theorem is stated here23twice. Every declaration is checked to depend on no axiom (`check_core_axioms.py`).24-/2526namespace FRC.Spacetime2728open FRC.Shell293031-- Ledger predicates of 7-spacetime (generated by make_predicates.py from docs/7-spacetime/7-spacetime-ledger.json; edit the ledger, not this section)32/-- 7:A4 (p00021) — The frame, Subject-only: $(\chron;0,1,\gen)$, origin, unit and the drive $x\mapsto\gen x$; $\gen$ the one nonsquare frame datum; the shell $\p=4\kap+1$, $\im=-\gen^{\kap}$, $\pi=2\kap$. -/33
theorem frame_subject_only : ∀ {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 :=34 @FRC.Ledger.p0002135/-- 7:A6 (p00150) — The signature is the square class of the temporal coefficient $\nu=\gen$; the split and the non-split torus are the two signatures. -/36theorem euclidean_lorentzian_dichotomy : (∀ {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)) :=37 @FRC.Ledger.p0015038/-- 7:A8 (p03008) — The counts of the two four-dimensional classes: $\p^{3}+\p^{2}-\p$ null vectors for the hyperbolic class, $\p^{3}-\p^{2}+\p$ for the elliptic. -/39theorem dichotomy_on_shell : (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν : FRC.Shell p}, ¬FRC.Shell.Frame.IsSquare ν → FRC.Causal.formCount ν (0 : FRC.Shell p) + p * p = p * p * p + p) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {w : FRC.Shell p}, w ≠ (0 : FRC.Shell p) → FRC.Causal.formCount (w * w) (0 : FRC.Shell p) + p = p * p * p + p * p) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν : FRC.Shell p}, ¬FRC.Shell.Frame.IsSquare ν → FRC.Causal.planeCount ν (0 : FRC.Shell p) = (1 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {w : FRC.Shell p}, w ≠ (0 : FRC.Shell p) → FRC.Causal.planeCount (w * w) (0 : FRC.Shell p) + (1 : Nat) = (2 : Nat) * p :=40 @FRC.Ledger.p0300841/-- 7:A9 (p03011) — For $\nu$ a nonsquare the two classes of non-null vectors of $Q_{\nu}$ are equal in size, $(\p-1)(\p^{3}+\p)/2$ each, and invariant under the orthogonal group and under rescaling. -/42theorem causal_classes : (∀ {p : Nat} [FRC.Pos p] (ν a b c t x y z : FRC.Shell p), a * a + b * b = ν → c * c = (-1 : FRC.Shell p) → -(ν * (c * z * (c * z))) + (a * x + -(b * y)) * (a * x + -(b * y)) + (b * x + a * y) * (b * x + a * y) + c * (ν * t) * (c * (ν * t)) = ν * (-(ν * (t * t)) + x * x + y * y + z * z)) ∧ (∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {s : FRC.Shell p}, s ≠ (0 : FRC.Shell p) → (FRC.Shell.Frame.IsSquare s ↔ ¬FRC.Shell.Frame.IsSquare (g * s))) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {ν : FRC.Shell p}, ¬FRC.Shell.Frame.IsSquare ν → FRC.Causal.formCount ν (0 : FRC.Shell p) + p * p = p * p * p + p :=43 @FRC.Ledger.p0301144/-- 7:A10 (p03013) — The norm-one group of the plane form $-\nu t^{2}+x^{2}$ is the cycle $C_{\p+1}$, the non-split torus, for $\nu$ a nonsquare, and the split torus $C_{\p-1}$ for $\nu$ a square. -/45theorem finite_boost : (∀ {p : Nat} [FRC.Pos p] {ν γ b : FRC.Shell p}, γ * γ + -(ν * (b * b)) = (1 : FRC.Shell p) → ∀ (t x : FRC.Shell p), FRC.Shell.Frame.Q2 ν (FRC.Shell.Frame.boostT ν γ b t x) (FRC.Shell.Frame.boostX ν γ b t x) = FRC.Shell.Frame.Q2 ν t x) ∧ (∀ {p : Nat} [FRC.Pos p] (ν γ1 b1 γ2 b2 t x : FRC.Shell p), FRC.Shell.Frame.boostT ν γ1 b1 (FRC.Shell.Frame.boostT ν γ2 b2 t x) (FRC.Shell.Frame.boostX ν γ2 b2 t x) = FRC.Shell.Frame.boostT ν (γ1 * γ2 + ν * (b1 * b2)) (γ1 * b2 + b1 * γ2) t x) ∧ (∀ {p : Nat} [FRC.Pos p] (ν γ1 b1 γ2 b2 t x : FRC.Shell p), FRC.Shell.Frame.boostX ν γ1 b1 (FRC.Shell.Frame.boostT ν γ2 b2 t x) (FRC.Shell.Frame.boostX ν γ2 b2 t x) = FRC.Shell.Frame.boostX ν (γ1 * γ2 + ν * (b1 * b2)) (γ1 * b2 + b1 * γ2) t x) ∧ (∀ {p : Nat} [FRC.Pos p] {ν γ1 b1 γ2 b2 : FRC.Shell p}, γ1 * γ1 + -(ν * (b1 * b1)) = (1 : FRC.Shell p) → γ2 * γ2 + -(ν * (b2 * b2)) = (1 : FRC.Shell p) → (γ1 * γ2 + ν * (b1 * b2)) * (γ1 * γ2 + ν * (b1 * b2)) + -(ν * ((γ1 * b2 + b1 * γ2) * (γ1 * b2 + b1 * γ2))) = (1 : FRC.Shell p)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ {c : FRC.Shell p}, c ≠ (0 : FRC.Shell p) → FRC.Causal.planeCount g c = p + (1 : Nat) :=46 @FRC.Ledger.p0301347/-- 7:A11 (p00190) — The Hopf section: the frame moves factor as the affine group times the non-split torus, $G=B\cdot T$, on the frames by elements. -/48theorem hopf_section : (∀ {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) :=49 @FRC.Ledger.p0019050/-- 7:A12 (p38050) — The frame triple: one projective direction, one shell cell, one drive phase; the $\p+1$ directions of $\mathbb{P}^{1}(\Fp)$. -/51theorem frame_triple : (∀ {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/-- 7:A13 (p00152) — $\mathrm{PGL}_2(\Fp)\cong\mathrm{SO}_3(\Fp)$; the census of its elements by type. -/54theorem frame_variety : (∀ {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}, (¬∃ 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)) ∧ (∀ {p : Nat} [FRC.Pos p] (M X : FRC.Shell.Frame.M2 p), ((M.mul X).mul M.adj).det = M.det * M.det * X.det ∧ ((M.mul X).mul M.adj).a + ((M.mul X).mul M.adj).d = M.det * (X.a + X.d)) ∧ ∀ {p : Nat} [FRC.Pos p] {κ : Nat} {g : FRC.Shell p}, FRC.Shell.Frame p κ g → ∀ (M : FRC.Shell.Frame.M2 p), M.mul FRC.Spin.J = FRC.Spin.J.mul M → M.mul FRC.Spin.D = FRC.Spin.D.mul M → M.b = (0 : FRC.Shell p) ∧ M.c = (0 : FRC.Shell p) ∧ M.a = M.d :=55 @FRC.Ledger.p0015256/-- 7:A14 (p00183) — The frame group has one form: $\mathrm{SU}_2(\F_{\p^{2}}/\Fp)=\mathrm{SL}_2(\Fp)$ for the Hermitian form $wJ$, $w^{\p}=-w$; the sphere $ad-bc=1$. -/57theorem frame_group_one_form : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} {w : FRC.Extension.Ext p ν}, w.conj = -w → (FRC.Spin.M2x.wJ w).dagger = FRC.Spin.M2x.wJ w) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → ∀ {w : FRC.Extension.Ext p ν}, w ≠ (0 : FRC.Extension.Ext p ν) → ∀ (M : FRC.Spin.M2x p ν), M.det = (1 : FRC.Extension.Ext p ν) → ((FRC.Spin.M2x.wJ w).unitary M ↔ M.conj = M)) ∧ (∀ {p : Nat} [FRC.Pos p] (M : FRC.Shell.Frame.M2 p), M.det = (1 : FRC.Shell p) → ∃ n, (0 : Nat) < n ∧ n ≤ p * (p * (p * p)) ∧ FRC.Spin.mpow M n = FRC.Spin.I) ∧ (∀ {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' :=58 @FRC.Ledger.p0018359/-- 7:A15 (p00139) — Origin and antipode: the origin $[0:1]$ and the antipode $[1:0]$ of the frame's line; the antipode is no residue, the antipodal point $\p/2$ of the additive cycle between $2\kap$ and $2\kap+1$. -/60theorem antipode_on_torus : (∀ {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 :=61 @FRC.Ledger.p0013962/-- 7:A16 (p00028) — The squares are the even drive steps: a residue's quadratic class is its drive-step parity; registered transport is even, the one-way multiplier $\gen$ odd. -/63theorem square_class_parity : (∀ {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 :=64 @FRC.Ledger.p0002865/-- 7:A17 (p00042) — Time is the drive: each Subject's clock is its own drive $x\mapsto\gen x$. A chronon is one drive step; a registered duration is the count of chronons, the Subject's chart count, injective on every registrable depth; the Carrier has no clock. -/66theorem time_is_scale_dilation : (∀ {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) ∧ (∀ (Om n : Nat), n < Om - (1 : Nat) → n % (Om - (1 : Nat)) = n) ∧ (∀ (p S n : Nat), p % (2 : Nat) = (1 : Nat) → p * p < (4 : Nat) * S + (1 : Nat) → n ≤ p * p → n < (4 : Nat) * S + (1 : Nat) - (1 : Nat)) ∧ (13 : Nat) * (13 : Nat) < (232 : Nat) ∧ (173 : Nat) * (173 : Nat) < (30088 : Nat) ∧ (1549 : Nat) * (1549 : Nat) < (2408560 : Nat) ∧ (13 : Nat) * (13 : Nat) < (180 : Nat) ∧ (13 : Nat) * (13 : Nat) < (696 : Nat) ∧ (173 : Nat) * (173 : Nat) < (1293784 : Nat) ∧ (1549 : Nat) * (1549 : Nat) < (932112720 : Nat) ∧ (13 : Nat) * (13 : Nat) < (180 : Nat) :=67 @FRC.Ledger.p0004268/-- 7:A21 (p38053) — The nesting condition $\p^{2}<\Om$: the Subject's pair space fits the Carrier; equivalent to $\kap/\dS<1/(\sqrt{\Om}+1)$ [chart]. -/69theorem apsidal_bound : (∀ (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 :=70 @FRC.Ledger.p3805371/-- 7:A23 (p00162) — Completeness is primality: the Carrier's chart $\F_{\Om}$ is a field and has no proper nonzero ideal. -/72theorem completeness_is_primality : ∀ {p : Nat} [FRC.Pos p], (2 : Nat) ≤ p → (FRC.Nat.isPrime p ↔ ∀ (I : FRC.Shell p → Prop), I (0 : FRC.Shell p) → (∀ (a b : FRC.Shell p), I a → I b → I (a + b)) → (∀ (r a : FRC.Shell p), I a → I (r * a)) → (∃ a, I a ∧ a ≠ (0 : FRC.Shell p)) → ∀ (x : FRC.Shell p), I x) :=73 @FRC.Ledger.p0016274/-- 7:A24 (p38044) — The per-chronon drift rate: an embedded shell's chart count, its position in its own chart of the Carrier's cycle, advances by $1/(\Om-1)$ of the cycle per chronon; on a hosted Carrier the host's clock drives every shell at that rate. -/75theorem drift_rate : (∀ {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) :=76 @FRC.Ledger.p3804477/-- 7:A25 (p38054) — The joint cycle of a hosted pair: the advance per shell revolution is $\kap/\dS=(\p-1)/(\Om-1)$ of the Carrier's chart cycle, and on a hosted Carrier run through its cycle the joint state returns after $\mathrm{lcm}(\p-1,\Om-1)$ chronons. -/78theorem joint_cycle : (∀ {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)) :=79 @FRC.Ledger.p3805480/-- 7:A26 (p38016) — One retarded flow law: registration is retarded along the drift, the same across the three representations. -/81theorem retarded_flow : (∀ (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) :=82 @FRC.Ledger.p3801683/-- 7:A28 (p21018) — The drive has a single arrow; its reversal would need the Frobenius-branch clock. -/84theorem single_arrow : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), z.norm = (1 : FRC.Shell p) → ∀ (n : Nat), z ^ n * z.conj ^ n = (1 : FRC.Extension.Ext p ν)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν) (n : Nat), (z ^ n).conj = z.conj ^ n :=85 @FRC.Ledger.p2101886/-- 7:A31 (p21052) — The weak-acceleration floor of registration against the drift is $a_{0}=c/T_H=cH_{0}/2\pi$, with $T_H=2\pi/H_{0}$ the drive period by the angle--count dictionary: $1.04\times10^{-10}$ m\,s$^{-2}$ at $H_{0}=67.4$ km\,s$^{-1}$\,Mpc$^{-1}$, against the fitted $1.20\pm0.24\times10^{-10}$ [chart]. -/87theorem weak_acceleration_floor : ∀ (a T H τ c : Nat), a * T = c → T * H = τ → a * τ = c * H :=88 @FRC.Ledger.p2105289/-- 7:A32 (p00032) — Temperature carries the acceleration domain: $[\Theta]=[E][k_B]^{-1}=[L][T]^{-2}$, flag-free, with $\Theta_P=E_P/|k_B|$, and the Unruh combination $\hbar a/2\pi c\,k_B$ closes as a domain identity; neither mass nor temperature is primitive. -/90theorem temperature_domain : (FRC.Domain.Lift.temp = FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.temp = { r := (1 : Int), s := (-2 : Int), j := (0 : Int) } ∧ FRC.Domain.Lift.kB = { r := (-1 : Int), s := (1 : Int), j := (1 : Int) }) ∧ (FRC.Domain.Lift.temp.j = (0 : Int) ∧ FRC.Domain.Lift.energy.j = (1 : Int) ∧ FRC.Domain.Lift.hbar.j = (1 : Int) ∧ FRC.Domain.Lift.kB.j = (1 : Int)) ∧ (FRC.Domain.Lift.unruh = FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.unruh.j = (0 : Int)) ∧ (FRC.Domain.Lift.mass = { r := (-2 : Int), s := (1 : Int), j := (1 : Int) } ∧ FRC.Domain.Lift.temp = FRC.Domain.Lift.L * FRC.Domain.Lift.T⁻¹ * FRC.Domain.Lift.T⁻¹ ∧ FRC.Domain.Lift.energy * (FRC.Domain.Lift.hbar * FRC.Domain.Lift.speed⁻¹)⁻¹ = FRC.Domain.Lift.accel ∧ (FRC.Domain.Lift.energy * (FRC.Domain.Lift.hbar * FRC.Domain.Lift.speed⁻¹)⁻¹).j = (0 : Int)) ∧ (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int) = FRC.Domain.Lift.mass ∧ FRC.Domain.Lift.classical (0 : Int) (1 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.speed ∧ FRC.Domain.Lift.classical (0 : Int) (1 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.energy ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.hbar ∧ FRC.Domain.Lift.classical (1 : Int) (1 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.force ∧ FRC.Domain.Lift.classical (1 : Int) (1 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.momentum ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-3 : Int) (0 : Int) = FRC.Domain.Lift.power ∧ FRC.Domain.Lift.classical (1 : Int) (-1 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.pressure ∧ FRC.Domain.Lift.classical (-1 : Int) (3 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.G ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-2 : Int) (-1 : Int) = FRC.Domain.Lift.kB ∧ FRC.Domain.Lift.classical (0 : Int) (0 : Int) (0 : Int) (1 : Int) = FRC.Domain.Lift.temp) ∧ (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int) = FRC.Domain.Lift.L ∧ FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int) = FRC.Domain.Lift.T ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.flag ∧ FRC.Domain.Lift.classical (0 : Int) (0 : Int) (0 : Int) (1 : Int) = FRC.Domain.Lift.classical (0 : Int) (1 : Int) (-2 : Int) (0 : Int) ∧ FRC.Domain.Lift.classical (0 : Int) (-1 : Int) (2 : Int) (1 : Int) = (1 : FRC.Domain.Lift) ∧ (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int)).r * ((FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).s * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).j - (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).j * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).s) - (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int)).s * ((FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).r * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).j - (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).j * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).r) + (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int)).j * ((FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).r * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).s - (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).s * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).r) = (1 : Int) ∧ FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag ≠ (1 : FRC.Domain.Lift)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.temp = FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.unruh = FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.temp = ((1 : Int), (10 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.flag = ((0 : Int), (3 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.T * FRC.Domain.Lift.T * FRC.Domain.Lift.T) = ((0 : Int), (3 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.flag ≠ ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) ≠ ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) ≠ ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.mass = ((11 : Int), (4 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.temp = FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.unruh = FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.temp = ((1 : Int), (170 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.flag = ((0 : Int), (43 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (86 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (129 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.mass = ((171 : Int), (44 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.temp = FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.unruh = FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.flag = ((0 : Int), (343 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (686 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (1029 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.mass = ((1371 : Int), (344 : Int)) :=91 @FRC.Ledger.p0003292/-- 7:A33 (p00165) — On a Carrier of even capacity $\dS$ ($\Om\equiv1\pmod 8$) the register $\{\dS,\Om,c,\hbar,G,k_B\}$ is generator-free in the capacity: $G=2\dS=-c^{2}$, $2c^{2}\equiv1$, $\hbar^{2}\equiv-1$ and $k_B^{2}\equiv-2\pmod\Om$, with $|k_B|=\hbar/c$; $G$ is exact and the rest hold up to sign. -/93theorem carrier_register : ∀ {Ω : Nat} [FRC.Pos Ω] (S : Nat), FRC.Nat.isPrime Ω → Ω = (4 : Nat) * S + (1 : Nat) → (2 : FRC.Shell Ω) * FRC.Carrier.csq Ω S = (1 : FRC.Shell Ω) ∧ FRC.Carrier.grav Ω S = -FRC.Carrier.csq Ω S ∧ (2 : FRC.Shell Ω) * FRC.Carrier.grav Ω S = (-1 : FRC.Shell Ω) ∧ (∀ (x : FRC.Shell Ω), (2 : FRC.Shell Ω) * x = (-1 : FRC.Shell Ω) → x = FRC.Carrier.grav Ω S) ∧ (∃ ħ, ħ * ħ = (-1 : FRC.Shell Ω)) ∧ ((∃ c, c * c = FRC.Carrier.csq Ω S) ↔ S % (2 : Nat) = (0 : Nat)) ∧ (∀ (c ħ k : FRC.Shell Ω), c * c = FRC.Carrier.csq Ω S → ħ * ħ = (-1 : FRC.Shell Ω) → k * c = ħ → k * k = (-2 : FRC.Shell Ω)) ∧ (∀ (x y : FRC.Shell Ω), x * x = y * y → x = y ∨ x = -y) ∧ ∀ (ħ : FRC.Shell Ω), ħ * ħ = (-1 : FRC.Shell Ω) → -ħ * -ħ = (-1 : FRC.Shell Ω) ∧ -ħ ≠ ħ :=94 @FRC.Ledger.p0016595/-- 7:B1 (p07003) — Every frame move of $G=\mathrm{PGL}_2(\Fp)$ factors uniquely as scale, translation and rotation, on $C_{4\kap}$, $C_{4\kap+1}$ and $C_{4\kap+2}$, of consecutive orders; on the spin cover the section obstructs at $-I$. -/96theorem frame_move_factors : (∀ {p : Nat} [FRC.Pos p], FRC.Shell.Frame.Fld 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) ∧ (∀ (κ : Nat), (4 : Nat) * κ + (1 : Nat) - (1 : Nat) = (4 : Nat) * κ ∧ (4 : Nat) * κ + (1 : Nat) + (1 : Nat) = (4 : Nat) * κ + (2 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : 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.Extension.Ext p ν).norm = (1 : FRC.Shell p) ∧ (-1 : FRC.Extension.Ext p ν).conj = (-1 : FRC.Extension.Ext p ν) :=97 @FRC.Ledger.p0700398set_option linter.defProp false in99/-- 7:B4 (p07042) — The necessity chain: time's coefficient is the drive's generator $\gen$, a nonsquare; the temporal plane $-\gen t^{2}+x^{2}$ is anisotropic with norm-one group $C_{\p+1}$, the third cycle, and the register square is elliptic; a square coefficient gives the split plane, the cycle $C_{\p-1}$ again, and no time. -/100def necessity_chain := @FRC.Ledger.p07042101/-- 7:B5 (p07049) — The registrable depth: the Subject's register pair takes $\p^{2}$ values, the pair space of the nesting condition, and the states of a registrable duration are pairwise distinct, so a registrable duration has at most $\p^{2}$ chronons. -/102theorem registrable_depth : (∀ (n : Nat) (l : List Nat), FRC.Pigeonhole.NoDup l → (∀ (e : Nat), FRC.Pigeonhole.mem e l → e < n) → l.length ≤ n) ∧ ∀ (p S n : Nat), p % (2 : Nat) = (1 : Nat) → p * p < (4 : Nat) * S + (1 : Nat) → n ≤ p * p → n < (4 : Nat) * S + (1 : Nat) - (1 : Nat) :=103 @FRC.Ledger.p07049104/-- 7:B6 (p07050) — The register: the capacity register is the ring $\Z_{\p}$, the additive cycle $C_{\p}$ of the $4\kap+1$ cells; its translations $z\mapsto z+b$ are the unipotent moves of the frame, and each nontrivial translation fixes exactly one direction of the frame's line, the antipode $[1:0]$. -/105theorem register_cycle : ∀ {p : Nat} [FRC.Pos p], FRC.Nat.isPrime p → ∀ (b x y : FRC.Shell p), b ≠ (0 : FRC.Shell p) → (x + b * y = x ↔ y = (0 : FRC.Shell p)) :=106 @FRC.Ledger.p07050107set_option linter.defProp false in108/-- 7:C1 (p07005) — The register square $\mathrm{Herm}_2(K)=\mathrm{Sym}^{2}(V)\oplus\Fp\,\eta J$ with $\det X=x_{0}^{2}-x_{1}^{2}-x_{3}^{2}+\gen x_{2}^{2}$; the map $\varphi$ is an isometry onto $Q_{\gen}$. -/109def register_square_isometry := @FRC.Ledger.p07005110/-- 7:C2 (p07006) — The congruence $X\mapsto AXA^{\dagger}$ of $\mathrm{SL}_2(K)$ preserves the register square and its determinant, has kernel $\pm I$ and image of order $\p^{2}(\p^{4}-1)/2$, the finite Lorentz group. -/111theorem congruence_preserves_square : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Spin.M2x p ν) (x0 x1 x2 x3 : FRC.Shell p), (FRC.Lorentz.cong A (FRC.Lorentz.X x0 x1 x2 x3)).det = A.det * A.det.conj * FRC.Extension.Ext.ofShell (FRC.Lorentz.Q ν x0 x1 x2 x3)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Spin.M2x p ν) (x0 x1 x2 x3 : FRC.Shell p), (FRC.Lorentz.cong A (FRC.Lorentz.X x0 x1 x2 x3)).dagger = FRC.Lorentz.cong A (FRC.Lorentz.X x0 x1 x2 x3)) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → ∀ (x0 x1 x2 x3 : FRC.Shell p), (FRC.Lorentz.cong A (FRC.Lorentz.X x0 x1 x2 x3)).det = FRC.Extension.Ext.ofShell (FRC.Lorentz.Q ν x0 x1 x2 x3)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) → A = FRC.Lorentz.diagx (1 : FRC.Extension.Ext p ν) (1 : FRC.Extension.Ext p ν) ∨ A = FRC.Lorentz.diagx (-1 : FRC.Extension.Ext p ν) (-1 : FRC.Extension.Ext p ν) :=112 @FRC.Ledger.p07006113/-- 7:C3 (p07007) — The cone is $\mathbb{P}^{1}(K)$: $[v]\mapsto[vv^{\dagger}]$ is a bijection onto the null lines of the register square, $\p^{2}+1$ directions. -/114theorem null_cone : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (h : FRC.Shell p), ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * h = (1 : FRC.Shell p) → ∀ (v1 v2 : FRC.Extension.Ext p ν), { a := v1 * v1.conj, b := v1 * v2.conj, c := v2 * v1.conj, d := v2 * v2.conj } = FRC.Lorentz.X (h * (v1.norm + v2.norm)) (v1 * v2.conj).re (v1 * v2.conj).im (h * (v1.norm + -v2.norm)) ∧ FRC.Lorentz.Q ν (h * (v1.norm + v2.norm)) (v1 * v2.conj).re (v1 * v2.conj).im (h * (v1.norm + -v2.norm)) = (0 : FRC.Shell p)) ∧ FRC.Lorentz.nullCount13 = (2041 : Nat) ∧ (2041 : Nat) = (13 : Nat) * (13 : Nat) * (13 : Nat) - (13 : Nat) * (13 : Nat) + (13 : Nat) ∧ ((2041 : Nat) - (1 : Nat)) / (12 : Nat) = (13 : Nat) * (13 : Nat) + (1 : Nat) :=115 @FRC.Ledger.p07007116/-- 7:C4 (p07008) — Space and the causal rays: the $\p+1$ points of $\mathbb{P}^{1}(\Fp)$ are the null directions inside space; the $\p(\p-1)$ others, the finite upper half-plane, carry a time component and are the cone chart. -/117theorem causal_rays : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), (z * FRC.Extension.Ext.conj (1 : FRC.Extension.Ext p ν)).im = z.im) ∧ (FRC.Lorentz.nullCount13 = (2041 : Nat) ∧ (2041 : Nat) = (13 : Nat) * (13 : Nat) * (13 : Nat) - (13 : Nat) * (13 : Nat) + (13 : Nat) ∧ ((2041 : Nat) - (1 : Nat)) / (12 : Nat) = (13 : Nat) * (13 : Nat) + (1 : Nat)) ∧ (13 : Nat) + (1 : Nat) + (13 : Nat) * (12 : Nat) = (13 : Nat) * (13 : Nat) + (1 : Nat) ∧ (173 : Nat) + (1 : Nat) + (173 : Nat) * (172 : Nat) = (173 : Nat) * (173 : Nat) + (1 : Nat) ∧ (1549 : Nat) + (1 : Nat) + (1549 : Nat) * (1548 : Nat) = (1549 : Nat) * (1549 : Nat) + (1 : Nat) :=118 @FRC.Ledger.p07008119set_option linter.defProp false in120/-- 7:C5 (p07009) — Exactly two four-dimensional classes: the frame quadric $(M_{2}(\Fp),\det)$ hyperbolic, the register square elliptic; Lorentzian exactly when $K$ is a field; $(3,1)$ names the elliptic class by the index chart [chart], in signs $(-+++)$ or equally $(+---)$, one class without inertia. -/121def two_classes := @FRC.Ledger.p07009122/-- 7:C6 (p07010) — No inertia: $\langle1,1,1,\gen\rangle\cong\langle1,\gen,\gen,\gen\rangle$; a similitude of multiplier $\gen$ exchanges the two non-null classes; the null cone is the invariant of a change of unit. -/123theorem no_inertia : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b : FRC.Shell p), a * a + b * b = ν → ∀ (x0 x1 x2 x3 : FRC.Shell p), FRC.Lorentz.Q ν (ν * x2) (a * x1 + -(b * x3)) x0 (b * x1 + a * x3) = ν * FRC.Lorentz.Q ν x0 x1 x2 x3) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (i h : FRC.Shell p), i * i = (-1 : FRC.Shell p) → ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * h = (1 : FRC.Shell p) → (ν + (1 : FRC.Shell p)) * h * ((ν + (1 : FRC.Shell p)) * h) + i * ((ν + (-1 : FRC.Shell p)) * h) * (i * ((ν + (-1 : FRC.Shell p)) * h)) = ν :=124 @FRC.Ledger.p07010125set_option linter.defProp false in126/-- 7:C7 (p07031) — The frame's orbits: on the cone, the $\p+1$ null directions of space (Borel stabilisers) and the $\p(\p-1)$ causal rays (torus stabilisers); $\mathrm{SL}_2(\Fp)$ transitive on the rays with stabiliser $C_{\p+1}$, the exact fibration; the Borel a section in $G$, none on the spin cover. -/127def frame_orbits := @FRC.Ledger.p07031128/-- 7:C8 (p07032) — The Hopf base is the set of oriented nonsquare axes of space: a causal ray's stabiliser fixes one nonsquare axis, whose roots are the ray and its conjugate; every direction of space is a root pair on $\mathbb{P}^{1}(K)$; the fibration covers the causal rays only. -/129theorem hopf_base : ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), z.trace * z.trace + -(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.norm) = ν * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.im * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.im)) :=130 @FRC.Ledger.p07032131/-- 7:C9 (p07040) — The class equation: every element of $G$ has order dividing $\p-1$, $\p$ or $\p+1$; the maximal cyclic subgroups are the split tori, the unipotent groups and the non-split tori, $\p(\p+1)/2$, $\p+1$ and $\p(\p-1)/2$ of them, partitioning $G\setminus\{1\}$. -/132theorem class_equation : (FRC.Lorentz.classCounts13 = ((12012 : Nat), (2028 : Nat), (12168 : Nat)) ∧ (12012 : Nat) = (12 : Nat) * ((13 : Nat) * (14 : Nat) * (11 : Nat) / (2 : Nat)) ∧ (2028 : Nat) = (12 : Nat) * ((1 : Nat) + ((13 : Nat) * (13 : Nat) - (1 : Nat))) ∧ (12168 : Nat) = (12 : Nat) * ((13 : Nat) * (13 : Nat) * (12 : Nat) / (2 : Nat)) ∧ (12012 : Nat) + (2028 : Nat) + (12168 : Nat) = (12 : Nat) * ((12 : Nat) * (13 : Nat) * (14 : Nat))) ∧ (1 : Nat) + ((13 : Nat) * (13 : Nat) - (1 : Nat)) + (13 : Nat) * (14 : Nat) * (11 : Nat) / (2 : Nat) + (13 : Nat) * (13 : Nat) * (12 : Nat) / (2 : Nat) = (12 : Nat) * (13 : Nat) * (14 : Nat) ∧ (1 : Nat) + ((173 : Nat) * (173 : Nat) - (1 : Nat)) + (173 : Nat) * (174 : Nat) * (171 : Nat) / (2 : Nat) + (173 : Nat) * (173 : Nat) * (172 : Nat) / (2 : Nat) = (172 : Nat) * (173 : Nat) * (174 : Nat) ∧ (1 : Nat) + ((1549 : Nat) * (1549 : Nat) - (1 : Nat)) + (1549 : Nat) * (1550 : Nat) * (1547 : Nat) / (2 : Nat) + (1549 : Nat) * (1549 : Nat) * (1548 : Nat) / (2 : Nat) = (1548 : Nat) * (1549 : Nat) * (1550 : Nat) ∧ ∀ {p : Nat} [FRC.Pos p] (M : FRC.Shell.Frame.M2 p), M.det = (1 : FRC.Shell p) → ∃ n, (0 : Nat) < n ∧ n ≤ p * (p * (p * p)) ∧ FRC.Spin.mpow M n = FRC.Spin.I :=133 @FRC.Ledger.p07040134/-- 7:C10 (p07051) — The fixed points: a split torus fixes exactly two points of $\mathbb{P}^{1}(\Fp)$, a unipotent group one and a non-split torus none, by the square class of the discriminant; the three kinds of cycle are the three kinds of direction of space, a square-norm axis, a null direction and a nonsquare axis. -/135theorem fixed_points : (FRC.Register.fixedTally13 = ((2183 : Nat), (1001 : Nat), (168 : Nat), (1014 : Nat)) ∧ (1 : Nat) + (1001 : Nat) + (168 : Nat) + (1014 : Nat) = (12 : Nat) * (13 : Nat) * (14 : Nat)) ∧ (FRC.Register.directionCounts13 = ((14 : Nat), (78 : Nat), (91 : Nat)) ∧ (1014 : Nat) = (78 : Nat) * (13 : Nat) ∧ (168 : Nat) = (14 : Nat) * (12 : Nat) ∧ (1001 : Nat) = (91 : Nat) * (11 : Nat) ∧ (14 : Nat) = (13 : Nat) + (1 : Nat) ∧ (78 : Nat) = (13 : Nat) * (12 : Nat) / (2 : Nat) ∧ (91 : Nat) = (13 : Nat) * (14 : Nat) / (2 : Nat)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), z.trace * z.trace + -(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.norm) = ν * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.im * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.im)) :=136 @FRC.Ledger.p07051137set_option linter.defProp false in138/-- 7:D1 (p07011) — The stabiliser of the time vector $\eta J$ in $\mathrm{SL}_2(K)$ is exactly the spin cover $\mathrm{SL}_2(\Fp)$, which acts on $\mathrm{Sym}^{2}(V)$ through $\mathrm{PSL}_2(\Fp)$, of index two in $G$; the moves of odd drive parity lie outside it. -/139def time_stabiliser := @FRC.Ledger.p07011140set_option linter.defProp false in141/-- 7:D3 (p07013) — The drive on the square: $\mathrm{diag}(\gen,1)$ carries $[z]$ to $[\gen z]$ and $\eta J$ to $\gen\,\eta J$; its unimodular lift $\mathrm{diag}(\eta,\eta^{-1})$ carries $\eta J$ to $-\eta J$; the even transport $\mathrm{diag}(\gen,\gen^{-1})$ fixes $\eta J$ and dilates the origin and the antipode by $\gen^{-2}$ and $\gen^{2}$. -/142def drive_on_square := @FRC.Ledger.p07013143set_option linter.defProp false in144/-- 7:D4 (p07014) — $N^{1}$ and the non-split torus are conjugate in $\mathrm{SL}_2(K)$; the spinor closes in two circuits, of order $\p+1$ in $\mathrm{SL}_2(K)$ and $(\p+1)/2$ on the square. -/145def torus_conjugate := @FRC.Ledger.p07014146set_option linter.defProp false in147/-- 7:D6 (p07033) — $K^{\times}/\Fpx$ is regular on $\mathbb{P}^{1}(\Fp)$; the antipode $[1:0]$ is its element of order two, reached from the origin at the half step $2\kap+1$ by every generator; the unimodular torus reaches only the even steps. -/148def antipode_half_step := @FRC.Ledger.p07033149/-- 7:F1 (p07044) — Every embedded shell drifts against its own chart of the Carrier by $1/(\Om-1)$ of the cycle per chronon and $\kap/\dS$ per revolution, below $1/(\sqrt{\Om}+1)$ exactly when $\p^{2}<\Om$ [chart]; the cycle's order $\Om-1$ is the same for every Subject, and no rate between two Subjects is defined. -/150theorem shell_drifts : ∀ {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 :=151 @FRC.Ledger.p07044152/-- 7:F3 (p07046) — The time reversal is not a Lorentz move: the congruence image is $\Omega^{-}_{4}(\p)$, of index four in $\mathrm{O}^{-}_{4}(\p)$; the time reversal is the Frobenius of $K$, and it, a spatial reflection and the total inversion lie outside the image. -/153theorem no_time_reversal : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (-1 : FRC.Shell p) (0 : FRC.Shell p) → False) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (-1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) → False) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (-1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (-1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (-1 : FRC.Shell p) → False) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → ∀ (x0 x1 x2 x3 : FRC.Shell p), (FRC.Lorentz.cong A (FRC.Lorentz.X x0 x1 x2 x3)).det = FRC.Extension.Ext.ofShell (FRC.Lorentz.Q ν x0 x1 x2 x3) :=154 @FRC.Ledger.p07046155/-- 7:F4 (p07047) — The drift is one-directional: one chronon is one step of the Carrier's chart cycle, a registered duration has at most $\p^{2}<\Om-1$ chronons, so the chart count is injective on every registrable depth and no recurrence is registrable; on a hosted Carrier the pair returns after $\mathrm{lcm}(4\kap,4\dS)$ chronons, the laboratory's period. -/156theorem one_directional_drift : (∀ (Om n : Nat), n < Om - (1 : Nat) → n % (Om - (1 : Nat)) = n) ∧ (∀ (p S n : Nat), p % (2 : Nat) = (1 : Nat) → p * p < (4 : Nat) * S + (1 : Nat) → n ≤ p * p → n < (4 : Nat) * S + (1 : Nat) - (1 : Nat)) ∧ ((13 : Nat) * (13 : Nat) < (232 : Nat) ∧ (173 : Nat) * (173 : Nat) < (30088 : Nat) ∧ (1549 : Nat) * (1549 : Nat) < (2408560 : Nat) ∧ (13 : Nat) * (13 : Nat) < (180 : Nat) ∧ (13 : Nat) * (13 : Nat) < (696 : Nat) ∧ (173 : Nat) * (173 : Nat) < (1293784 : Nat) ∧ (1549 : Nat) * (1549 : Nat) < (932112720 : Nat) ∧ (13 : Nat) * (13 : Nat) < (180 : Nat)) ∧ (∀ (κ S a b : Nat), (0 : Nat) < S → a * κ = b * S + (1 : Nat) → (∃ x, (4 : Nat) * κ * S = (4 : Nat) * κ * x) ∧ (∃ y, (4 : Nat) * κ * S = (4 : Nat) * S * y) ∧ ∀ (L x y : Nat), L = (4 : Nat) * κ * x → L = (4 : Nat) * S * y → ∃ z, L = (4 : Nat) * κ * S * z) ∧ (∀ (κ S n m a b : Nat), (0 : Nat) < S → a * κ = b * S + (1 : Nat) → n < S → m < S → (4 : Nat) * κ * n % ((4 : Nat) * S) = (4 : Nat) * κ * m % ((4 : Nat) * S) → n = m) ∧ (∀ (κ' S' d n m a b : Nat), (0 : Nat) < d → (0 : Nat) < S' → a * κ' = b * S' + (1 : Nat) → n < S' → m < S' → (4 : Nat) * (d * κ') * n % ((4 : Nat) * (d * S')) = (4 : Nat) * (d * κ') * m % ((4 : Nat) * (d * S')) → n = m) ∧ (((39 : Nat) * (3 : Nat) = (2 : Nat) * (58 : Nat) + (1 : Nat) ∧ (4 : Nat) * (3 : Nat) * (58 : Nat) = (696 : Nat)) ∧ ((5073 : Nat) * (43 : Nat) = (29 : Nat) * (7522 : Nat) + (1 : Nat) ∧ (4 : Nat) * (43 : Nat) * (7522 : Nat) = (1293784 : Nat)) ∧ (395203 : Nat) * (387 : Nat) = (254 : Nat) * (602140 : Nat) + (1 : Nat) ∧ (4 : Nat) * (387 : Nat) * (602140 : Nat) = (932112720 : Nat)) ∧ (3 : Nat) = (3 : Nat) * (1 : Nat) ∧ (45 : Nat) = (3 : Nat) * (15 : Nat) ∧ (1 : Nat) * (1 : Nat) = (0 : Nat) * (15 : Nat) + (1 : Nat) ∧ (4 : Nat) * (3 : Nat) * (45 : Nat) / (3 : Nat) = (180 : Nat) ∧ (13 : Nat) * (13 : Nat) < (181 : Nat) :=157 @FRC.Ledger.p07047158/-- 7:F5 (p07052) — The second law of the record: along a registrable duration the record gains one chart count per chronon, its entries pairwise distinct, and no count recurs below $\Om-1$; its entropy $S_{\mathrm{th}}(n)=k_B\,n$ [chart] never decreases on a registrable duration; the record holds at most $\p^{2}=4\kap(\p+1)+1$ entries, the $\kap(\p+1)$ orbits of the quarter-turn group on the nonzero pair states plus the origin. -/159theorem second_law : (∀ (Om n m : Nat), m < Om - (1 : Nat) → n < m → n % (Om - (1 : Nat)) < m % (Om - (1 : Nat))) ∧ (∀ (k : Nat), ((4 : Nat) * k + (1 : Nat)) * ((4 : Nat) * k + (1 : Nat)) = (4 : Nat) * (k * ((4 : Nat) * k + (1 : Nat) + (1 : Nat))) + (1 : Nat)) ∧ ((13 : Nat) * (13 : Nat) = (4 : Nat) * ((3 : Nat) * (14 : Nat)) + (1 : Nat) ∧ (173 : Nat) * (173 : Nat) = (4 : Nat) * ((43 : Nat) * (174 : Nat)) + (1 : Nat) ∧ (1549 : Nat) * (1549 : Nat) = (4 : Nat) * ((387 : Nat) * (1550 : Nat)) + (1 : Nat) ∧ (13 : Nat) * (13 : Nat) < (233 : Nat) - (1 : Nat) ∧ (173 : Nat) * (173 : Nat) < (30089 : Nat) - (1 : Nat) ∧ (1549 : Nat) * (1549 : Nat) < (2408561 : Nat) - (1 : Nat)) ∧ (∀ (Om n : Nat), n < Om - (1 : Nat) → n % (Om - (1 : Nat)) = n) ∧ ∀ (p S n : Nat), p % (2 : Nat) = (1 : Nat) → p * p < (4 : Nat) * S + (1 : Nat) → n ≤ p * p → n < (4 : Nat) * S + (1 : Nat) - (1 : Nat) :=160 @FRC.Ledger.p07052161set_option linter.defProp false in162/-- 7:X1 (p07020) — Why Lorentzian: a finite four-geometry is hyperbolic or elliptic, and the register square is elliptic because time's coefficient is the drive's generator, a nonsquare. -/163def why_lorentzian := @FRC.Ledger.p07020164/-- 7:X2 (p07021) — Why three spatial dimensions: space is $\mathrm{Sym}^{2}(V)$, of dimension three, and the frame moves have exactly three cyclic symmetries, the three kinds of direction of that space. -/165theorem why_three_dimensions : (FRC.Lorentz.classCounts13 = ((12012 : Nat), (2028 : Nat), (12168 : Nat)) ∧ (12012 : Nat) = (12 : Nat) * ((13 : Nat) * (14 : Nat) * (11 : Nat) / (2 : Nat)) ∧ (2028 : Nat) = (12 : Nat) * ((1 : Nat) + ((13 : Nat) * (13 : Nat) - (1 : Nat))) ∧ (12168 : Nat) = (12 : Nat) * ((13 : Nat) * (13 : Nat) * (12 : Nat) / (2 : Nat)) ∧ (12012 : Nat) + (2028 : Nat) + (12168 : Nat) = (12 : Nat) * ((12 : Nat) * (13 : Nat) * (14 : Nat))) ∧ (1 : Nat) + ((13 : Nat) * (13 : Nat) - (1 : Nat)) + (13 : Nat) * (14 : Nat) * (11 : Nat) / (2 : Nat) + (13 : Nat) * (13 : Nat) * (12 : Nat) / (2 : Nat) = (12 : Nat) * (13 : Nat) * (14 : Nat) ∧ (1 : Nat) + ((173 : Nat) * (173 : Nat) - (1 : Nat)) + (173 : Nat) * (174 : Nat) * (171 : Nat) / (2 : Nat) + (173 : Nat) * (173 : Nat) * (172 : Nat) / (2 : Nat) = (172 : Nat) * (173 : Nat) * (174 : Nat) ∧ (1 : Nat) + ((1549 : Nat) * (1549 : Nat) - (1 : Nat)) + (1549 : Nat) * (1550 : Nat) * (1547 : Nat) / (2 : Nat) + (1549 : Nat) * (1549 : Nat) * (1548 : Nat) / (2 : Nat) = (1548 : Nat) * (1549 : Nat) * (1550 : Nat) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (z : FRC.Extension.Ext p ν), z.trace * z.trace + -(((1 : FRC.Shell p) + (1 : FRC.Shell p)) * ((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.norm) = ν * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.im * (((1 : FRC.Shell p) + (1 : FRC.Shell p)) * z.im)) :=166 @FRC.Ledger.p07021167/-- 7:X4 (p07023) — Why spin one half: the kernel of the congruence is $\pm I$ and the spinor closes in two circuits. -/168theorem why_spin_half : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) → A = FRC.Lorentz.diagx (1 : FRC.Extension.Ext p ν) (1 : FRC.Extension.Ext p ν) ∨ A = FRC.Lorentz.diagx (-1 : FRC.Extension.Ext p ν) (-1 : FRC.Extension.Ext p ν)) ∧ ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (x0 x1 x2 x3 : FRC.Shell p), FRC.Lorentz.cong (FRC.Lorentz.diagx (-1 : FRC.Extension.Ext p ν) (-1 : FRC.Extension.Ext p ν)) (FRC.Lorentz.X x0 x1 x2 x3) = FRC.Lorentz.X x0 x1 x2 x3 :=169 @FRC.Ledger.p07023170/-- 7:X5 (p07024) — Why time is relational: there is no inertia, and a change of unit exchanges the label. -/171theorem why_time_relational : ∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p} (a b : FRC.Shell p), a * a + b * b = ν → ∀ (x0 x1 x2 x3 : FRC.Shell p), FRC.Lorentz.Q ν (ν * x2) (a * x1 + -(b * x3)) x0 (b * x1 + a * x3) = ν * FRC.Lorentz.Q ν x0 x1 x2 x3 :=172 @FRC.Ledger.p07024173/-- 7:X6 (p07048) — Why causality has an arrow: every embedded shell's chart count is a one-directional count on a cycle of one order for every observer, it orders the shell's revolutions, and the time reversal is not a Lorentz move. -/174theorem why_arrow : (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (-1 : FRC.Shell p) (0 : FRC.Shell p) → False) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (-1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) → False) ∧ (∀ {p : Nat} [FRC.Pos p] {ν : FRC.Shell p}, FRC.Shell.Frame.Fld p → (¬∃ y, y * y = ν) → (1 : FRC.Shell p) + (1 : FRC.Shell p) ≠ (0 : FRC.Shell p) → ∀ (A : FRC.Spin.M2x p ν), A.det = (1 : FRC.Extension.Ext p ν) → FRC.Lorentz.cong A (FRC.Lorentz.X (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (-1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (-1 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) → FRC.Lorentz.cong A (FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (1 : FRC.Shell p)) = FRC.Lorentz.X (0 : FRC.Shell p) (0 : FRC.Shell p) (0 : FRC.Shell p) (-1 : FRC.Shell p) → False) ∧ ∀ (Om n : Nat), n < Om - (1 : Nat) → n % (Om - (1 : Nat)) = n :=175 @FRC.Ledger.p07048176/-- 7:P1 (p07026) — Exactly three spatial dimensions at every scale the Subject registers, read through the declared metric chart. Falsifier: a short-range departure from the inverse-square law of the extra-dimension form; holds to $52\,\mu$m [data]. -/177theorem three_dimensions : (∀ {p : Nat} [FRC.Pos p], FRC.Shell.Frame.Fld 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) ∧ ∀ (κ : Nat), (4 : Nat) * κ + (1 : Nat) - (1 : Nat) = (4 : Nat) * κ ∧ (4 : Nat) * κ + (1 : Nat) + (1 : Nat) = (4 : Nat) * κ + (2 : Nat) :=178 @FRC.Ledger.p07026179/-- 7:P2 (p07054) — The floor is the Carrier's temperature: the de Sitter temperature of the Carrier's horizon, $T_{\mathrm{dS}}=\hbar H_{0}/2\pi k_B$, and the floor $a_{0}=cH_{0}/2\pi$ are one number in the acceleration domain, $k_BT_{\mathrm{dS}}=(\hbar/c)\,a_{0}$ with $|k_B|=\hbar/c$ the chart's unit [chart]: $2.66\times10^{-30}$ K and $1.04\times10^{-10}$ m\,s$^{-2}$ at $H_{0}=67.4$. Falsifier: a measured floor that departs from $cH_{0}/2\pi$. -/180theorem floor_is_temperature : (∀ (kB c hbar H : Nat), kB * c = hbar → kB * (c * H) = hbar * H) ∧ (124 : Nat) * (159 : Nat) % (233 : Nat) = (144 : Nat) ∧ (144 : Nat) * (144 : Nat) % (233 : Nat) = (232 : Nat) ∧ (124 : Nat) * (124 : Nat) % (233 : Nat) = (231 : Nat) ∧ (2567 : Nat) * (27765 : Nat) % (30089 : Nat) = (22003 : Nat) ∧ (22003 : Nat) * (22003 : Nat) % (30089 : Nat) = (30088 : Nat) ∧ (2567 : Nat) * (2567 : Nat) % (30089 : Nat) = (30087 : Nat) ∧ (1880160 : Nat) * (2237455 : Nat) % (2408561 : Nat) = (18688 : Nat) ∧ (18688 : Nat) * (18688 : Nat) % (2408561 : Nat) = (2408560 : Nat) ∧ (1880160 : Nat) * (1880160 : Nat) % (2408561 : Nat) = (2408559 : Nat) :=181 @FRC.Ledger.p07054182-- end ledger predicates183184end FRC.Spacetime185