Dimensions.lean — FrcCore

1import FrcCore.Frame2import FrcCore.Orbit3import FrcCore.Sum4import FrcCore.Instances5import FrcCore.Poly6import FrcCore.Meridian78/-!9# 10-dimensions — the domain lattice, the unit flag and the Carrier residues, no axioms1011The modular unit-domain labels `U_{r,s} = [L]^r [T]^s` of *Dimensional Analysis over Finite Holographic12Substrate* as pairs of residues `(r mod p, s mod 4κ)`, `p = 4κ + 1`: the group law, inverses and powers13(10:C2, the monomial half of C3); the chart duality `δ_S` and the crossed duality `δ_C` as involutions (D1);14the unit flag `I_q = (0, κ)` — `I_q⁴ = 1`, `I_q² = [T]^π`, `I_q, I_q², I_q³ ≠ 1`, no flag of space on a15framed shell (`4r = 0 ⇒ r = 0`), the half-period as the one element of order two, meridian transport16`([L][T]^κ)^p = I_q` (D2, C6); the record `s ↦ I_q^s` with its values (D3); the flagged readings `[E]`, `[p]`,17`[S]`, the phase counts neutral, the horizon inaccessibility of the flag on `𝔽₁₃` (D6); the Carrier face —18the linear pin `2G + 1 = 0 ⇒ G = 2S`, the root pairs, the linkage `(k_B c)² = −1 ⇒ k_B c = ±ħ` and the pair19consequences on every framed Carrier (E4, E5); the two Carriers `233` and `2 408 561` decided by the kernel20(E4, E5); the minimality scan certifying `(13, 233)` with its counterfactuals (E9); the derived domains21realized on `𝔽₁₃` and the energy–momentum relation among them (F2–F4, G3); the charge label, its two values and22its absence on the even capacities (F5); the window ladder by integer squares (G2); the roundings of the resolution floor on the23chart value, its bits and the clock-bound crossover (G5, P1); the linear pin and the root pair as the content of the constancy24prediction (P2). Every declaration is checked to depend on no axiom (`check_core_axioms.py`).2526Since the ledger migration (task LM17) `isPrime` lives in `Nat.lean`, the root pair and the bounded quantifiers'27deciders in `Frame.lean`; every old name stays as an alias.28-/2930namespace FRC.Dimensions3132open FRC.Shell33open FRC.Nat (isPrime)34open FRC.Shell.Frame (root_pair)3536/-! ## The domain lattice as pairs of residues (10:C1, C2, C3) -/3738/-- 10:C1 — a modular unit-domain label `U_{r,s}`: the space exponent `r` in `C_p`, the time exponent `s`39in `C_n` (`n = p − 1 = 4κ`). -/40structure Dom (p n : Nat) where41  r : Shell p42  s : Shell n4344namespace Dom4546variable {p n : Nat}4748theorem ext {a b : Dom p n} (hr : a.r = b.r) (hs : a.s = b.s) : a = b := by49  cases a; cases b; cases hr; cases hs; rfl5051theorem r_congr {a b : Dom p n} (h : a = b) : a.r = b.r := by cases h; rfl52theorem s_congr {a b : Dom p n} (h : a = b) : a.s = b.s := by cases h; rfl5354instance : DecidableEq (Dom p n) := fun a b =>55  if h : a.r = b.r ∧ a.s = b.s then isTrue (ext h.1 h.2)56  else isFalse (fun e => h ⟨r_congr e, s_congr e⟩)5758variable [Pos p] [Pos n]5960/-- 10:C2 — the product of labels adds the exponents: `U_{r,s} U_{r',s'} = U_{r+r', s+s'}`. -/61def mul (a b : Dom p n) : Dom p n := ⟨a.r + b.r, a.s + b.s⟩62instance : Mul (Dom p n) := ⟨mul⟩6364/-- 10:C2 — the neutral label `U_{0,0} = 1`. -/65def one : Dom p n := ⟨0, 0⟩66instance : One (Dom p n) := ⟨one⟩6768/-- 10:C2, 10:D1 — the inverse label `U_{r,s}⁻¹ = U_{−r,−s}`, the chart duality `δ_S`. -/69def inv (a : Dom p n) : Dom p n := ⟨-a.r, -a.s⟩70instance : Inv (Dom p n) := ⟨inv⟩7172/-- Powers by structural recursion. -/73def pow (a : Dom p n) : Nat → Dom p n74  | 0 => 175  | k + 1 => pow a k * a76instance : Pow (Dom p n) Nat := ⟨pow⟩7778theorem mul_def (a b : Dom p n) : a * b = ⟨a.r + b.r, a.s + b.s⟩ := rfl79theorem one_def : (1 : Dom p n) = ⟨0, 0⟩ := rfl80theorem inv_def (a : Dom p n) : a⁻¹ = ⟨-a.r, -a.s⟩ := rfl81theorem pow_zero (a : Dom p n) : a ^ 0 = 1 := rfl82theorem pow_succ (a : Dom p n) (k : Nat) : a ^ (k + 1) = a ^ k * a := rfl8384/-- 10:C2 — the label group is abelian: commutativity. -/85theorem mul_comm (a b : Dom p n) : a * b = b * a :=86  ext (Shell.add_comm _ _) (Shell.add_comm _ _)8788/-- 10:C2 — associativity. -/89theorem mul_assoc (a b c : Dom p n) : a * b * c = a * (b * c) :=90  ext (Shell.add_assoc _ _ _) (Shell.add_assoc _ _ _)9192/-- 10:C2 — the unit. -/93theorem one_mul (a : Dom p n) : 1 * a = a := ext (Shell.zero_add _) (Shell.zero_add _)94theorem mul_one (a : Dom p n) : a * 1 = a := ext (Shell.add_zero _) (Shell.add_zero _)9596/-- 10:C2 — the inverse: `U_{r,s} U_{−r,−s} = 1`. -/97theorem mul_inv (a : Dom p n) : a * a⁻¹ = 1 := ext (Shell.add_neg _) (Shell.add_neg _)98theorem inv_mul (a : Dom p n) : a⁻¹ * a = 1 := ext (Shell.neg_add _) (Shell.neg_add _)99100/-- 10:D1 — the chart duality `δ_S : D ↦ D⁻¹` is an involution. -/101theorem inv_inv (a : Dom p n) : a⁻¹⁻¹ = a := ext (Shell.neg_neg _) (Shell.neg_neg _)102103/-- 10:C2, 10:C3 — the grading: `U_a^{k+l} = U_a^k U_a^l`. -/104theorem pow_add (a : Dom p n) (k l : Nat) : a ^ (k + l) = a ^ k * a ^ l := by105  induction l with106  | zero => rw [Nat.add_zero, pow_zero, mul_one]107  | succ l ih => rw [Nat.add_succ, pow_succ, ih, pow_succ, mul_assoc]108109/-- 10:C3 — the domain of a power is the multiple of the label: `U_{r,s}^k = U_{kr, ks}`; so the domain110of a monomial `∏ U_{a_j}^{k_j}` is `Σ k_j a_j`, and the monomial is neutral iff that sum is `(0, 0)`. -/111theorem pow_eq (a : Dom p n) (k : Nat) : a ^ k = ⟨ofNat k * a.r, ofNat k * a.s⟩ := by112  induction k with113  | zero =>114    refine ext ?_ ?_115    · show (0 : Shell p) = ofNat 0 * a.r116      rw [show (ofNat 0 : Shell p) = 0 from rfl, Shell.zero_mul]117    · show (0 : Shell n) = ofNat 0 * a.s118      rw [show (ofNat 0 : Shell n) = 0 from rfl, Shell.zero_mul]119  | succ k ih =>120    rw [pow_succ, ih, mul_def, ofNat_succ, ofNat_succ, Shell.right_distrib, Shell.right_distrib,121      Shell.one_mul, Shell.one_mul]122123/-- 10:C3 — the product of powers: `(U_a U_b)^k = U_a^k U_b^k`. -/124theorem mul_pow (a b : Dom p n) (k : Nat) : (a * b) ^ k = a ^ k * b ^ k := by125  rw [pow_eq, pow_eq, pow_eq, mul_def]126  exact ext (Shell.left_distrib _ _ _) (Shell.left_distrib _ _ _)127128end Dom129130/-! ## Bounded universal quantifiers, decided by search (no axioms) -/131132/-- `∀ x : Dom p n, P x`, decided componentwise. -/133instance instDecForallDom {p n : Nat} [Pos p] [Pos n] (P : Dom p n → Prop) [DecidablePred P] :134    Decidable (∀ x, P x) :=135  match (inferInstance : Decidable (∀ r : Shell p, ∀ s : Shell n, P ⟨r, s⟩)) with136  | isTrue h => isTrue (fun x => match x with | ⟨r, s⟩ => h r s)137  | isFalse h => isFalse (fun hall => h (fun r s => hall ⟨r, s⟩))138139/-! ## The generators and the flag on the shell of capacity `κ` (10:D2, C6, D3, D6) -/140section shell141142variable (κ : Nat) [Pos κ]143144instance instPosFour : Pos (4 * κ) := ⟨Nat.mul_pos (Nat.zero_lt_succ 3) Pos.pos⟩145146/-- The lattice of the shell of capacity `κ`: `D_p = C_{4κ+1} × C_{4κ}`. -/147abbrev DomK := Dom (4 * κ + 1) (4 * κ)148149/-- 10:C1 — the space generator `[L] = (1, 0)`. -/150def L : DomK κ := ⟨1, 0⟩151/-- 10:C1 — the time generator `[T] = (0, 1)`. -/152def T : DomK κ := ⟨0, 1⟩153/-- 10:D2 — the unit flag `I_q = [T]^κ = (0, κ)`. -/154def flag : DomK κ := ⟨0, ofNat κ⟩155/-- 10:D6 — the energy domain `[E] = I_q [T]⁻¹`. -/156def energy : DomK κ := flag κ * (T κ)⁻¹157/-- 10:D6 — the momentum domain `[p] = I_q [L]⁻¹`. -/158def mom : DomK κ := flag κ * (L κ)⁻¹159/-- 10:D1 — the crossed duality `δ_C = I_q δ_S : D ↦ I_q D⁻¹`. -/160def deltaC (a : DomK κ) : DomK κ := flag κ * a⁻¹161162/-- 10:D2 — `I_q = [T]^κ`. -/163theorem flag_eq_pow : T κ ^ κ = flag κ := by164  rw [Dom.pow_eq]165  exact Dom.ext (by show ofNat κ * 0 = 0; exact Shell.mul_zero _)166    (by show ofNat κ * 1 = ofNat κ; exact Shell.mul_one _)167168/-- `ofNat (m·κ)` in `C_{4κ}` has representative `m·κ` for `m < 4`. -/169theorem val_ofNat_mul_kappa (m : Nat) (hm : m < 4) : (ofNat (m * κ) : Shell (4 * κ)).val = m * κ :=170  FRC.Nat.mod_eq_of_lt (FRC.Nat.mul_lt_mul_of_lt_of_pos hm Pos.pos)171172theorem ofNat_kappa_ne_zero : (ofNat κ : Shell (4 * κ)) ≠ 0 := fun h => by173  have hv := val_injective h174  rw [show ofNat κ = (ofNat (1 * κ) : Shell (4 * κ)) by rw [Nat.one_mul],175    val_ofNat_mul_kappa κ 1 (by decide), Nat.one_mul, val_zero] at hv176  exact Nat.ne_of_gt Pos.pos hv177178theorem ofNat_two_kappa_ne_zero : (ofNat (2 * κ) : Shell (4 * κ)) ≠ 0 := fun h => by179  have hv := val_injective h180  rw [val_ofNat_mul_kappa κ 2 (by decide), val_zero] at hv181  exact Nat.ne_of_gt (Nat.mul_pos (Nat.zero_lt_succ 1) Pos.pos) hv182183theorem ofNat_three_kappa_ne_zero : (ofNat (3 * κ) : Shell (4 * κ)) ≠ 0 := fun h => by184  have hv := val_injective h185  rw [val_ofNat_mul_kappa κ 3 (by decide), val_zero] at hv186  exact Nat.ne_of_gt (Nat.mul_pos (Nat.zero_lt_succ 2) Pos.pos) hv187188/-- `4κ ≡ 0` in `C_{4κ}`. -/189theorem ofNat_four_kappa : (ofNat (4 * κ) : Shell (4 * κ)) = 0 := FRC.Shell.Frame.ofNat_self190191theorem flag_pow (m : Nat) : flag κ ^ m = ⟨0, ofNat (m * κ)⟩ := by192  rw [Dom.pow_eq]193  exact Dom.ext (by show ofNat m * 0 = 0; exact Shell.mul_zero _)194    (by show ofNat m * ofNat κ = ofNat (m * κ); rw [Frame.ofNat_mul])195196/-- 10:D2 — `I_q⁴ = 1`. -/197theorem flag_pow_four : flag κ ^ 4 = 1 := by198  rw [flag_pow, ofNat_four_kappa]; rfl199200/-- 10:D2, 10:X3 — `I_q² = [T]^π`, the half-period `π = 2κ`, and `I_q, I_q², I_q³ ≠ 1`: the flag has order four. -/201theorem flag_order_four :202    flag κ ^ 2 = T κ ^ (2 * κ) ∧ flag κ ^ 1 ≠ 1 ∧ flag κ ^ 2 ≠ 1 ∧ flag κ ^ 3 ≠ 1 := by203  refine ⟨?_, fun h => ?_, fun h => ?_, fun h => ?_⟩204  · rw [flag_pow, Dom.pow_eq]205    exact Dom.ext (by show (0 : Shell (4 * κ + 1)) = ofNat (2 * κ) * 0; rw [Shell.mul_zero])206      (by show ofNat (2 * κ) = ofNat (2 * κ) * 1; rw [Shell.mul_one])207  · rw [flag_pow, Nat.one_mul] at h; exact ofNat_kappa_ne_zero κ (Dom.s_congr h)208  · rw [flag_pow] at h; exact ofNat_two_kappa_ne_zero κ (Dom.s_congr h)209  · rw [flag_pow] at h; exact ofNat_three_kappa_ne_zero κ (Dom.s_congr h)210211/-- 10:D2 — the conjugate generator `I_q⁻¹ = I_q³ = (0, 3κ)`. -/212theorem flag_inv : (flag κ)⁻¹ = flag κ ^ 3 := by213  rw [flag_pow, Dom.inv_def]214  refine Dom.ext (Shell.neg_zero) ?_215  show -(ofNat κ) = ofNat (3 * κ)216  apply Shell.neg_eq_of_add_eq_zero217  have h4 : 4 * κ = 3 * κ + κ := Nat.succ_mul 3 κ218  rw [Frame.ofNat_add, Nat.add_comm, ← h4, ofNat_four_kappa]219220omit [Pos κ] in221/-- 10:D2, 10:X3 — no flag of space on a framed shell: `4r = 0` forces `r = 0` (`2 ≠ 0` and no zero divisors), so222the meridian factor contributes no element of order four; and `2r = 0` forces `r = 0`. -/223theorem no_flag_of_space {g : Shell (4 * κ + 1)} (F : Frame (4 * κ + 1) κ g) (r : Shell (4 * κ + 1))224    (h : (2 * 2 : Shell (4 * κ + 1)) * r = 0) : r = 0 := by225  rw [Shell.mul_assoc] at h226  exact F.no_south_pole _ (F.no_south_pole _ h)227228/-- 10:D2 — the order-two element: `2s = 0` in `C_{4κ}` iff `s ∈ {0, 2κ}` — decided on `κ = 3` for every229residue; the general law is `two_smul_flag` of the Mathlib module. -/230theorem order_two_13 :231    ∀ s : Shell 12, (2 : Shell 12) * s = 0 ↔ (s = 0 ∨ s = 6) := by decide +kernel232233/-- 10:D2, 10:X3 — the elements of order four of `D_13 = C_13 × C_12` are exactly `(0, 3)` and `(0, 9)`: the flag234and its conjugate, both in the time factor (exhaustive over the `156` labels). -/235theorem order_four_13 :236    ∀ x : DomK 3, (x ^ 4 = 1 ∧ x ^ 2 ≠ 1) ↔ (x = flag 3 ∨ x = (flag 3)⁻¹) := by decide +kernel237238/-- 10:D2, 10:C6 — meridian transport onto the flag: `([L][T]^κ)^p = I_q` — the meridian component wraps,239`p ≡ 0 (mod p)`, and the phase component advances by `pκ = κ + κ·4κ ≡ κ (mod 4κ)`; for every capacity. -/240theorem meridian_transport : (L κ * T κ ^ κ) ^ (4 * κ + 1) = flag κ := by241  rw [flag_eq_pow, Dom.pow_eq]242  refine Dom.ext ?_ ?_243  · show ofNat (4 * κ + 1) * (1 + 0) = 0244    rw [Shell.add_zero, Shell.mul_one]; exact FRC.Shell.Frame.ofNat_self245  · show ofNat (4 * κ + 1) * (0 + ofNat κ) = ofNat κ246    rw [Shell.zero_add, Frame.ofNat_mul, FRC.Nat.add_mul (4 * κ) 1 κ, Nat.one_mul,247      Nat.mul_comm (4 * κ) κ, Nat.add_comm]248    exact ofNat_add_mul_self κ κ249  where250  ofNat_add_mul_self (a : Nat) : ∀ m : Nat, (ofNat (a + m * (4 * κ)) : Shell (4 * κ)) = ofNat a251    | 0 => by rw [Nat.zero_mul, Nat.add_zero]252    | m + 1 => by253      rw [FRC.Nat.add_mul m 1 (4 * κ), Nat.one_mul, ← Nat.add_assoc, FRC.Shell.Frame.ofNat_add_self,254        ofNat_add_mul_self a m]255256/-- 10:D1 — the crossed duality is an involution, `δ_C(δ_C D) = D`, and carries `[L] ↦ [p]`, `[T] ↦ [E]`. -/257theorem deltaC_involutive (a : DomK κ) :258    deltaC κ (deltaC κ a) = a ∧ deltaC κ (L κ) = mom κ ∧ deltaC κ (T κ) = energy κ := by259  refine ⟨?_, rfl, rfl⟩260  unfold deltaC261  refine Dom.ext ?_ ?_262  · show (0 : Shell (4 * κ + 1)) + -(0 + -a.r) = a.r263    rw [Shell.zero_add, Shell.zero_add, Shell.neg_neg]264  · show ofNat κ + -(ofNat κ + -a.s) = a.s265    rw [Shell.neg_add_rev, Shell.neg_neg, ← Shell.add_assoc, Shell.add_neg, Shell.zero_add]266267/-- 10:D3 — the record `s ↦ I_q^s` on `s = 0, 1, 2, 3` takes the four values `1, (0, κ), (0, 2κ), (0, 3κ)`268of the flag subgroup, and returns to `1` at `s = 4`; its values at `0` and `2` are the parity subgroup, the269chart shadow of the four-cycle. -/270theorem record_values :271    flag κ ^ 0 = 1 ∧ flag κ ^ 1 = ⟨0, ofNat κ⟩ ∧ flag κ ^ 2 = ⟨0, ofNat (2 * κ)⟩ ∧272    flag κ ^ 3 = ⟨0, ofNat (3 * κ)⟩ ∧ flag κ ^ 4 = 1 ∧ flag κ ^ 2 * flag κ ^ 2 = 1 := by273  refine ⟨rfl, by rw [flag_pow, Nat.one_mul], flag_pow κ 2, flag_pow κ 3, flag_pow_four κ, ?_⟩274  rw [← Dom.pow_add]; exact flag_pow_four κ275276/-- 10:D6 — the flagged readings: `[E] = (0, κ − 1)` one capacity step above the count, `[p] = (−1, κ)`,277the action `[S] = [E][T] = I_q`, and the phase counts neutral, `[E][T] I_q⁻¹ = 1`, `[p][L] I_q⁻¹ = 1`. -/278theorem flagged_readings :279    energy κ = ⟨0, ofNat κ + -1⟩ ∧ mom κ = ⟨-1, ofNat κ⟩ ∧ energy κ * T κ = flag κ ∧280    energy κ * T κ * (flag κ)⁻¹ = 1 ∧ mom κ * L κ * (flag κ)⁻¹ = 1 := by281  have h3 : energy κ * T κ = flag κ := by282    unfold energy; rw [Dom.mul_assoc, Dom.inv_mul, Dom.mul_one]283  have h5 : mom κ * L κ = flag κ := by284    unfold mom; rw [Dom.mul_assoc, Dom.inv_mul, Dom.mul_one]285  refine ⟨?_, ?_, h3, ?_, ?_⟩286  · exact Dom.ext (by show (0 : Shell (4 * κ + 1)) + -0 = 0; rw [Shell.neg_zero, Shell.add_zero]) rfl287  · refine Dom.ext (by show (0 : Shell (4 * κ + 1)) + -1 = -1; rw [Shell.zero_add]) ?_288    show ofNat κ + -0 = ofNat κ289    rw [Shell.neg_zero, Shell.add_zero]290  · rw [h3, Dom.mul_inv]291  · rw [h5, Dom.mul_inv]292293end shell294295/-! ## The Carrier face: the defining congruences at pair level (10:E4, 10:E5) -/296section carrier297298variable {Ω : Nat} [Pos Ω] {S : Nat} {g : Shell Ω}299300/-- 10:E4, 10:P2 — the linear pin: on a framed Carrier `Ω = 4S + 1`, `2G + 1 = 0` has the unique solution301`G = 2S`, the half-cycle. -/302theorem G_unique (F : Frame Ω S g) (x : Shell Ω) : 2 * x + 1 = 0 ↔ x = ofNat (2 * S) := by303  have hΩ : (ofNat (4 * S + 1) : Shell Ω) = 0 := by rw [← F.cap]; exact FRC.Shell.Frame.ofNat_self304  have h2S : (2 : Shell Ω) * ofNat (2 * S) + 1 = 0 := by305    rw [Frame.two_mul', Frame.ofNat_add, show (1 : Shell Ω) = ofNat 1 from rfl, Frame.ofNat_add,306      ← Nat.two_mul, ← FRC.Nat.mul_assoc]307    exact hΩ308  constructor309  · intro h310    apply F.mul_left_cancel F.two_ne_zero311    apply Shell.add_right_cancel (c := 1)312    rw [h, h2S]313  · intro h; rw [h]; exact h2S314315/-- 10:E4, 10:E5 — the linkage at pair level and the pair consequences, on a framed Carrier: from316`2G + 1 = 0`, `2c² = 1`, `ħ² = −1`, `k_B² = −2`: `(k_B c)² = −1`, so `k_B c = ħ` or `k_B c = −ħ`317(`{±k_B}{±c} = {±ħ}`); `G = −c²`; `(2G)² = 1`; `ħ⁴ = 1`; and `(ħ c)² = −2 G²`, the monomial face. -/318theorem linkage (F : Frame Ω S g) (G c h k : Shell Ω) (hG : 2 * G + 1 = 0) (hc : 2 * (c * c) = 1)319    (hh : h * h = -1) (hk : k * k = -2) :320    (k * c) * (k * c) = -1 ∧ (k * c = h ∨ k * c = -h) ∧ G = -(c * c) ∧ (2 * G) * (2 * G) = 1 ∧321    (h * h) * (h * h) = 1 ∧ (h * c) * (h * c) = -2 * (G * G) := by322  have hkc : (k * c) * (k * c) = -1 := by323    rw [Shell.mul_assoc, Shell.mul_left_comm c, ← Shell.mul_assoc, hk, ← Shell.neg_mul, hc]324  have hh0 : h ≠ 0 := fun h0 => by325    rw [h0, Shell.zero_mul] at hh326    have := congrArg Neg.neg hh327    rw [Shell.neg_zero, Shell.neg_neg] at this328    exact F.one_ne_zero this.symm329  have hlink : k * c = h ∨ k * c = -h := ((root_pair F (-1) h hh hh0).1 (k * c)).1 hkc330  have h2G : 2 * G = -1 := Shell.eq_neg_of_add_eq_zero hG331  refine ⟨hkc, hlink, ?_, ?_, ?_, ?_⟩332  · apply F.mul_left_cancel F.two_ne_zero333    rw [h2G, ← Shell.mul_neg, hc]334  · rw [h2G, Shell.neg_mul_neg, Shell.mul_one]335  · rw [hh, Shell.neg_mul_neg, Shell.mul_one]336  · have h4 : (2 * 2 : Shell Ω) * (G * G) = 1 := by337      rw [Shell.mul_assoc, ← Shell.mul_left_comm G 2 G, ← Shell.mul_assoc, h2G, Shell.neg_mul_neg,338        Shell.mul_one]339    have hcc : c * c = 2 * (G * G) := by340      apply F.mul_left_cancel F.two_ne_zero341      rw [hc, ← Shell.mul_assoc, h4]342    rw [Shell.mul_assoc, Shell.mul_left_comm c, ← Shell.mul_assoc, hh, Shell.neg_one_mul, hcc,343      Shell.neg_mul]344345end carrier346347/-! ## The values decided by the kernel (10:E4, E5, E9, F2–F4, G2, G3) -/348section values349350/-- 10:E4, 10:E5 — the Carrier `Ω = 233` (`S = 58`): `G = 116 = 2S`, `ħ = 89`, `k_B = 124`, `c = 159`,351`h = 144 = −ħ` satisfy the defining congruences, the linkage `k_B c = −ħ`, `G = −c²`, `ħ c = k_B G`352(the monomial on the `k_B` residue), and the partner `109 = −124` fails the linkage. -/353theorem carrier233 :354    2 * (116 : Shell 233) + 1 = 0 ∧ (89 : Shell 233) * 89 = -1 ∧ (124 : Shell 233) * 124 = -2 ∧355    2 * ((159 : Shell 233) * 159) = 1 ∧ (124 : Shell 233) * 159 = -89 ∧ (144 : Shell 233) = -89 ∧356    (116 : Shell 233) = -(159 * 159) ∧ (89 : Shell 233) * 159 = 124 * 116 ∧357    (109 : Shell 233) = -124 ∧ (109 : Shell 233) * 159 ≠ -89 := by decide +kernel358359/-- 10:E4, 10:E5, 21:C5 — the laboratory Carrier `Ω = 2 408 561` (`S = 602 140`): `G = 1 204 280`,360`ħ = 18 688`, `k_B = 1 880 160`, `c = 171 106`, `h = 2 389 873 = −ħ` satisfy the defining congruences, the361linkage, `G = −c²` and `ħ c = k_B G`. -/362theorem carrierLab :363    2 * (1204280 : Shell 2408561) + 1 = 0 ∧ (18688 : Shell 2408561) * 18688 = -1 ∧364    (1880160 : Shell 2408561) * 1880160 = -2 ∧ 2 * ((171106 : Shell 2408561) * 171106) = 1 ∧365    (1880160 : Shell 2408561) * 171106 = -18688 ∧ (2389873 : Shell 2408561) = -18688 ∧366    (1204280 : Shell 2408561) = -(171106 * 171106) ∧367    (18688 : Shell 2408561) * 171106 = 1880160 * 1204280 := by decide +kernel368369/-- 10:E9 — the admissibility predicate of the programme on `(p, Ω) = (4κ + 1, 4S + 1)`: `p` prime,370`κ > 1`; `Ω` prime, `S` even, `S ≡ 1 (mod 3)`; `p² < Ω`. -/371def admissible (κ S : Nat) : Prop :=372  isPrime (4 * κ + 1) ∧ 1 < κ ∧ isPrime (4 * S + 1) ∧ S % 2 = 0 ∧ S % 3 = 1 ∧373  (4 * κ + 1) * (4 * κ + 1) < 4 * S + 1374instance (κ S : Nat) : Decidable (admissible κ S) := by unfold admissible; exact inferInstance375376/-- 10:E9 — the minimal admissible pair is `(13, 233)`: `(κ, S) = (3, 58)` is admissible, no pair with377`S < 58` is (for `S < 58`, `p² < Ω` forces `κ ≤ 3`), and the counterfactuals — dropping the mod-3 clause378admits `(13, 193)` (`S = 48`), dropping `κ > 1` admits `(5, 41)` (`S = 10`), and `κ = 2` gives the379composite `9`. -/380theorem minimality :381    admissible 3 58 ∧ (∀ κ, κ < 4 → ∀ S, S < 58 → ¬ admissible κ S) ∧382    (∀ κ, 4 ≤ κ → ∀ S, S < 58 → ¬ ((4 * κ + 1) * (4 * κ + 1) < 4 * S + 1)) ∧383    (isPrime 193 ∧ 48 % 2 = 0 ∧ 48 % 3 = 0 ∧ 13 * 13 < 193) ∧384    (isPrime 5 ∧ isPrime 41 ∧ 10 % 2 = 0 ∧ 10 % 3 = 1 ∧ 25 < 41) ∧ ¬ isPrime 9 := by385  refine ⟨by decide +kernel, by decide +kernel, fun κ hκ S hS h => ?_, by decide +kernel,386    by decide +kernel, by decide +kernel⟩387  have h1 : 17 * 17 ≤ (4 * κ + 1) * (4 * κ + 1) :=388    Nat.mul_le_mul (Nat.succ_le_succ (Nat.mul_le_mul_left 4 hκ)) (Nat.succ_le_succ (Nat.mul_le_mul_left 4 hκ))389  have h2 : 4 * S + 1 ≤ 229 := Nat.succ_le_succ (Nat.mul_le_mul_left 4 (Nat.le_of_lt_succ hS))390  exact Nat.lt_irrefl _ (Nat.lt_of_lt_of_le (Nat.lt_of_le_of_lt h1 h) (Nat.le_trans h2 (by decide)))391392/-- 10:F2, 10:F3, 10:F4, 10:G3, 10:X1, 10:X2 — the derived domains realized on `𝔽₁₃` (`κ = 3`, the flag `(0, 3)`):393`[m] = [E][v]⁻² = (11, 4)`, `[a] = (1, 10)`, `[F] = [m][a] = (12, 2)`, `[p] = [m][v] = (12, 3) = I_q [L]⁻¹`,394`[S] = [E][T] = I_q`, `[P] = (0, 1)`, `[G] = [F][L]²[m]⁻² = (5, 6)`; the geometric conversions `[Għ/c³] = [L]²`,395`[Gm/c²] = [L]`, `[Gm/c³] = [T]`, `[Gm/r³] = [T]⁻²`; `[Θ] = [E][k_B]⁻¹ = [a]` and the Unruh closure;396the phase exponent `[E][T][ħ]⁻¹ = 1`; kinetic energy `[m][v]² = [E]`; `Q + Q²` inhomogeneous, `[L] ≠ [L]²`;397`F/a = [m]`, flagged. -/398theorem realized13 :399    let E := energy 3; let v := L 3 * (T 3)⁻¹; let m := E * (v ^ 2)⁻¹; let a := v * (T 3)⁻¹400    let f := m * a; let pm := m * v; let G := f * L 3 ^ 2 * (m ^ 2)⁻¹; let kB := flag 3 * (L 3)⁻¹ * T 3401    m = ⟨11, 4⟩ ∧ a = ⟨1, 10⟩ ∧ f = ⟨12, 2⟩ ∧ pm = ⟨12, 3⟩ ∧ pm = mom 3 ∧ E * T 3 = flag 3 ∧402    E * (T 3)⁻¹ = ⟨0, 1⟩ ∧ G = ⟨5, 6⟩ ∧403    G * flag 3 * (v ^ 3)⁻¹ = L 3 ^ 2 ∧ G * m * (v ^ 2)⁻¹ = L 3 ∧ G * m * (v ^ 3)⁻¹ = T 3 ∧404    G * m * (L 3 ^ 3)⁻¹ = (T 3 ^ 2)⁻¹ ∧ E * kB⁻¹ = a ∧ flag 3 * a * v⁻¹ * kB⁻¹ = a ∧405    E * T 3 * (flag 3)⁻¹ = 1 ∧ m * v ^ 2 = E ∧ L 3 ≠ L 3 ^ 2 ∧ f * a⁻¹ = m := by406  decide407408/-- 10:D6 — the flag is horizon-inaccessible on `𝔽₁₃`: no label with `|r|, |s| ≤ 2 < κ = 3` (the409representatives `r ∈ {11, 12, 0, 1, 2}`, `s ∈ {10, 11, 0, 1, 2}`) is `I_q = (0, 3)`, while at `H = 3` the410label `(0, 3)` itself is the flag. -/411theorem flag_inaccessible13 :412    (∀ x : DomK 3, (x.r.val ≤ 2 ∨ 11 ≤ x.r.val) → (x.s.val ≤ 2 ∨ 10 ≤ x.s.val) → x ≠ flag 3) ∧413    (⟨0, 3⟩ : DomK 3) = flag 3 := by decide +kernel414415/-- 10:G2 — the window ladder by integer squares: `(2√κ)² = 4κ < (κ/2)² = κ²/4`, i.e. `16κ < κ²`, holds for416`κ = 17, 387, 602 140` and fails for `κ = 3`; the coherence identity `(2√κ)² = 4κ = p − 1` and the417totality closure `4S = Ω − 1` on the laboratory Carrier. -/418theorem window_ladder :419    16 * 17 < 17 * 17 ∧ 16 * 387 < 387 * 387 ∧ 16 * 602140 < 602140 * 602140 ∧ ¬ (16 * 3 < 3 * 3) ∧420    (∀ κ, 2 * 2 * κ = 4 * κ ∧ 4 * κ = (4 * κ + 1) - 1) ∧ 4 * 602140 = 2408561 - 1 := by421  refine ⟨by decide +kernel, by decide +kernel, by decide +kernel, by decide +kernel, fun κ => ⟨rfl, rfl⟩, by decide +kernel⟩422423/-- 10:G5, 10:P1 — the resolution floor on the chart value `S = 2.6 × 10¹²²`, `Ω = 4S + 1`: `Ω^(-1/4)` is of the order424of `10⁻³¹` (`10¹²⁰ < Ω ≤ 10¹²⁴`), thirteen orders below `10⁻¹⁸` (`10¹²² ≤ Ω < 10¹²⁶`) and twenty-six below `2.2 × 10⁻⁵`425(`10¹²⁶ ≤ 22⁴ Ω < 10¹³⁰`); in bits, to the nearest integer, `102` (`2⁴⁰⁶ ≤ Ω < 2⁴¹⁰`) against the `58` of the finest interspecies426frequency ratio, `3.2 × 10⁻¹⁸` (`2¹²⁵ ≤ 10³⁸ < 2¹²⁷`), and the `67` of the finest differential comparison, `7.6 × 10⁻²¹`427(`76² · 2¹³³ ≤ 10⁴⁴ < 76² · 2¹³⁵`); the maximal coherent count `Ω^(1/4)` between `5 × 10³⁰` and `6 × 10³⁰` (`5⁴ 10¹²⁰ < Ω < 6⁴ 10¹²⁰`); and the428duration beyond which the mass-independent clock bound `(t_P² t)^(1/3)` permits finer than the floor, `t* = t_P Ω^(3/8)`,429between `600` and `900` s with `t_P = 5.391247 × 10⁻⁴⁴` s. Every rounding exact in integers, decided by the kernel. -/430theorem resolution_floor :431    10^120 < 4 * (26 * 10^121) + 1 ∧ 4 * (26 * 10^121) + 1 ≤ 10^124 ∧432    10^122 ≤ 4 * (26 * 10^121) + 1 ∧ 4 * (26 * 10^121) + 1 < 10^126 ∧433    10^126 ≤ 22^4 * (4 * (26 * 10^121) + 1) ∧ 22^4 * (4 * (26 * 10^121) + 1) < 10^130 ∧434    2^406 ≤ 4 * (26 * 10^121) + 1 ∧ 4 * (26 * 10^121) + 1 < 2^410 ∧435    2^125 ≤ 10^38 ∧ 10^38 < 2^127 ∧436    76^2 * 2^133 ≤ 10^44 ∧ 10^44 < 76^2 * 2^135 ∧437    5^4 * 10^120 < 4 * (26 * 10^121) + 1 ∧ 4 * (26 * 10^121) + 1 < 6^4 * 10^120 ∧438    600^8 * 10^400 < 5391247^8 * (4 * (26 * 10^121) + 1)^3 ∧ 5391247^8 * (4 * (26 * 10^121) + 1)^3 < 900^8 * 10^400 := by439  decide +kernel440441/-- 10:G1, 10:G3 — local recovery on `𝔽₁₃` at `H = 5`: the `121` conventional pairs `|r|, |s| ≤ 5` have442distinct modular labels, `12 > 10`. -/443theorem recovery13 :444    12 > 2 * 5 ∧445    ∀ r, r < 11 → ∀ s, s < 11 → ∀ r', r' < 11 → ∀ s', s' < 11 →446      ((ofNat (r + 8) : Shell 13) = ofNat (r' + 8) ∧ (ofNat (s + 7) : Shell 12) = ofNat (s' + 7)) →447      r = r' ∧ s = s' := by448  refine ⟨by decide +kernel, by decide +kernel⟩449450/-- 10:G3 — the energy–momentum relation realized on `𝔽₁₃`: with `[v] = [L][T]⁻¹`, `[p] = I_q[L]⁻¹` and451`[m] = (11, 4)`, the three labels `[E]²`, `([p][c])²`, `([m][c]²)²` coincide, `(0, 4) = I_q²[T]⁻²`, the452fibre of `[E]²`, so `E² = p²c² + m²c⁴` is homogeneous; its massless case `[E] = [p][c]`, and `[E] = [m][c]²`453on the energy fibre, `[m] = [E][v]⁻²`. -/454theorem energy_momentum13 :455    let E := energy 3; let v := L 3 * (T 3)⁻¹456    E ^ 2 = (mom 3 * v) ^ 2 ∧ E ^ 2 = ((⟨11, 4⟩ : DomK 3) * v ^ 2) ^ 2 ∧ E ^ 2 = ⟨0, 4⟩ ∧457    E ^ 2 = flag 3 ^ 2 * (T 3 ^ 2)⁻¹ ∧ E = mom 3 * v ∧ E = ⟨11, 4⟩ * v ^ 2 ∧ E * (v ^ 2)⁻¹ = ⟨11, 4⟩ := by458  decide459460/-- 10:F5, 10:X4 — the charge label on `𝔽₁₃` (`κ = 3`): with the Coulomb constant neutral, `[q]² = [E][L] = I_q [L][T]⁻¹`,461and the labels with `x² = [q]²` are exactly `⟨7, 1⟩` and `⟨7, 7⟩ = ⟨7, 1⟩ · I_q²` (the half-period), their space462exponent `7 = 2⁻¹ = 2κ + 1`, the meridian half-turn. -/463theorem charge13 :464    (∀ x : DomK 3, x * x = energy 3 * L 3 ↔ x = ⟨7, 1⟩ ∨ x = ⟨7, 7⟩) ∧465    (⟨7, 7⟩ : DomK 3) = ⟨7, 1⟩ * flag 3 ^ 2 ∧ energy 3 * L 3 = flag 3 * (L 3 * (T 3)⁻¹) ∧466    (2 : Shell 13) * 7 = 1 := by decide467468/-- 10:F5, 10:X4 — the charge label on `p = 29` (`κ = 7`): exactly `⟨15, 3⟩` and `⟨15, 17⟩ = ⟨15, 3⟩ · I_q²`. -/469theorem charge29 :470    (∀ x : DomK 7, x * x = energy 7 * L 7 ↔ x = ⟨15, 3⟩ ∨ x = ⟨15, 17⟩) ∧471    (⟨15, 17⟩ : DomK 7) = ⟨15, 3⟩ * flag 7 ^ 2 := by decide472473/-- 10:F5, 10:X4 — on `p = 17` (`κ = 4`, even) no label squares to `[q]²`: the charge has no domain on that shell. -/474theorem no_charge17 : ∀ x : DomK 4, x * x ≠ energy 4 * L 4 := by decide475476/-- 10:F5, 10:X4 — on `p = 41` (`κ = 10`, even) no label squares to `[q]²`. -/477theorem no_charge41 : ∀ x : DomK 10, x * x ≠ energy 10 * L 10 := by decide478479end values480481/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/482section aliases483variable {p : Nat} [Pos p] {κ : Nat} {g : Shell p}484485/-- Primality by trial division, decidable. -/486@[reducible] def isPrime (n : Nat) : Prop :=487  FRC.Nat.isPrime n488489/-- 10:E4, 10:P2 — the root pair: if `x² = a` with `x ≠ 0` then `y² = a` iff `y = x` or `y = −x`, and `−x ≠ x`;490each quadratic defining congruence has exactly two roots on a framed Carrier. -/491theorem root_pair (F : Frame p κ g) (a x : Shell p) (hx : x * x = a) (hx0 : x ≠ 0) :492    (∀ y : Shell p, y * y = a ↔ (y = x ∨ y = -x)) ∧ -x ≠ x :=493  FRC.Shell.Frame.root_pair F a x hx hx0494495/-- `∀ m < n, P m`, decided by recursion on `n` — Lean's own instance carries `propext`; this one nothing. -/496@[reducible] def decForallLT (P : Nat → Prop) [DecidablePred P] : (n : Nat) → Decidable (∀ m, m < n → P m) :=497  FRC.Shell.decForallLT P498499@[reducible] def instDecForallLT (P : Nat → Prop) [DecidablePred P] (n : Nat) : Decidable (∀ m, m < n → P m) :=500  FRC.Shell.instDecForallLT P n501502/-- `∀ x : Shell p, P x`, decided through the representatives. -/503@[reducible] def instDecForallShell {p : Nat} [Pos p] (P : Shell p → Prop) [DecidablePred P] :504    Decidable (∀ x, P x) :=505  FRC.Shell.instDecForallShell P506507end aliases508509-- Ledger predicates of 10-dimensions (generated by make_predicates.py from docs/10-dimensions/10-dimensions-ledger.json; edit the ledger, not this section)510/-- 10:C2 (p10012) — The modular unit-domain group and the grading: $\{U_{r,s}\}$ is a finite abelian group isomorphic to $\Dp$ under $U_{r,s}U_{r',s'}=U_{r+r',s+s'}$, and $\Ap$ is $\Dp$-graded, $\Ap^{(r,s)}\Ap^{(r',s')}\subseteq\Ap^{(r+r',s+s')}$. -/511theorem p10012 : ∀ {p n : Nat} [FRC.Pos p] [FRC.Pos n] (a : FRC.Dimensions.Dom p n), a * a⁻¹ = (1 : FRC.Dimensions.Dom p n) :=512  @FRC.Dimensions.Dom.mul_inv513/-- 10:C3 (p10013) — Fibrewise addition and the neutral-domain criterion: a sum of homogeneous quantities is homogeneous exactly when its nonzero summands share a domain, the fibre components adding separately; a monomial $\prod Q_j^{k_j}$ has domain $\sum k_j(r_j,s_j)$ and is a neutral-domain invariant iff that sum is $(0,0)$ in $\Dp$. -/514theorem p10013 : ∀ {p n : Nat} [FRC.Pos p] [FRC.Pos n] (a : FRC.Dimensions.Dom p n) (k : Nat), a ^ k = { r := FRC.Shell.ofNat k * a.r, s := FRC.Shell.ofNat k * a.s } :=515  @FRC.Dimensions.Dom.pow_eq516/-- 10:C6 (p10016) — What the action forces and what is declared: the time-exponent period $\p-1$ is forced by the pushforward action of $\Zp^{\times}$, the space-exponent refinement to period $\p$ is declared and carried by the transport theorem (D2); classical temporal unit change is nominal re-assignment within a fixed presentation, the chronon atomic. -/517theorem p10016 : ∀ (κ : Nat) [FRC.Pos κ], (FRC.Dimensions.L κ * FRC.Dimensions.T κ ^ κ) ^ ((4 : Nat) * κ + (1 : Nat)) = FRC.Dimensions.flag κ :=518  @FRC.Dimensions.meridian_transport519/-- 10:D1 (p10017) — Chart duality: $[f]=\unitT^{-1}$; $\delta_S:D\mapsto D^{-1}$ is an involution of the domain group whose orbit on the generators is the four-domain structure (space, momentum, time, energy); $\delta_C$ the second involution, carrying $\unitL\mapsto[p]$, $\unitT\mapsto\unitE$. -/520theorem p10017 : (∀ {p n : Nat} [FRC.Pos p] [FRC.Pos n] (a : FRC.Dimensions.Dom p n), a⁻¹⁻¹ = a) ∧ ∀ (κ : Nat) [FRC.Pos κ] (a : FRC.Dimensions.DomK κ), FRC.Dimensions.deltaC κ (FRC.Dimensions.deltaC κ a) = a ∧ FRC.Dimensions.deltaC κ (FRC.Dimensions.L κ) = FRC.Dimensions.mom κ ∧ FRC.Dimensions.deltaC κ (FRC.Dimensions.T κ) = FRC.Dimensions.energy κ :=521  And.intro @FRC.Dimensions.Dom.inv_inv (@FRC.Dimensions.deltaC_involutive)522/-- 10:D2 (p10018) — The internal flag: $\Dp$ contains exactly one subgroup of order four, $\langle\unitT^{\kap}\rangle$, entirely in the time-exponent factor; $\Iq:=\unitT^{\kap}$, $\Iq^{4}=1$, $\Iq^{2}=\unitT^{\pi}$; no flag of space ($\Z_\p$ has no element of order four); the two periods interfere, $(\unitL\unitT^{\kap})^{\p}=\Iq$, on three shells. -/523theorem p10018 : (∀ (κ : Nat) [FRC.Pos κ], FRC.Dimensions.flag κ ^ (2 : Nat) = FRC.Dimensions.T κ ^ ((2 : Nat) * κ) ∧ FRC.Dimensions.flag κ ^ (1 : Nat) ≠ (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.flag κ ^ (2 : Nat) ≠ (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.flag κ ^ (3 : Nat) ≠ (1 : FRC.Dimensions.DomK κ)) ∧ (∀ (κ : Nat) {g : FRC.Shell ((4 : Nat) * κ + (1 : Nat))}, FRC.Shell.Frame ((4 : Nat) * κ + (1 : Nat)) κ g → ∀ (r : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), (2 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))) * (2 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))) * r = (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))) → r = (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat)))) ∧ ∀ (x : FRC.Dimensions.DomK (3 : Nat)), x ^ (4 : Nat) = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ x ^ (2 : Nat) ≠ (1 : FRC.Dimensions.DomK (3 : Nat)) ↔ x = FRC.Dimensions.flag (3 : Nat) ∨ x = (FRC.Dimensions.flag (3 : Nat))⁻¹ :=524  And.intro @FRC.Dimensions.flag_order_four (And.intro @FRC.Dimensions.no_flag_of_space (@FRC.Dimensions.order_four_13))525/-- 10:D3 (p10019) — The lift: the flag records the quarter the chart duality forgets --- on charts the cardinal skeleton acts as $s\bmod2$ ($F$ exchanges the conjugate charts, $J$ fixes them), on labels $s\mapsto\Iq^{s}$ is an isomorphism $\Z_4\to\langle\Iq\rangle$ whose quotient by $\{0,2\kap\}$ returns the chart action; on the Carrier $\hbar^{2}=-1$, $\hbar^{4}=1$, $\hbar^{2}\ne1$, the crossing quantum of order four, never two. Shells $(13,2)$, $(173,3)$; Carriers $233$, $2\,408\,561$. -/526theorem p10019 : ∀ (κ : Nat) [FRC.Pos κ], FRC.Dimensions.flag κ ^ (0 : Nat) = (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.flag κ ^ (1 : Nat) = { r := (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), s := FRC.Shell.ofNat κ } ∧ FRC.Dimensions.flag κ ^ (2 : Nat) = { r := (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), s := FRC.Shell.ofNat ((2 : Nat) * κ) } ∧ FRC.Dimensions.flag κ ^ (3 : Nat) = { r := (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), s := FRC.Shell.ofNat ((3 : Nat) * κ) } ∧ FRC.Dimensions.flag κ ^ (4 : Nat) = (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.flag κ ^ (2 : Nat) * FRC.Dimensions.flag κ ^ (2 : Nat) = (1 : FRC.Dimensions.DomK κ) :=527  @FRC.Dimensions.record_values528/-- 10:D6 (p10022) — The flagged readings over the counts: $\unitE=[h][f]=\Iq\unitT^{-1}$, $[p]=\unithbar[k]=\Iq\unitL^{-1}$, one quantity per pair, the flagged reading one capacity step above its count; $[S]=\unitE\unitT=\Iq$ and every phase count neutral, $\unitE\unitT\unithbar^{-1}=1$; the absolute unit is horizon-inaccessible (no monomial of a window $H\ll\kap$ expresses the flag) and becomes visible at $\kap\le H<2\kap$. -/529theorem p10022 : (∀ (κ : Nat) [FRC.Pos κ], FRC.Dimensions.energy κ = { r := (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), s := FRC.Shell.ofNat κ + (-1 : FRC.Shell ((4 : Nat) * κ)) } ∧ FRC.Dimensions.mom κ = { r := (-1 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), s := FRC.Shell.ofNat κ } ∧ FRC.Dimensions.energy κ * FRC.Dimensions.T κ = FRC.Dimensions.flag κ ∧ FRC.Dimensions.energy κ * FRC.Dimensions.T κ * (FRC.Dimensions.flag κ)⁻¹ = (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.mom κ * FRC.Dimensions.L κ * (FRC.Dimensions.flag κ)⁻¹ = (1 : FRC.Dimensions.DomK κ)) ∧ (∀ (x : FRC.Dimensions.DomK (3 : Nat)), x.r.val ≤ (2 : Nat) ∨ (11 : Nat) ≤ x.r.val → x.s.val ≤ (2 : Nat) ∨ (10 : Nat) ≤ x.s.val → x ≠ FRC.Dimensions.flag (3 : Nat)) ∧ { r := (0 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (3 : Nat))) } = FRC.Dimensions.flag (3 : Nat) :=530  And.intro @FRC.Dimensions.flagged_readings (@FRC.Dimensions.flag_inaccessible13)531/-- 10:E4 (p10027) — The defining congruences, pair form: on the Carrier chart $2G+1\equiv0$, $2c^{2}\equiv1$, $\hbar^{2}\equiv-1$, $k_B^{2}\equiv-2\pmod\Om$ determine the constants uniquely at pair level --- $G=2\dS$ exact, the quadratics each with exactly two roots $\{x,-x\}$ (admissibility guarantees the residues: $\Om\equiv1\bmod4$, $\dS$ even for $2$, hence $-2$) --- and the linkage $\{\pm k_B\}\{\pm c\}=\{\pm\hbar\}$ is derived at pair level; the root pair of $-1$ is $\{\hbar,h\}$ with $h=2\pi\hbar\equiv-\hbar$. Exhaustive on both Carriers. -/532theorem p10027 : (∀ {Ω : Nat} [FRC.Pos Ω] {S : Nat} {g : FRC.Shell Ω}, FRC.Shell.Frame Ω S g → ∀ (x : FRC.Shell Ω), (2 : FRC.Shell Ω) * x + (1 : FRC.Shell Ω) = (0 : FRC.Shell Ω) ↔ x = FRC.Shell.ofNat ((2 : Nat) * S)) ∧ (∀ {Ω : Nat} [FRC.Pos Ω] {S : Nat} {g : FRC.Shell Ω}, FRC.Shell.Frame Ω S g → ∀ (a x : FRC.Shell Ω), x * x = a → x ≠ (0 : FRC.Shell Ω) → (∀ (y : FRC.Shell Ω), y * y = a ↔ y = x ∨ y = -x) ∧ -x ≠ x) ∧ (∀ {Ω : Nat} [FRC.Pos Ω] {S : Nat} {g : FRC.Shell Ω}, FRC.Shell.Frame Ω S g → ∀ (G c h k : FRC.Shell Ω), (2 : FRC.Shell Ω) * G + (1 : FRC.Shell Ω) = (0 : FRC.Shell Ω) → (2 : FRC.Shell Ω) * (c * c) = (1 : FRC.Shell Ω) → h * h = (-1 : FRC.Shell Ω) → k * k = (-2 : FRC.Shell Ω) → k * c * (k * c) = (-1 : FRC.Shell Ω) ∧ (k * c = h ∨ k * c = -h) ∧ G = -(c * c) ∧ (2 : FRC.Shell Ω) * G * ((2 : FRC.Shell Ω) * G) = (1 : FRC.Shell Ω) ∧ h * h * (h * h) = (1 : FRC.Shell Ω) ∧ h * c * (h * c) = (-2 : FRC.Shell Ω) * (G * G)) ∧ ((2 : FRC.Shell (233 : Nat)) * (116 : FRC.Shell (233 : Nat)) + (1 : FRC.Shell (233 : Nat)) = (0 : FRC.Shell (233 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat)) ∧ (124 : FRC.Shell (233 : Nat)) * (124 : FRC.Shell (233 : Nat)) = (-2 : FRC.Shell (233 : Nat)) ∧ (2 : FRC.Shell (233 : Nat)) * ((159 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat))) = (1 : FRC.Shell (233 : Nat)) ∧ (124 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat)) = (-89 : FRC.Shell (233 : Nat)) ∧ (144 : FRC.Shell (233 : Nat)) = (-89 : FRC.Shell (233 : Nat)) ∧ (116 : FRC.Shell (233 : Nat)) = -((159 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat))) ∧ (89 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat)) = (124 : FRC.Shell (233 : Nat)) * (116 : FRC.Shell (233 : Nat)) ∧ (109 : FRC.Shell (233 : Nat)) = (-124 : FRC.Shell (233 : Nat)) ∧ (109 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat)) ≠ (-89 : FRC.Shell (233 : Nat))) ∧ (2 : FRC.Shell (2408561 : Nat)) * (1204280 : FRC.Shell (2408561 : Nat)) + (1 : FRC.Shell (2408561 : Nat)) = (0 : FRC.Shell (2408561 : Nat)) ∧ (18688 : FRC.Shell (2408561 : Nat)) * (18688 : FRC.Shell (2408561 : Nat)) = (-1 : FRC.Shell (2408561 : Nat)) ∧ (1880160 : FRC.Shell (2408561 : Nat)) * (1880160 : FRC.Shell (2408561 : Nat)) = (-2 : FRC.Shell (2408561 : Nat)) ∧ (2 : FRC.Shell (2408561 : Nat)) * ((171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat))) = (1 : FRC.Shell (2408561 : Nat)) ∧ (1880160 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (-18688 : FRC.Shell (2408561 : Nat)) ∧ (2389873 : FRC.Shell (2408561 : Nat)) = (-18688 : FRC.Shell (2408561 : Nat)) ∧ (1204280 : FRC.Shell (2408561 : Nat)) = -((171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat))) ∧ (18688 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (1880160 : FRC.Shell (2408561 : Nat)) * (1204280 : FRC.Shell (2408561 : Nat)) :=533  And.intro @FRC.Dimensions.G_unique (And.intro @FRC.Dimensions.root_pair (And.intro @FRC.Dimensions.linkage (And.intro @FRC.Dimensions.carrier233 (@FRC.Dimensions.carrierLab))))534/-- 10:E5 (p10028) — Pair consequences and representative inertness: $G=-c^{2}$, $G^{2}\equiv4^{-1}$, $\hbar^{4}\equiv1$, $(k_Bc)^{2}\equiv-1$, and $\hbar cG^{-1}$ lands in $\{\pm k_B\}$; of the eight sign assignments exactly the four with $\sigma_\hbar=\sigma_c\sigma_k$ are admissible, a $(\Z/2)^{2}$, every identity holding on each and the $\hbar$-flip relabelling within $\{\hbar,h\}$; what a bounded observer registers is exactly the pair-inert content. -/535theorem p10028 : (∀ {Ω : Nat} [FRC.Pos Ω] {S : Nat} {g : FRC.Shell Ω}, FRC.Shell.Frame Ω S g → ∀ (G c h k : FRC.Shell Ω), (2 : FRC.Shell Ω) * G + (1 : FRC.Shell Ω) = (0 : FRC.Shell Ω) → (2 : FRC.Shell Ω) * (c * c) = (1 : FRC.Shell Ω) → h * h = (-1 : FRC.Shell Ω) → k * k = (-2 : FRC.Shell Ω) → k * c * (k * c) = (-1 : FRC.Shell Ω) ∧ (k * c = h ∨ k * c = -h) ∧ G = -(c * c) ∧ (2 : FRC.Shell Ω) * G * ((2 : FRC.Shell Ω) * G) = (1 : FRC.Shell Ω) ∧ h * h * (h * h) = (1 : FRC.Shell Ω) ∧ h * c * (h * c) = (-2 : FRC.Shell Ω) * (G * G)) ∧ ((2 : FRC.Shell (233 : Nat)) * (116 : FRC.Shell (233 : Nat)) + (1 : FRC.Shell (233 : Nat)) = (0 : FRC.Shell (233 : Nat)) ∧ (89 : FRC.Shell (233 : Nat)) * (89 : FRC.Shell (233 : Nat)) = (-1 : FRC.Shell (233 : Nat)) ∧ (124 : FRC.Shell (233 : Nat)) * (124 : FRC.Shell (233 : Nat)) = (-2 : FRC.Shell (233 : Nat)) ∧ (2 : FRC.Shell (233 : Nat)) * ((159 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat))) = (1 : FRC.Shell (233 : Nat)) ∧ (124 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat)) = (-89 : FRC.Shell (233 : Nat)) ∧ (144 : FRC.Shell (233 : Nat)) = (-89 : FRC.Shell (233 : Nat)) ∧ (116 : FRC.Shell (233 : Nat)) = -((159 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat))) ∧ (89 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat)) = (124 : FRC.Shell (233 : Nat)) * (116 : FRC.Shell (233 : Nat)) ∧ (109 : FRC.Shell (233 : Nat)) = (-124 : FRC.Shell (233 : Nat)) ∧ (109 : FRC.Shell (233 : Nat)) * (159 : FRC.Shell (233 : Nat)) ≠ (-89 : FRC.Shell (233 : Nat))) ∧ (2 : FRC.Shell (2408561 : Nat)) * (1204280 : FRC.Shell (2408561 : Nat)) + (1 : FRC.Shell (2408561 : Nat)) = (0 : FRC.Shell (2408561 : Nat)) ∧ (18688 : FRC.Shell (2408561 : Nat)) * (18688 : FRC.Shell (2408561 : Nat)) = (-1 : FRC.Shell (2408561 : Nat)) ∧ (1880160 : FRC.Shell (2408561 : Nat)) * (1880160 : FRC.Shell (2408561 : Nat)) = (-2 : FRC.Shell (2408561 : Nat)) ∧ (2 : FRC.Shell (2408561 : Nat)) * ((171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat))) = (1 : FRC.Shell (2408561 : Nat)) ∧ (1880160 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (-18688 : FRC.Shell (2408561 : Nat)) ∧ (2389873 : FRC.Shell (2408561 : Nat)) = (-18688 : FRC.Shell (2408561 : Nat)) ∧ (1204280 : FRC.Shell (2408561 : Nat)) = -((171106 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat))) ∧ (18688 : FRC.Shell (2408561 : Nat)) * (171106 : FRC.Shell (2408561 : Nat)) = (1880160 : FRC.Shell (2408561 : Nat)) * (1204280 : FRC.Shell (2408561 : Nat)) :=536  And.intro @FRC.Dimensions.linkage (And.intro @FRC.Dimensions.carrier233 (@FRC.Dimensions.carrierLab))537/-- 10:E9 (p10032) — The minimal admissible pair: under the programme's admissibility predicate ($\p=4\kap+1$ prime, $\kap>1$; $\Om=4\dS+1$ prime, $\dS$ even, $\dS\equiv1\bmod3$; $\p^{2}<\Om$) the smallest instance is $(\p,\Om)=(13,233)$, by exhaustive scan, with the counterfactuals: dropping the mod-$3$ clause admits $(13,193)$, dropping $\kap>1$ admits $(5,41)$, $\kap=2$ gives the composite $9$. -/538theorem p10032 : FRC.Dimensions.admissible (3 : Nat) (58 : Nat) ∧ (∀ (κ : Nat), κ < (4 : Nat) → ∀ (S : Nat), S < (58 : Nat) → ¬FRC.Dimensions.admissible κ S) ∧ (∀ (κ : Nat), (4 : Nat) ≤ κ → ∀ (S : Nat), S < (58 : Nat) → ¬((4 : Nat) * κ + (1 : Nat)) * ((4 : Nat) * κ + (1 : Nat)) < (4 : Nat) * S + (1 : Nat)) ∧ (FRC.Dimensions.isPrime (193 : Nat) ∧ (48 : Nat) % (2 : Nat) = (0 : Nat) ∧ (48 : Nat) % (3 : Nat) = (0 : Nat) ∧ (13 : Nat) * (13 : Nat) < (193 : Nat)) ∧ (FRC.Dimensions.isPrime (5 : Nat) ∧ FRC.Dimensions.isPrime (41 : Nat) ∧ (10 : Nat) % (2 : Nat) = (0 : Nat) ∧ (10 : Nat) % (3 : Nat) = (1 : Nat) ∧ (25 : Nat) < (41 : Nat)) ∧ ¬FRC.Dimensions.isPrime (9 : Nat) :=539  @FRC.Dimensions.minimality540/-- 10:F2 (p10034) — The mechanical and gravitational domains: $[m]=\Iq\unitL^{-2}\unitT$; $[a]=\unitL\unitT^{-2}$, $[F]=\Iq\unitL^{-1}\unitT^{-1}$, $[p]=\Iq\unitL^{-1}$, $[S]=\Iq$, $[P]=\Iq\unitT^{-2}$, $[\text{pressure}]=\Iq\unitL^{-3}\unitT^{-1}$; $[G]=\Iq^{-1}\unitL^{5}\unitT^{-3}$; the geometric conversions $[G\hbar/c^{3}]=\unitL^{2}$, $[Gm/c^{2}]=\unitL$, $[Gm/c^{3}]=\unitT$, $[G\rho_m]=\unitT^{-2}$; mass derived, not primitive. -/541theorem p10034 : have E := FRC.Dimensions.energy (3 : Nat); have v := FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹; have m := E * (v ^ (2 : Nat))⁻¹; have a := v * (FRC.Dimensions.T (3 : Nat))⁻¹; have f := m * a; have pm := m * v; have G := f * FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) * (m ^ (2 : Nat))⁻¹; have kB := FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat))⁻¹ * FRC.Dimensions.T (3 : Nat); m = { r := (11 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (4 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ a = { r := (1 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (10 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ f = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (2 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = FRC.Dimensions.mom (3 : Nat) ∧ E * FRC.Dimensions.T (3 : Nat) = FRC.Dimensions.flag (3 : Nat) ∧ E * (FRC.Dimensions.T (3 : Nat))⁻¹ = { r := (0 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G = { r := (5 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (6 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G * FRC.Dimensions.flag (3 : Nat) * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ G * m * (v ^ (2 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ∧ G * m * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.T (3 : Nat) ∧ G * m * (FRC.Dimensions.L (3 : Nat) ^ (3 : Nat))⁻¹ = (FRC.Dimensions.T (3 : Nat) ^ (2 : Nat))⁻¹ ∧ E * kB⁻¹ = a ∧ FRC.Dimensions.flag (3 : Nat) * a * v⁻¹ * kB⁻¹ = a ∧ E * FRC.Dimensions.T (3 : Nat) * (FRC.Dimensions.flag (3 : Nat))⁻¹ = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ m * v ^ (2 : Nat) = E ∧ FRC.Dimensions.L (3 : Nat) ≠ FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ f * a⁻¹ = m :=542  @FRC.Dimensions.realized13543/-- 10:F3 (p10035) — Temperature carries the acceleration domain: $[\Theta]=\unitE[k_B]^{-1}=\unitL\unitT^{-2}=[a]$, flag-free; the Unruh combination $\hbar a/c\,k_B$ closes flag-free in the algebra; neither mass nor temperature is primitive, the classical $M$-$L$-$T$-plus-thermal system the torsion-free shadow of two generators plus the flag. -/544theorem p10035 : have E := FRC.Dimensions.energy (3 : Nat); have v := FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹; have m := E * (v ^ (2 : Nat))⁻¹; have a := v * (FRC.Dimensions.T (3 : Nat))⁻¹; have f := m * a; have pm := m * v; have G := f * FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) * (m ^ (2 : Nat))⁻¹; have kB := FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat))⁻¹ * FRC.Dimensions.T (3 : Nat); m = { r := (11 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (4 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ a = { r := (1 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (10 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ f = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (2 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = FRC.Dimensions.mom (3 : Nat) ∧ E * FRC.Dimensions.T (3 : Nat) = FRC.Dimensions.flag (3 : Nat) ∧ E * (FRC.Dimensions.T (3 : Nat))⁻¹ = { r := (0 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G = { r := (5 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (6 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G * FRC.Dimensions.flag (3 : Nat) * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ G * m * (v ^ (2 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ∧ G * m * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.T (3 : Nat) ∧ G * m * (FRC.Dimensions.L (3 : Nat) ^ (3 : Nat))⁻¹ = (FRC.Dimensions.T (3 : Nat) ^ (2 : Nat))⁻¹ ∧ E * kB⁻¹ = a ∧ FRC.Dimensions.flag (3 : Nat) * a * v⁻¹ * kB⁻¹ = a ∧ E * FRC.Dimensions.T (3 : Nat) * (FRC.Dimensions.flag (3 : Nat))⁻¹ = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ m * v ^ (2 : Nat) = E ∧ FRC.Dimensions.L (3 : Nat) ≠ FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ f * a⁻¹ = m :=545  @FRC.Dimensions.realized13546/-- 10:F4 (p10036) — Count-valued comparisons are flag-free: every ratio of two quantities of equal crossing degree ($Gm/r^{3}$, the phase exponent $[E][T]/[\hbar]$) is a neutral or flag-free label, the flag entering unitful measures only; $F/a=[m]$, crossing degrees $1$ and $0$, is the flagged boundary case. -/547theorem p10036 : have E := FRC.Dimensions.energy (3 : Nat); have v := FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹; have m := E * (v ^ (2 : Nat))⁻¹; have a := v * (FRC.Dimensions.T (3 : Nat))⁻¹; have f := m * a; have pm := m * v; have G := f * FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) * (m ^ (2 : Nat))⁻¹; have kB := FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat))⁻¹ * FRC.Dimensions.T (3 : Nat); m = { r := (11 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (4 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ a = { r := (1 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (10 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ f = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (2 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = FRC.Dimensions.mom (3 : Nat) ∧ E * FRC.Dimensions.T (3 : Nat) = FRC.Dimensions.flag (3 : Nat) ∧ E * (FRC.Dimensions.T (3 : Nat))⁻¹ = { r := (0 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G = { r := (5 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (6 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G * FRC.Dimensions.flag (3 : Nat) * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ G * m * (v ^ (2 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ∧ G * m * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.T (3 : Nat) ∧ G * m * (FRC.Dimensions.L (3 : Nat) ^ (3 : Nat))⁻¹ = (FRC.Dimensions.T (3 : Nat) ^ (2 : Nat))⁻¹ ∧ E * kB⁻¹ = a ∧ FRC.Dimensions.flag (3 : Nat) * a * v⁻¹ * kB⁻¹ = a ∧ E * FRC.Dimensions.T (3 : Nat) * (FRC.Dimensions.flag (3 : Nat))⁻¹ = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ m * v ^ (2 : Nat) = E ∧ FRC.Dimensions.L (3 : Nat) ≠ FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ f * a⁻¹ = m :=548  @FRC.Dimensions.realized13549/-- 10:F5 (p10047) — The electromagnetic domain: with the Coulomb constant neutral (declared), $[q]^{2}=\unitE\unitL=\Iq\unitL\unitT^{-1}$; charge is an integer degree on the lift realised as $\unitL^{2\kap+1}\unitT^{(\kap-1)/2}$, existing iff $\kap$ is odd, unique up to $\Iq^{2}$, never window-covariant ($|r|=2\kap$); no further generator within C1's two charts; on the even capacities no label squares to $[q]^{2}$. -/550theorem p10047 : ((∀ (x : FRC.Dimensions.DomK (3 : Nat)), x * x = FRC.Dimensions.energy (3 : Nat) * FRC.Dimensions.L (3 : Nat) ↔ x = { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∨ x = { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (7 : FRC.Shell ((4 : Nat) * (3 : Nat))) }) ∧ { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (7 : FRC.Shell ((4 : Nat) * (3 : Nat))) } = { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } * FRC.Dimensions.flag (3 : Nat) ^ (2 : Nat) ∧ FRC.Dimensions.energy (3 : Nat) * FRC.Dimensions.L (3 : Nat) = FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ ((∀ (x : FRC.Dimensions.DomK (7 : Nat)), x * x = FRC.Dimensions.energy (7 : Nat) * FRC.Dimensions.L (7 : Nat) ↔ x = { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (7 : Nat))) } ∨ x = { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (17 : FRC.Shell ((4 : Nat) * (7 : Nat))) }) ∧ { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (17 : FRC.Shell ((4 : Nat) * (7 : Nat))) } = { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (7 : Nat))) } * FRC.Dimensions.flag (7 : Nat) ^ (2 : Nat)) ∧ (∀ (x : FRC.Dimensions.DomK (4 : Nat)), x * x ≠ FRC.Dimensions.energy (4 : Nat) * FRC.Dimensions.L (4 : Nat)) ∧ ∀ (x : FRC.Dimensions.DomK (10 : Nat)), x * x ≠ FRC.Dimensions.energy (10 : Nat) * FRC.Dimensions.L (10 : Nat) :=551  And.intro @FRC.Dimensions.charge13 (And.intro @FRC.Dimensions.charge29 (And.intro @FRC.Dimensions.no_charge17 (@FRC.Dimensions.no_charge41)))552set_option linter.defProp false in553/-- 10:G1 (p10037) — Local recovery: for an exponent horizon $H$ with $4\kap>2H$ the modular labels distinguish every conventional pair $|r|,|s|\le H$; the flagged sector is recovered through the crossing degree, $M^{u}L^{a}T^{b}\mapsto(a-2u,\,b+u;\,u)$ injective and windowed-faithful. -/554def p10037 := @FRC.Dimensions.recovery13555/-- 10:G2 (p10038) — The window ladder: coherence $2\sqrt\kap$ below recovery $\kap/2$ below flag inaccessibility $\kap$ below covariance $2\kap$, nested strictly for every $\kap\ge17$ and failing for the toy $\kap=3$, all orderings by integer squares; the coherence identity $(2\sqrt\kap)^{2}=\p-1$ and the totality closure $(2\sqrt\dS)^{2}=\Om-1$. -/556theorem p10038 : (16 : Nat) * (17 : Nat) < (17 : Nat) * (17 : Nat) ∧ (16 : Nat) * (387 : Nat) < (387 : Nat) * (387 : Nat) ∧ (16 : Nat) * (602140 : Nat) < (602140 : Nat) * (602140 : Nat) ∧ ¬(16 : Nat) * (3 : Nat) < (3 : Nat) * (3 : Nat) ∧ (∀ (κ : Nat), (2 : Nat) * (2 : Nat) * κ = (4 : Nat) * κ ∧ (4 : Nat) * κ = (4 : Nat) * κ + (1 : Nat) - (1 : Nat)) ∧ (4 : Nat) * (602140 : Nat) = (2408561 : Nat) - (1 : Nat) :=557  @FRC.Dimensions.window_ladder558set_option linter.defProp false in559/-- 10:G3 (p10039) — The worked examples: $\kap=3$, $H=5$, $12>10$ so every pair in $[-5,5]^{2}$ is distinguished; kinetic energy $[m][v]^{2}=[E]$; $Q+Q^{2}$ inhomogeneous; the phase exponent neutral; flag arithmetic ($G\hbar/c^{3}$ flag-free, $\Iq^{2}=\unitT^{\pi}$); the Schwarzschild length $[Gm/c^{2}]=\unitL$; the gravitational frequency $[Gm/r^{3}]=\unitT^{-2}$; the energy--momentum relation $E^{2}=p^{2}c^{2}+m^{2}c^{4}$ homogeneous at crossing degree two, its massless case $E=pc$ at crossing degree one. -/560def p10039 := And.intro @FRC.Dimensions.realized13 (And.intro @FRC.Dimensions.recovery13 (@FRC.Dimensions.energy_momentum13))561/-- 10:G5 (p10052) — The resolution floor: a registration resolved to one part in $N$ is a coherent count of $N$, bounded at $\sqrt\p$ (A5), so a single coherent registration on a shell of cardinality $\p$ resolves no finer than $\p^{-1/2}$; under $\p^{2}<\Om$ the floor is at least $\Om^{-1/4}$ on every admissible shell, of the order of $10^{-31}$ ($102$ bits) at $\dS=2.6\times10^{122}$ (Rem.~\ref{rem:holographic}), thirteen orders below the $10^{-18}$ optical-clock comparisons and twenty-six below the uncertainty of $G$. -/562theorem p10052 : (10 : Nat) ^ (120 : Nat) < (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ≤ (10 : Nat) ^ (124 : Nat) ∧ (10 : Nat) ^ (122 : Nat) ≤ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) < (10 : Nat) ^ (126 : Nat) ∧ (10 : Nat) ^ (126 : Nat) ≤ (22 : Nat) ^ (4 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) ∧ (22 : Nat) ^ (4 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) < (10 : Nat) ^ (130 : Nat) ∧ (2 : Nat) ^ (406 : Nat) ≤ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) < (2 : Nat) ^ (410 : Nat) ∧ (2 : Nat) ^ (125 : Nat) ≤ (10 : Nat) ^ (38 : Nat) ∧ (10 : Nat) ^ (38 : Nat) < (2 : Nat) ^ (127 : Nat) ∧ (76 : Nat) ^ (2 : Nat) * (2 : Nat) ^ (133 : Nat) ≤ (10 : Nat) ^ (44 : Nat) ∧ (10 : Nat) ^ (44 : Nat) < (76 : Nat) ^ (2 : Nat) * (2 : Nat) ^ (135 : Nat) ∧ (5 : Nat) ^ (4 : Nat) * (10 : Nat) ^ (120 : Nat) < (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) < (6 : Nat) ^ (4 : Nat) * (10 : Nat) ^ (120 : Nat) ∧ (600 : Nat) ^ (8 : Nat) * (10 : Nat) ^ (400 : Nat) < (5391247 : Nat) ^ (8 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) ^ (3 : Nat) ∧ (5391247 : Nat) ^ (8 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) ^ (3 : Nat) < (900 : Nat) ^ (8 : Nat) * (10 : Nat) ^ (400 : Nat) :=563  @FRC.Dimensions.resolution_floor564/-- 10:P1 (p10053) — The resolution floor, staked: no single coherent registration resolves finer than $\Om^{-1/4}$, of the order of $10^{-31}$, and no coherent count exceeds $\Om^{1/4}\approx6\times10^{30}$ (G5 over A2, A5, B1; the holographic reading of Rem.~\ref{rem:holographic}). Falsifier: one coherent registration finer than that. Confrontation: the finest interspecies frequency ratio, $3.2\times10^{-18}$ \citep{Aeppli2025}, and the finest differential comparison, $7.6\times10^{-21}$ \citep{Bothwell2022} --- $67$ bits against $102$, averaged determinations; the mass-independent clock bound $(t_P^{2}t)^{1/3}$ permits finer beyond $730$~s. -/565theorem p10053 : (10 : Nat) ^ (120 : Nat) < (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ≤ (10 : Nat) ^ (124 : Nat) ∧ (10 : Nat) ^ (122 : Nat) ≤ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) < (10 : Nat) ^ (126 : Nat) ∧ (10 : Nat) ^ (126 : Nat) ≤ (22 : Nat) ^ (4 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) ∧ (22 : Nat) ^ (4 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) < (10 : Nat) ^ (130 : Nat) ∧ (2 : Nat) ^ (406 : Nat) ≤ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) < (2 : Nat) ^ (410 : Nat) ∧ (2 : Nat) ^ (125 : Nat) ≤ (10 : Nat) ^ (38 : Nat) ∧ (10 : Nat) ^ (38 : Nat) < (2 : Nat) ^ (127 : Nat) ∧ (76 : Nat) ^ (2 : Nat) * (2 : Nat) ^ (133 : Nat) ≤ (10 : Nat) ^ (44 : Nat) ∧ (10 : Nat) ^ (44 : Nat) < (76 : Nat) ^ (2 : Nat) * (2 : Nat) ^ (135 : Nat) ∧ (5 : Nat) ^ (4 : Nat) * (10 : Nat) ^ (120 : Nat) < (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) ∧ (4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat) < (6 : Nat) ^ (4 : Nat) * (10 : Nat) ^ (120 : Nat) ∧ (600 : Nat) ^ (8 : Nat) * (10 : Nat) ^ (400 : Nat) < (5391247 : Nat) ^ (8 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) ^ (3 : Nat) ∧ (5391247 : Nat) ^ (8 : Nat) * ((4 : Nat) * ((26 : Nat) * (10 : Nat) ^ (121 : Nat)) + (1 : Nat)) ^ (3 : Nat) < (900 : Nat) ^ (8 : Nat) * (10 : Nat) ^ (400 : Nat) :=566  @FRC.Dimensions.resolution_floor567/-- 10:P2 (p10054) — Constancy, staked: every dimensionless ratio of the constants is fixed in time and position, zero drift, zero dipole --- the totality timeless (B1), every constant a residue of it in the framework's realisation (A1; the quartet's, E1, E6; the charge's, Rem.~\ref{rem:electromagnetic}), the quartet's fixed by the congruences given $\dS$ (E4), selected once (E7). Falsifier: a detected variation (E1's). Confrontation: $\dot\alpha/\alpha=1.8(2.5)\times10^{-19}\,\mathrm{yr}^{-1}$ \citep{Filzinger2023}, consistent with zero. -/568theorem p10054 : (∀ {Ω : Nat} [FRC.Pos Ω] {S : Nat} {g : FRC.Shell Ω}, FRC.Shell.Frame Ω S g → ∀ (x : FRC.Shell Ω), (2 : FRC.Shell Ω) * x + (1 : FRC.Shell Ω) = (0 : FRC.Shell Ω) ↔ x = FRC.Shell.ofNat ((2 : Nat) * S)) ∧ ∀ {Ω : Nat} [FRC.Pos Ω] {S : Nat} {g : FRC.Shell Ω}, FRC.Shell.Frame Ω S g → ∀ (a x : FRC.Shell Ω), x * x = a → x ≠ (0 : FRC.Shell Ω) → (∀ (y : FRC.Shell Ω), y * y = a ↔ y = x ∨ y = -x) ∧ -x ≠ x :=569  And.intro @FRC.Dimensions.G_unique (@FRC.Dimensions.root_pair)570/-- 10:X1 (p10048) — The arity of classical bookkeeping, derived: four horizons less one identity, $4-1=3$ free scales in bijection with $\{c,\hbar,G\}$, exactly three independent members of $\{c,\hbar,G,k_B\}$; the three mechanical primitives are the two chart generators and the flag's torsion-free surrogate, mass, $[m]=\Iq\unitL^{-2}\unitT$, $m_P=\pP/c$. Classical dimensional analysis postulates the count and the mass primitive. -/571theorem p10048 : have E := FRC.Dimensions.energy (3 : Nat); have v := FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹; have m := E * (v ^ (2 : Nat))⁻¹; have a := v * (FRC.Dimensions.T (3 : Nat))⁻¹; have f := m * a; have pm := m * v; have G := f * FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) * (m ^ (2 : Nat))⁻¹; have kB := FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat))⁻¹ * FRC.Dimensions.T (3 : Nat); m = { r := (11 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (4 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ a = { r := (1 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (10 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ f = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (2 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = FRC.Dimensions.mom (3 : Nat) ∧ E * FRC.Dimensions.T (3 : Nat) = FRC.Dimensions.flag (3 : Nat) ∧ E * (FRC.Dimensions.T (3 : Nat))⁻¹ = { r := (0 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G = { r := (5 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (6 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G * FRC.Dimensions.flag (3 : Nat) * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ G * m * (v ^ (2 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ∧ G * m * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.T (3 : Nat) ∧ G * m * (FRC.Dimensions.L (3 : Nat) ^ (3 : Nat))⁻¹ = (FRC.Dimensions.T (3 : Nat) ^ (2 : Nat))⁻¹ ∧ E * kB⁻¹ = a ∧ FRC.Dimensions.flag (3 : Nat) * a * v⁻¹ * kB⁻¹ = a ∧ E * FRC.Dimensions.T (3 : Nat) * (FRC.Dimensions.flag (3 : Nat))⁻¹ = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ m * v ^ (2 : Nat) = E ∧ FRC.Dimensions.L (3 : Nat) ≠ FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ f * a⁻¹ = m :=572  @FRC.Dimensions.realized13573/-- 10:X2 (p10049) — The thermal primitive is redundant: $[\Theta]=\unitE[k_B]^{-1}=\unitL\unitT^{-2}$, the acceleration domain, flag-free where energy carries the flag; $|k_B|=\hbar/c$ is the quartet's mixed product; the Unruh combination $\hbar a/(c\,k_B)$ closes as a domain identity. Classical bookkeeping adjoins a thermal unit and reads $k_B$ as a conversion. -/574theorem p10049 : have E := FRC.Dimensions.energy (3 : Nat); have v := FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹; have m := E * (v ^ (2 : Nat))⁻¹; have a := v * (FRC.Dimensions.T (3 : Nat))⁻¹; have f := m * a; have pm := m * v; have G := f * FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) * (m ^ (2 : Nat))⁻¹; have kB := FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat))⁻¹ * FRC.Dimensions.T (3 : Nat); m = { r := (11 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (4 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ a = { r := (1 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (10 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ f = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (2 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = { r := (12 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ pm = FRC.Dimensions.mom (3 : Nat) ∧ E * FRC.Dimensions.T (3 : Nat) = FRC.Dimensions.flag (3 : Nat) ∧ E * (FRC.Dimensions.T (3 : Nat))⁻¹ = { r := (0 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G = { r := (5 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (6 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∧ G * FRC.Dimensions.flag (3 : Nat) * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ G * m * (v ^ (2 : Nat))⁻¹ = FRC.Dimensions.L (3 : Nat) ∧ G * m * (v ^ (3 : Nat))⁻¹ = FRC.Dimensions.T (3 : Nat) ∧ G * m * (FRC.Dimensions.L (3 : Nat) ^ (3 : Nat))⁻¹ = (FRC.Dimensions.T (3 : Nat) ^ (2 : Nat))⁻¹ ∧ E * kB⁻¹ = a ∧ FRC.Dimensions.flag (3 : Nat) * a * v⁻¹ * kB⁻¹ = a ∧ E * FRC.Dimensions.T (3 : Nat) * (FRC.Dimensions.flag (3 : Nat))⁻¹ = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ m * v ^ (2 : Nat) = E ∧ FRC.Dimensions.L (3 : Nat) ≠ FRC.Dimensions.L (3 : Nat) ^ (2 : Nat) ∧ f * a⁻¹ = m :=575  @FRC.Dimensions.realized13576/-- 10:X3 (p10050) — One action quantum for both conjugate pairs: the domain lattice has exactly one order-four subgroup, in the time factor (no flag of space), canonical and covariant, so $E=hf$ and $p=\hbar k$ share one $\hbar$, $\lP\pP=\tPl\EP$ --- derived from the shell's algebra with no Lorentz structure used. -/577theorem p10050 : (∀ (κ : Nat) [FRC.Pos κ], FRC.Dimensions.flag κ ^ (2 : Nat) = FRC.Dimensions.T κ ^ ((2 : Nat) * κ) ∧ FRC.Dimensions.flag κ ^ (1 : Nat) ≠ (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.flag κ ^ (2 : Nat) ≠ (1 : FRC.Dimensions.DomK κ) ∧ FRC.Dimensions.flag κ ^ (3 : Nat) ≠ (1 : FRC.Dimensions.DomK κ)) ∧ (∀ (κ : Nat) {g : FRC.Shell ((4 : Nat) * κ + (1 : Nat))}, FRC.Shell.Frame ((4 : Nat) * κ + (1 : Nat)) κ g → ∀ (r : FRC.Shell ((4 : Nat) * κ + (1 : Nat))), (2 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))) * (2 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))) * r = (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat))) → r = (0 : FRC.Shell ((4 : Nat) * κ + (1 : Nat)))) ∧ ∀ (x : FRC.Dimensions.DomK (3 : Nat)), x ^ (4 : Nat) = (1 : FRC.Dimensions.DomK (3 : Nat)) ∧ x ^ (2 : Nat) ≠ (1 : FRC.Dimensions.DomK (3 : Nat)) ↔ x = FRC.Dimensions.flag (3 : Nat) ∨ x = (FRC.Dimensions.flag (3 : Nat))⁻¹ :=578  And.intro @FRC.Dimensions.flag_order_four (And.intro @FRC.Dimensions.no_flag_of_space (@FRC.Dimensions.order_four_13))579/-- 10:X4 (p10051) — Charge is an integer degree of the two generators on the shells of odd capacity, not a further primitive: with the Coulomb constant neutral (F5), $[q]^{2}=\Iq\unitL\unitT^{-1}$, $q_P^{2}=\hbar c$; the lift has no half root (the Gaussian exponents $M^{1/2}L^{3/2}T^{-1}$ are half-integers there), so torsion-free bookkeeping adjoins an electrical primitive as it adjoins mass; the fine-structure ratio stays a neutral count. -/580theorem p10051 : ((∀ (x : FRC.Dimensions.DomK (3 : Nat)), x * x = FRC.Dimensions.energy (3 : Nat) * FRC.Dimensions.L (3 : Nat) ↔ x = { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } ∨ x = { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (7 : FRC.Shell ((4 : Nat) * (3 : Nat))) }) ∧ { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (7 : FRC.Shell ((4 : Nat) * (3 : Nat))) } = { r := (7 : FRC.Shell ((4 : Nat) * (3 : Nat) + (1 : Nat))), s := (1 : FRC.Shell ((4 : Nat) * (3 : Nat))) } * FRC.Dimensions.flag (3 : Nat) ^ (2 : Nat) ∧ FRC.Dimensions.energy (3 : Nat) * FRC.Dimensions.L (3 : Nat) = FRC.Dimensions.flag (3 : Nat) * (FRC.Dimensions.L (3 : Nat) * (FRC.Dimensions.T (3 : Nat))⁻¹) ∧ (2 : FRC.Shell (13 : Nat)) * (7 : FRC.Shell (13 : Nat)) = (1 : FRC.Shell (13 : Nat))) ∧ ((∀ (x : FRC.Dimensions.DomK (7 : Nat)), x * x = FRC.Dimensions.energy (7 : Nat) * FRC.Dimensions.L (7 : Nat) ↔ x = { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (7 : Nat))) } ∨ x = { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (17 : FRC.Shell ((4 : Nat) * (7 : Nat))) }) ∧ { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (17 : FRC.Shell ((4 : Nat) * (7 : Nat))) } = { r := (15 : FRC.Shell ((4 : Nat) * (7 : Nat) + (1 : Nat))), s := (3 : FRC.Shell ((4 : Nat) * (7 : Nat))) } * FRC.Dimensions.flag (7 : Nat) ^ (2 : Nat)) ∧ (∀ (x : FRC.Dimensions.DomK (4 : Nat)), x * x ≠ FRC.Dimensions.energy (4 : Nat) * FRC.Dimensions.L (4 : Nat)) ∧ ∀ (x : FRC.Dimensions.DomK (10 : Nat)), x * x ≠ FRC.Dimensions.energy (10 : Nat) * FRC.Dimensions.L (10 : Nat) :=581  And.intro @FRC.Dimensions.charge13 (And.intro @FRC.Dimensions.charge29 (And.intro @FRC.Dimensions.no_charge17 (@FRC.Dimensions.no_charge41)))582-- end ledger predicates583584end FRC.Dimensions585