Dimensions.lean — FrcLedger

1import Mathlib2import FrcLedger.Theme.Fourier3import FrcLedger.Theme.Frame45/-!6# 10-dimensions — the shell-domain calculus with the unit flag: the ledger predicates in Lean (2026-09-18)78Predicates of the ledger of *Dimensional Analysis over Finite Holographic Substrate* (tree9`10-dimensions-20260720`). The domain lattice `D_p = C_p × C_{p−1}`, `p = 4κ + 1`, with the labels `U_{r,s}`10as the basis of the monoid algebra `A_p = ⊕ F_p U_{r,s}`: the label group, the grading, fibrewise addition11and the neutral-domain criterion (C2, C3); the chart duality `δ_S` and the crossed duality `δ_C` (D1); the12internal flag — the elements of order four are `(0, ±κ)`, the one element of order two is `(0, 2κ)`, no flag13of space, the unique subgroup of order four, meridian transport `(L T^κ)^p = I_q` (D2, C6); the lift — the14record map `Z_4 → ⟨I_q⟩`, its kernel, the quotient by the half-period, the operator four-cycle from156-fourier, the Carrier face `ħ² = −1 ⇒ ħ⁴ = 1 ≠ ħ²` (D3); the flagged readings and the horizon16inaccessibility of the flag (D6); window covariance — the dilation character, the invariants `{0, 2κ}` of the17pushforward, the quarter-turn fix/swap law, the `σ`-twisted lift (C5); the unit face of the quartet — the18action identity, the rank-three parametrisation, the pairing closure, the cancellation identity, the19normalisation and the positive root (E2, E3); the defining congruences at pair level — the linear pin, the20root pairs, the linkage, the pair consequences, representative inertness, the `h`-form, the existence of the21residues on every admissible Carrier, and the two Carriers `233` and `2 408 561` decided (E4, E5); the22lifted labels `(r, s; j)` and the mechanical, gravitational and thermal domains (F2–F4); local recovery, the23crossing embedding and its windowed faithfulness (G1); the window ladder (G2); the `κ = 3` examples and the24energy–momentum relation on the lift (G3); the window coincidence and Buckingham's count on the pendulum (G4).25Classical (tier 2) on Mathlib's hierarchy; the finite content — the lattice as pairs of residues, the flag,26the transport, the Carrier values and the minimality scan — is proved with no axioms in27`FrcCore/Dimensions.lean`.28-/2930namespace FRC.Dimensions3132section33open FRC.Frame (root_pair)3435open AddMonoidAlgebra3637/-! ## The domain lattice and the quantity algebra (10:C1–C3) -/38section lattice3940variable (κ : ℕ)4142instance instNeZeroFour [NeZero κ] : NeZero (4 * κ) := ⟨by have := NeZero.ne κ; omega⟩4344/-- 10:C1 — the domain lattice `D_p = C_p × C_{p−1}`, `p = 4κ + 1`: the space exponent mod `p`, the time45exponent mod `p − 1 = 4κ`. -/46abbrev Dom := ZMod (4 * κ + 1) × ZMod (4 * κ)4748/-- 10:C1 — the space generator `[L] = U_{1,0}`, anchored on the unit. -/49def L : Dom κ := (1, 0)5051/-- 10:C1 — the time generator `[T] = U_{0,1}`, anchored on the chronon step. -/52def T : Dom κ := (0, 1)5354/-- 10:D2 — the unit flag `I_q = [T]^κ`, the label `(0, κ)`. -/55def flag : Dom κ := (0, (κ : ZMod (4 * κ)))5657/-- 10:C1 — the homogeneous quantity algebra `A_p = ⊕_{(r,s)} F_p U_{r,s}`: the monoid algebra of the58lattice over the shell. -/59abbrev QA := AddMonoidAlgebra (ZMod (4 * κ + 1)) (Dom κ)6061/-- 10:C1 — the modular unit-domain label `U_{r,s} = [L]^r [T]^s`, the basis element of the fibre `(r, s)`. -/62noncomputable def U (a : Dom κ) : QA κ := single a 16364/-- 10:C2 — the product of labels: `U_{r,s} U_{r',s'} = U_{r+r', s+s'}`. -/65theorem U_mul (a b : Dom κ) : U κ a * U κ b = U κ (a + b) := by66  unfold U; rw [single_mul_single, one_mul]6768/-- 10:C2 — the neutral label is the unit: `U_{0,0} = 1`. -/69theorem U_zero : U κ 0 = 1 := one_def.symm7071/-- 10:C2 — the inverse of `U_{r,s}` is `U_{−r,−s}`. -/72theorem U_add_neg (a : Dom κ) : U κ a * U κ (-a) = 1 := by rw [U_mul, add_neg_cancel, U_zero]7374theorem U_neg_add (a : Dom κ) : U κ (-a) * U κ a = 1 := by rw [U_mul, neg_add_cancel, U_zero]7576/-- 10:C2 — distinct labels are distinct elements of `A_p` (`κ ≥ 1`). -/77theorem U_injective [NeZero κ] : Function.Injective (U κ) := by78  have : Fact (1 < 4 * κ + 1) := ⟨by have := NeZero.pos κ; omega⟩79  exact single_left_injective one_ne_zero8081/-- The label as a unit of `A_p`. -/82noncomputable def Uunit (a : Dom κ) : (QA κ)ˣ := ⟨U κ a, U κ (-a), U_add_neg κ a, U_neg_add κ a⟩8384/-- 10:C2 — the modular unit-domain group: `(r, s) ↦ U_{r,s}` is a homomorphism from `D_p` (written85multiplicatively) to the units of `A_p`; with `U_injective` the label group is `D_p`. -/86noncomputable def Uhom : Multiplicative (Dom κ) →* (QA κ)ˣ where87  toFun a := Uunit κ a.toAdd88  map_one' := Units.ext (U_zero κ)89  map_mul' := fun a b => Units.ext (by90    show U κ (a * b).toAdd = U κ a.toAdd * U κ b.toAdd91    rw [U_mul, toAdd_mul])9293theorem Uhom_apply (a : Dom κ) : (Uhom κ (Multiplicative.ofAdd a) : QA κ) = U κ a := rfl9495/-- 10:C2 — the label group is `D_p`: the homomorphism is injective (`κ ≥ 1`). -/96theorem Uhom_injective [NeZero κ] : Function.Injective (Uhom κ) := fun a b h =>97  Multiplicative.toAdd.injective (U_injective κ (congrArg Units.val h))9899/-- 10:C2 — the grading `A_p^{(r,s)} A_p^{(r',s')} ⊆ A_p^{(r+r', s+s')}` on the basis:100`(q U_{r,s})(q' U_{r',s'}) = q q' U_{r+r', s+s'}`. -/101theorem fibre_mul (a b : Dom κ) (q q' : ZMod (4 * κ + 1)) :102    single a q * single b q' = single (a + b) (q * q') :=103  single_mul_single a b q q'104105/-- 10:C2 — the grading on the fibres `A_p^{(r,s)} = F_p U_{r,s}` (Mathlib's `grade`): the product of two106homogeneous quantities lies in the fibre of the sum of their domains. -/107theorem graded {x y : QA κ} {a b : Dom κ} (hx : x ∈ grade (ZMod (4 * κ + 1)) a)108    (hy : y ∈ grade (ZMod (4 * κ + 1)) b) : x * y ∈ grade (ZMod (4 * κ + 1)) (a + b) :=109  SetLike.mul_mem_graded (A := grade (ZMod (4 * κ + 1))) hx hy110111/-- 10:C3 — fibrewise addition: two quantities of one domain add within the fibre,112`q U_{r,s} + q' U_{r,s} = (q + q') U_{r,s}`. -/113theorem fibre_add (a : Dom κ) (q q' : ZMod (4 * κ + 1)) :114    single a q + single a q' = single a (q + q') :=115  (single_add a q q').symm116117/-- 10:C3 — the component of a sum of homogeneous quantities in the fibre `a` is the sum of the summands of118domain `a`: the sum is homogeneous of domain `a` exactly when every other component vanishes. -/119theorem coeff_sum_single {ι : Type*} (s : Finset ι) (m : ι → Dom κ) (q : ι → ZMod (4 * κ + 1))120    (a : Dom κ) : (∑ j ∈ s, single (m j) (q j)).coeff a = ∑ j ∈ s with m j = a, q j := by121  rw [coeff_sum, Finsupp.finsetSum_apply, Finset.sum_filter]122  refine Finset.sum_congr rfl (fun j _ => ?_)123  rw [coeff_single, Finsupp.single_apply]124125/-- 10:C3 — the domain of a monomial: `∏ (q_j U_{a_j})^{k_j} = (∏ q_j^{k_j}) U_{Σ k_j a_j}`. -/126theorem monomial {ι : Type*} (s : Finset ι) (m : ι → Dom κ) (q : ι → ZMod (4 * κ + 1)) (k : ι → ℕ) :127    ∏ j ∈ s, single (m j) (q j) ^ k j = single (∑ j ∈ s, k j • m j) (∏ j ∈ s, q j ^ k j) := by128  simp_rw [single_pow]; exact prod_single s _ _129130/-- 10:C3, 10:G4 — the domain of a monomial with integer exponents, in the label group:131`∏ U_{a_j}^{k_j} = U_{Σ k_j a_j}`; so on the shell a monomial is neutral iff `Σ k_j a_j = 0`, the neutrality132criterion that G4's count reads on the lift through the window coincidence (`window_neutrality`). -/133theorem monomial_units {ι : Type*} (s : Finset ι) (m : ι → Dom κ) (k : ι → ℤ) :134    ∏ j ∈ s, Uhom κ (Multiplicative.ofAdd (m j)) ^ k j135      = Uhom κ (Multiplicative.ofAdd (∑ j ∈ s, k j • m j)) := by136  rw [ofAdd_sum, map_prod]137  exact Finset.prod_congr rfl (fun j _ => by rw [ofAdd_zsmul, map_zpow])138139/-- 10:C3 — the neutral-domain criterion: a nonzero homogeneous quantity `c U_a` lies in the fibre `b` iff140`a = b`; so a monomial with nonzero coefficient is a neutral-domain invariant iff `Σ k_j a_j = 0` in `D_p`. -/141theorem single_mem_grade_iff (a b : Dom κ) {c : ZMod (4 * κ + 1)} (hc : c ≠ 0) :142    single a c ∈ grade (ZMod (4 * κ + 1)) b ↔ a = b := by143  rw [mem_grade_iff, coeff_single, Finsupp.support_single_ne_zero _ hc,144    Finset.singleton_subset_iff, Finset.mem_singleton]145146end lattice147148/-! ## Arithmetic of the time factor `C_{4κ}`, and the flag (10:D2, 10:C6, 10:D3) -/149section timefactor150151variable (κ : ℕ) [NeZero κ]152153theorem kappa_ne_zero : (κ : ZMod (4 * κ)) ≠ 0 := by154  rw [Ne, ZMod.natCast_eq_zero_iff]155  intro h156  have h1 := Nat.le_of_dvd (NeZero.pos κ) h157  have h2 := NeZero.pos κ158  omega159160theorem two_kappa_ne_zero : 2 * (κ : ZMod (4 * κ)) ≠ 0 := by161  rw [show 2 * (κ : ZMod (4 * κ)) = ((2 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl, Ne,162    ZMod.natCast_eq_zero_iff]163  intro h164  have h2 := NeZero.pos κ165  have h1 := Nat.le_of_dvd (by omega) h166  omega167168theorem three_kappa_ne_zero : 3 * (κ : ZMod (4 * κ)) ≠ 0 := by169  rw [show 3 * (κ : ZMod (4 * κ)) = ((3 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl, Ne,170    ZMod.natCast_eq_zero_iff]171  intro h172  have h2 := NeZero.pos κ173  have h1 := Nat.le_of_dvd (by omega) h174  omega175176omit [NeZero κ] in177theorem four_kappa : 4 * (κ : ZMod (4 * κ)) = 0 := by178  rw [show 4 * (κ : ZMod (4 * κ)) = ((4 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl]179  exact ZMod.natCast_self _180181omit [NeZero κ] in182/-- `3κ = −κ` in `C_{4κ}`: the two generators of the flag subgroup are inverse. -/183theorem three_kappa : 3 * (κ : ZMod (4 * κ)) = -(κ : ZMod (4 * κ)) := by184  have := four_kappa κ; linear_combination this185186/-- `a·s = 0` in `C_{4κ}` iff `b ∣ s.val`, where `4κ = a·b`. -/187theorem nat_mul_eq_zero_iff (a b : ℕ) (ha : 0 < a) (hb : 4 * κ = a * b) (s : ZMod (4 * κ)) :188    (a : ZMod (4 * κ)) * s = 0 ↔ b ∣ s.val := by189  have h1 : (a : ZMod (4 * κ)) * s = ((a * s.val : ℕ) : ZMod (4 * κ)) := by190    rw [Nat.cast_mul, ZMod.natCast_zmod_val]191  rw [h1, ZMod.natCast_eq_zero_iff]192  generalize s.val = v193  rw [hb]194  exact Nat.mul_dvd_mul_iff_left ha195196/-- `2s = 0` in `C_{4κ}` iff `s ∈ {0, 2κ}`: the one element of order two is the half-period. -/197theorem two_mul_eq_zero_iff (s : ZMod (4 * κ)) :198    2 * s = 0 ↔ s = 0 ∨ s = 2 * (κ : ZMod (4 * κ)) := by199  have hκ := NeZero.pos κ200  have h := nat_mul_eq_zero_iff κ 2 (2 * κ) (by norm_num) (by ring) s201  push_cast at h202  rw [h]203  constructor204  · rintro ⟨m, hm⟩205    have hlt := s.val_lt206    rw [hm] at hlt207    have hm2 : m < 2 := by208      have : 2 * κ * m < 2 * κ * 2 := by rw [show 2 * κ * 2 = 4 * κ by ring]; exact hlt209      exact Nat.lt_of_mul_lt_mul_left this210    have hs : s = ((2 * κ * m : ℕ) : ZMod (4 * κ)) := by rw [← hm, ZMod.natCast_zmod_val]211    interval_cases m212    · left; rw [hs]; simp213    · right; rw [hs]; push_cast; ring214  · rintro (rfl | rfl)215    · simp216    · rw [show (2 * (κ : ZMod (4 * κ))) = ((2 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl,217        ZMod.val_natCast_of_lt (by omega)]218219/-- `4s = 0` in `C_{4κ}` iff `s ∈ {0, κ, 2κ, 3κ}`: the subgroup of order four. -/220theorem four_mul_eq_zero_iff (s : ZMod (4 * κ)) :221    4 * s = 0 ↔ s = 0 ∨ s = κ ∨ s = 2 * (κ : ZMod (4 * κ)) ∨ s = 3 * (κ : ZMod (4 * κ)) := by222  have hκ := NeZero.pos κ223  have h := nat_mul_eq_zero_iff κ 4 κ (by norm_num) rfl s224  push_cast at h225  rw [h]226  constructor227  · rintro ⟨m, hm⟩228    have hlt := s.val_lt229    rw [hm] at hlt230    have hm4 : m < 4 := by231      have : κ * m < κ * 4 := by rw [Nat.mul_comm κ 4]; exact hlt232      exact Nat.lt_of_mul_lt_mul_left this233    have hs : s = ((κ * m : ℕ) : ZMod (4 * κ)) := by rw [← hm, ZMod.natCast_zmod_val]234    interval_cases m235    · left; rw [hs]; simp236    · right; left; rw [hs]; simp237    · right; right; left; rw [hs]; push_cast; ring238    · right; right; right; rw [hs]; push_cast; ring239  · rintro (rfl | rfl | rfl | rfl)240    · simp241    · rw [ZMod.val_natCast_of_lt (by omega)]242    · rw [show (2 * (κ : ZMod (4 * κ))) = ((2 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl,243        ZMod.val_natCast_of_lt (by omega)]244      exact Dvd.intro_left 2 rfl245    · rw [show (3 * (κ : ZMod (4 * κ))) = ((3 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl,246        ZMod.val_natCast_of_lt (by omega)]247      exact Dvd.intro_left 3 rfl248249omit [NeZero κ] in250/-- Every unit of `C_{4κ}` is odd: its representative is coprime to `4κ`, hence to `2`. -/251theorem unit_odd (ε : (ZMod (4 * κ))ˣ) : Odd (ε : ZMod (4 * κ)).val := by252  have h := ZMod.val_coe_unit_coprime ε253  have h2 : Nat.Coprime 2 (ε : ZMod (4 * κ)).val :=254    (Nat.Coprime.coprime_dvd_right ⟨2 * κ, by ring⟩ h).symm255  exact Nat.Coprime.odd_of_left h2256257/-- `ε · u` for a unit, written through the odd representative `2m + 1`. -/258theorem unit_mul (ε : (ZMod (4 * κ))ˣ) (u : ZMod (4 * κ)) :259    ∃ m : ℕ, (ε : ZMod (4 * κ)) * u = ((2 * m + 1 : ℕ) : ZMod (4 * κ)) * u := by260  obtain ⟨m, hm⟩ := unit_odd κ ε261  exact ⟨m, by rw [← ZMod.natCast_zmod_val (ε : ZMod (4 * κ)), hm]⟩262263theorem flag_ne_zero : flag κ ≠ 0 := fun h => kappa_ne_zero κ (congrArg Prod.snd h)264265omit [NeZero κ] in266/-- 10:D2 — `I_q⁴ = 1`. -/267theorem four_smul_flag : 4 • flag κ = 0 := by268  ext269  · simp [flag]270  · simp only [flag, nsmul_eq_mul, Nat.cast_ofNat, Prod.snd_zero]; exact four_kappa κ271272omit [NeZero κ] in273/-- 10:D2 — `I_q² = [T]^π`, the half-period `π = 2κ`. -/274theorem two_smul_flag : 2 • flag κ = (0, 2 * (κ : ZMod (4 * κ))) := by275  ext <;> simp [flag]276277theorem two_smul_flag_ne_zero : 2 • flag κ ≠ 0 := by278  rw [two_smul_flag]; intro h; exact two_kappa_ne_zero κ (congrArg Prod.snd h)279280theorem three_smul_flag_ne_zero : 3 • flag κ ≠ 0 := by281  intro h282  have := congrArg Prod.snd h283  simp only [flag, nsmul_eq_mul, Nat.cast_ofNat, Prod.snd_zero] at this284  exact three_kappa_ne_zero κ this285286/-- 10:D2 — the flag has order four. -/287theorem addOrderOf_flag : addOrderOf (flag κ) = 4 := by288  rw [addOrderOf_eq_iff (by norm_num)]289  refine ⟨four_smul_flag κ, fun m hm hm0 => ?_⟩290  interval_cases m291  · rw [one_smul]; exact flag_ne_zero κ292  · exact two_smul_flag_ne_zero κ293  · exact three_smul_flag_ne_zero κ294295/-- 10:D2 — the conjugate generator `I_q⁻¹ = (0, 3κ)` has order four as well. -/296theorem addOrderOf_neg_flag : addOrderOf (-flag κ) = 4 := by297  rw [addOrderOf_eq_iff (by norm_num)]298  refine ⟨by rw [smul_neg, four_smul_flag, neg_zero], fun m hm hm0 h => ?_⟩299  rw [smul_neg, neg_eq_zero] at h300  interval_cases m301  · rw [one_smul] at h; exact flag_ne_zero κ h302  · exact two_smul_flag_ne_zero κ h303  · exact three_smul_flag_ne_zero κ h304305omit [NeZero κ] in306/-- 10:D2, 10:C6 — meridian transport onto the flag: the two periods interfere, `([L][T]^κ)^p = I_q` —307the meridian component wraps (`p ≡ 0 (mod p)`) while the phase component advances by308`pκ = 4κ·κ + κ ≡ κ (mod 4κ)`; for every shell. -/309theorem meridian_transport : (4 * κ + 1) • (L κ + κ • T κ) = flag κ := by310  have h1 : L κ + κ • T κ = (1, (κ : ZMod (4 * κ))) := by ext <;> simp [L, T]311  rw [h1, flag, Prod.smul_mk]312  ext313  · show (4 * κ + 1) • (1 : ZMod (4 * κ + 1)) = 0314    rw [nsmul_eq_mul, mul_one]; exact ZMod.natCast_self _315  · show (4 * κ + 1) • (κ : ZMod (4 * κ)) = κ316    rw [nsmul_eq_mul]; push_cast317    rw [show (4 : ZMod (4 * κ)) * κ = ((4 * κ : ℕ) : ZMod (4 * κ)) by push_cast; rfl,318      ZMod.natCast_self, zero_add, one_mul]319320/-- 10:D3 — the record map `s ↦ I_q^s`, `Z_4 → D_p`: index-preserving (the flag exponent `κ` is the321fractional index of one quarter), a homomorphism because `I_q⁴ = 1`. -/322def record : ZMod 4 →+ Dom κ :=323  ZMod.lift 4 ⟨zmultiplesHom _ (flag κ), by324    rw [zmultiplesHom_apply, natCast_zsmul]; exact four_smul_flag κ⟩325326omit [NeZero κ] in327theorem record_natCast (m : ℕ) : record κ (m : ZMod 4) = m • flag κ := by328  have h : ((m : ℤ) : ZMod 4) = (m : ZMod 4) := Int.cast_natCast m329  rw [← h, record, ZMod.lift_coe, zmultiplesHom_apply, natCast_zsmul]330331/-- 10:D3 — the record map is injective: an isomorphism of `Z_4` onto the flag subgroup. -/332theorem record_injective : Function.Injective (record κ) := by333  rw [injective_iff_map_eq_zero]334  intro s hs335  rw [← ZMod.natCast_zmod_val s, record_natCast, ← addOrderOf_dvd_iff_nsmul_eq_zero,336    addOrderOf_flag] at hs337  have h0 := Nat.eq_zero_of_dvd_of_lt hs s.val_lt338  exact (ZMod.natCast_zmod_val s).symm.trans (by rw [h0, Nat.cast_zero])339340omit [NeZero κ] in341/-- 10:D3 — the image of the record map is the flag subgroup `⟨I_q⟩ = {1, I_q, I_q², I_q³}`. -/342theorem record_range : (record κ).range = AddSubgroup.zmultiples (flag κ) := by343  apply le_antisymm344  · intro x hx345    obtain ⟨s, rfl⟩ := AddMonoidHom.mem_range.mp hx346    rw [← ZMod.natCast_zmod_val s, record_natCast, ← natCast_zsmul]347    exact AddSubgroup.mem_zmultiples_iff.mpr ⟨_, rfl⟩348  · intro x hx349    obtain ⟨n, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx350    refine AddMonoidHom.mem_range.mpr ⟨(n : ZMod 4), ?_⟩351    rw [record, ZMod.lift_coe, zmultiplesHom_apply]352353omit [NeZero κ] in354/-- An element of the parity subgroup `⟨I_q²⟩` is killed by `2`. -/355theorem two_smul_of_mem_parity (x : Dom κ) (hx : x ∈ AddSubgroup.zmultiples (2 • flag κ)) :356    2 • x = 0 := by357  obtain ⟨n, rfl⟩ := AddSubgroup.mem_zmultiples_iff.mp hx358  rw [smul_comm, smul_smul, show 2 * 2 = 4 from rfl, four_smul_flag, smul_zero]359360/-- 10:D3 — the chart shadow: `I_q^s` lies in the parity subgroup `{1, I_q²}` exactly when `s` is even —361the quotient of the record by `⟨I_q²⟩ = ⟨[T]^π⟩` returns `s mod 2`, and the kernel of the forgetting is362`{id, J}`. -/363theorem record_mem_parity_iff (s : ZMod 4) :364    record κ s ∈ AddSubgroup.zmultiples (2 • flag κ) ↔ 2 ∣ s.val := by365  obtain ⟨v, hv, rfl⟩ : ∃ v : ℕ, v < 4 ∧ s = (v : ZMod 4) :=366    ⟨s.val, s.val_lt, (ZMod.natCast_zmod_val s).symm⟩367  rw [record_natCast, ZMod.val_natCast, Nat.mod_eq_of_lt hv]368  interval_cases v369  · simp370  · rw [one_smul]371    refine ⟨fun h => ?_, fun h => by omega⟩372    exact absurd (two_smul_of_mem_parity κ _ h) (two_smul_flag_ne_zero κ)373  · exact ⟨fun _ => dvd_refl 2, fun _ => AddSubgroup.mem_zmultiples _⟩374  · refine ⟨fun h => ?_, fun h => by omega⟩375    have h2 := two_smul_of_mem_parity κ _ h376    rw [smul_smul, show 2 * 3 = 4 + 2 from rfl, add_nsmul, four_smul_flag, zero_add] at h2377    exact absurd h2 (two_smul_flag_ne_zero κ)378379end timefactor380381/-! ## The chart duality and the crossed duality (10:D1, 10:D6) -/382section duality383384variable (κ : ℕ)385386/-- 10:D1 — the chart duality `δ_S : D ↦ D⁻¹`, an automorphism of the domain group. -/387def deltaS : Dom κ ≃+ Dom κ := AddEquiv.neg _388389/-- 10:D1 — `δ_S` is an involution. -/390theorem deltaS_involutive (a : Dom κ) : deltaS κ (deltaS κ a) = a := neg_neg a391392/-- 10:D1 — the orbit of `δ_S` on the generators: `[L] ↦ [L]⁻¹` (the momentum chart), `[T] ↦ [T]⁻¹` (the393energy chart). -/394theorem deltaS_generators : deltaS κ (L κ) = -L κ ∧ deltaS κ (T κ) = -T κ := ⟨rfl, rfl⟩395396/-- 10:D1 — the four labels `[L], [L]⁻¹, [T], [T]⁻¹` are pairwise distinct (`κ ≥ 1`): the orbit is the397four-domain structure. -/398theorem four_domains [NeZero κ] :399    L κ ≠ -L κ ∧ T κ ≠ -T κ ∧ L κ ≠ T κ ∧ L κ ≠ -T κ ∧ -L κ ≠ T κ ∧ -L κ ≠ -T κ := by400  have : Fact (2 < 4 * κ + 1) := ⟨by have := NeZero.pos κ; omega⟩401  have : Fact (2 < 4 * κ) := ⟨by have := NeZero.pos κ; omega⟩402  have : Fact (1 < 4 * κ + 1) := ⟨by have := NeZero.pos κ; omega⟩403  refine ⟨fun h => ?_, fun h => ?_, fun h => ?_, fun h => ?_, fun h => ?_, fun h => ?_⟩404  · have := congrArg Prod.fst h; simp [L] at this; exact ZMod.neg_one_ne_one this.symm405  · have := congrArg Prod.snd h; simp [T] at this; exact ZMod.neg_one_ne_one this.symm406  · have := congrArg Prod.fst h; simp [L, T] at this407  · have := congrArg Prod.fst h; simp [L, T] at this408  · have := congrArg Prod.fst h; simp [L, T] at this409  · have := congrArg Prod.fst h; simp [L, T] at this410411/-- 10:D6 — the flagged reading of frequency: the energy domain `[E] = [h][f] = I_q [T]⁻¹`. -/412def energy : Dom κ := flag κ - T κ413414/-- 10:D6 — the flagged reading of wavenumber: the momentum domain `[p] = [ħ][k] = I_q [L]⁻¹`. -/415def mom : Dom κ := flag κ - L κ416417/-- 10:D1, 10:E8 — the crossed duality `δ_C = I_q δ_S : D ↦ I_q D⁻¹`, the primal-to-dual passage of the418Carrier register. -/419def deltaC (a : Dom κ) : Dom κ := flag κ - a420421/-- 10:D1 — `δ_C` is an involution: `δ_C²(D) = I_q (I_q D⁻¹)⁻¹ = D`. -/422theorem deltaC_involutive (a : Dom κ) : deltaC κ (deltaC κ a) = a := sub_sub_cancel _ _423424/-- 10:D1 — `δ_C` carries `[L] ↦ [p]` and `[T] ↦ [E]`: the dual horizons are the flag-crossed images of the425primal charts, while `δ_S` is flag-free. -/426theorem deltaC_generators : deltaC κ (L κ) = mom κ ∧ deltaC κ (T κ) = energy κ := ⟨rfl, rfl⟩427428/-- 10:D6 — the flagged readings sit one capacity step above their counts: `[E] = [T]^{κ−1}` and429`[p] = [L]^{−1}[T]^κ` on the realized lattice; `[S] = [E][T] = I_q` and the phase counts are neutral,430`[E][T][ħ]⁻¹ = 1`, `[p][L][ħ]⁻¹ = 1`. -/431theorem flagged_readings :432    energy κ = (0, (κ : ZMod (4 * κ)) - 1) ∧ mom κ = (-1, (κ : ZMod (4 * κ))) ∧433    energy κ + T κ = flag κ ∧ energy κ + T κ - flag κ = 0 ∧ mom κ + L κ - flag κ = 0 := by434  refine ⟨?_, ?_, sub_add_cancel _ _, ?_, ?_⟩435  · ext <;> simp [energy, flag, T]436  · ext <;> simp [mom, flag, L]437  · rw [energy, sub_add_cancel, sub_self]438  · rw [mom, sub_add_cancel, sub_self]439440/-- 10:D6 — the flag is horizon-inaccessible: no in-window label `(r, s)` with `|s| ≤ H < κ` realizes441`I_q = (0, κ)`, since `s ≡ κ (mod 4κ)` with `|κ − s| < 2κ` and `κ − s ≠ 0` is impossible; at442`κ ≤ H < 2κ` the chart monomial `[T]^κ` itself is the flag. -/443theorem flag_inaccessible (H : ℕ) (hH : H < κ) (r s : ℤ) (hs : |s| ≤ H) :444    ((r : ZMod (4 * κ + 1)), (s : ZMod (4 * κ))) ≠ flag κ ∧445    ((0 : ZMod (4 * κ + 1)), ((κ : ℤ) : ZMod (4 * κ))) = flag κ := by446  refine ⟨fun h => ?_, by simp [flag]⟩447  have h2 := congrArg Prod.snd h448  simp only [flag] at h2449  rw [← Int.cast_natCast κ, ZMod.intCast_eq_intCast_iff_dvd_sub] at h2450  have hb := abs_le.mp hs451  have := Int.eq_zero_of_abs_lt_dvd h2 (abs_lt.mpr ⟨by push_cast; omega, by push_cast; omega⟩)452  omega453454end duality455456/-! ## The internal flag on the prime shell (10:D2) -/457section flagprime458459variable (κ : ℕ) [NeZero κ] [hp : Fact (Nat.Prime (4 * κ + 1))]460461omit [NeZero κ] in462/-- 10:D2, 10:X3 — no flag of space: `4r = 0` in `C_p` forces `r = 0` (`p` an odd prime), so the meridian factor463contributes no element of order four. -/464theorem no_flag_of_space (r : ZMod (4 * κ + 1)) (h : 4 * r = 0) : r = 0 := by465  have h4 : (4 : ZMod (4 * κ + 1)) ≠ 0 := by466    rw [show (4 : ZMod (4 * κ + 1)) = ((4 : ℕ) : ZMod (4 * κ + 1)) by norm_cast, Ne,467      ZMod.natCast_eq_zero_iff]468    intro hd469    have h1 : 4 * κ + 1 ≤ 4 := Nat.le_of_dvd (by norm_num) hd470    have h2 : 2 ≤ 4 * κ + 1 := hp.out.two_le471    omega472  rcases mul_eq_zero.mp h with h | h473  · exact absurd h h4474  · exact h475476/-- `2r = 0` in `C_p` forces `r = 0`. -/477theorem two_mul_eq_zero (r : ZMod (4 * κ + 1)) (h : 2 * r = 0) : r = 0 := by478  have h2 : (2 : ZMod (4 * κ + 1)) ≠ 0 := by479    rw [show (2 : ZMod (4 * κ + 1)) = ((2 : ℕ) : ZMod (4 * κ + 1)) by norm_cast, Ne,480      ZMod.natCast_eq_zero_iff]481    intro hd482    have h1 : 4 * κ + 1 ≤ 2 := Nat.le_of_dvd (by norm_num) hd483    have h2 := NeZero.pos κ484    omega485  rcases mul_eq_zero.mp h with h | h486  · exact absurd h h2487  · exact h488489/-- 10:D2 — the elements of order four of `D_p` are exactly `I_q = (0, κ)` and `I_q⁻¹ = (0, 3κ)`: every one490lies in the time-exponent factor. -/491theorem order_four_iff (x : Dom κ) : addOrderOf x = 4 ↔ x = flag κ ∨ x = -flag κ := by492  constructor493  · intro h494    rw [addOrderOf_eq_iff (by norm_num)] at h495    obtain ⟨h4, hlt⟩ := h496    obtain ⟨r, s⟩ := x497    have h4' := h4498    rw [Prod.smul_mk, Prod.mk_eq_zero, nsmul_eq_mul, nsmul_eq_mul] at h4'499    obtain ⟨hr, hs⟩ := h4'500    have hr0 : r = 0 := no_flag_of_space κ r (by exact_mod_cast hr)501    subst hr0502    have hs' := (four_mul_eq_zero_iff κ s).mp (by exact_mod_cast hs)503    rcases hs' with rfl | rfl | rfl | rfl504    · exact absurd (by simp) (hlt 1 (by norm_num) (by norm_num))505    · left; rfl506    · exfalso507      apply hlt 2 (by norm_num) (by norm_num)508      ext509      · simp510      · simp only [Prod.smul_mk, nsmul_eq_mul, Nat.cast_ofNat, Prod.snd_zero]511        linear_combination four_kappa κ512    · right; ext513      · show (0 : ZMod (4 * κ + 1)) = -(0 : ZMod (4 * κ + 1)); exact neg_zero.symm514      · show 3 * (κ : ZMod (4 * κ)) = -(κ : ZMod (4 * κ)); exact three_kappa κ515  · rintro (rfl | rfl)516    · exact addOrderOf_flag κ517    · exact addOrderOf_neg_flag κ518519/-- 10:D2 — the one element of order two of `D_p` is the half-period `I_q² = (0, 2κ)`. -/520theorem order_two_iff (x : Dom κ) : addOrderOf x = 2 ↔ x = 2 • flag κ := by521  constructor522  · intro h523    rw [addOrderOf_eq_iff (by norm_num)] at h524    obtain ⟨h2, hlt⟩ := h525    obtain ⟨r, s⟩ := x526    have h2' := h2527    rw [Prod.smul_mk, Prod.mk_eq_zero, nsmul_eq_mul, nsmul_eq_mul] at h2'528    obtain ⟨hr, hs⟩ := h2'529    have hr0 : r = 0 := two_mul_eq_zero κ r (by exact_mod_cast hr)530    subst hr0531    have hs' := (two_mul_eq_zero_iff κ s).mp (by exact_mod_cast hs)532    rcases hs' with rfl | rfl533    · exact absurd (by simp) (hlt 1 (by norm_num) (by norm_num))534    · rw [two_smul_flag]535  · rintro rfl536    rw [addOrderOf_eq_iff (by norm_num)]537    refine ⟨?_, fun m hm hm0 => ?_⟩538    · rw [smul_smul, show 2 * 2 = 4 from rfl]; exact four_smul_flag κ539    · interval_cases m; rw [one_smul]; exact two_smul_flag_ne_zero κ540541/-- 10:D2, 10:X3 — `D_p` contains exactly one subgroup of order four, `⟨I_q⟩ = {1, I_q, I_q², I_q³}`. -/542theorem unique_order_four_subgroup (H : AddSubgroup (Dom κ)) (hH : Nat.card H = 4) :543    H = AddSubgroup.zmultiples (flag κ) := by544  have horder : ∀ x ∈ H, addOrderOf x ∣ 4 := fun x hx => by545    have := addOrderOf_dvd_natCard (⟨x, hx⟩ : H)546    rw [← AddSubgroup.addOrderOf_coe, hH] at this547    exact this548  by_cases hex : ∃ x ∈ H, addOrderOf x = 4549  · obtain ⟨x, hx, hx4⟩ := hex550    have hflag : flag κ ∈ H := by551      rcases (order_four_iff κ x).mp hx4 with rfl | rfl552      · exact hx553      · exact H.neg_mem_iff.mp hx554    have hle : AddSubgroup.zmultiples (flag κ) ≤ H := by555      rw [AddSubgroup.zmultiples_le]; exact hflag556    symm557    refine AddSubgroup.eq_of_le_of_card_ge hle ?_558    rw [hH, Nat.card_zmultiples, addOrderOf_flag]559  · exfalso560    have hex' : ∀ x ∈ H, addOrderOf x ≠ 4 := fun x hx h4 => hex ⟨x, hx, h4⟩561    -- every element has order one or two, so `H ≤ ⟨I_q²⟩`, of order two562    have hle : H ≤ AddSubgroup.zmultiples (2 • flag κ) := by563      intro x hx564      have hd : addOrderOf x ∣ 2 ^ 2 := horder x hx565      rw [Nat.dvd_prime_pow Nat.prime_two] at hd566      obtain ⟨k, hk, hk'⟩ := hd567      interval_cases k568      · rw [pow_zero] at hk'569        have h1 : 1 • x = 0 := addOrderOf_dvd_iff_nsmul_eq_zero.mp (by rw [hk'])570        rw [one_smul] at h1571        rw [h1]; exact zero_mem _572      · rw [pow_one, order_two_iff] at hk'573        rw [hk']; exact AddSubgroup.mem_zmultiples _574      · exact absurd hk' (hex' x hx)575    have hcard := AddSubgroup.card_le_of_le hle576    rw [hH, Nat.card_zmultiples, (order_two_iff κ _).mpr rfl] at hcard577    omega578579end flagprime580581/-! ## The lift: the operator four-cycle and the Carrier face (10:D3) -/582section lift583584/-- 10:D3 — the operator four-cycle behind the lift, on the shell `F_p`, `p = 4κ + 1`: `F = i W` with585`i = −g^κ` has `F² = J` and `F⁴ = 1` (6-fourier's B7, `FRC.DFT.shell_relations`), and `F² = J ≠ 1` since586`J` exchanges the index `1` with `−1 ≠ 1` on a cycle of length `4κ ≥ 4`: the operator has order four, its587square the parity. -/588theorem operator_four_cycle (κ : ℕ) [NeZero κ] [Fact (Nat.Prime (4 * κ + 1))]589    (g : ZMod (4 * κ + 1)) (hg : IsPrimitiveRoot g (Fintype.card (ZMod (4 * κ + 1)) - 1)) :590    haveI : NeZero (Fintype.card (ZMod (4 * κ + 1)) - 1) :=591      ⟨by have := Fintype.one_lt_card (α := ZMod (4 * κ + 1)); omega⟩592    ((-(g ^ κ)) • FRC.DFT.W g : Matrix (Fin (Fintype.card (ZMod (4 * κ + 1)) - 1))593        (Fin (Fintype.card (ZMod (4 * κ + 1)) - 1)) (ZMod (4 * κ + 1))) ^ 2 = FRC.DFT.J ∧594    ((-(g ^ κ)) • FRC.DFT.W g : Matrix (Fin (Fintype.card (ZMod (4 * κ + 1)) - 1))595        (Fin (Fintype.card (ZMod (4 * κ + 1)) - 1)) (ZMod (4 * κ + 1))) ^ 4 = 1 ∧596    (FRC.DFT.J : Matrix (Fin (Fintype.card (ZMod (4 * κ + 1)) - 1))597        (Fin (Fintype.card (ZMod (4 * κ + 1)) - 1)) (ZMod (4 * κ + 1))) ≠ 1 := by598  have : NeZero (Fintype.card (ZMod (4 * κ + 1)) - 1) :=599    ⟨by have := Fintype.one_lt_card (α := ZMod (4 * κ + 1)); omega⟩600  have hc : Fintype.card (ZMod (4 * κ + 1)) = 4 * κ + 1 := ZMod.card _601  obtain ⟨-, hF2, hF4, -⟩ := FRC.DFT.shell_relations κ hc g hg602  refine ⟨hF2, hF4, fun hJ => ?_⟩603  have hn : 4 ≤ Fintype.card (ZMod (4 * κ + 1)) - 1 := by604    rw [hc]; have := NeZero.pos κ; omega605  have h1 : ((1 : Fin (Fintype.card (ZMod (4 * κ + 1)) - 1)) : ℕ) = 1 := by606    rw [Fin.val_one']; exact Nat.mod_eq_of_lt (by omega)607  have hne : (1 : Fin (Fintype.card (ZMod (4 * κ + 1)) - 1)) ≠ -1 := by608    intro h609    have h0 : (1 : Fin (Fintype.card (ZMod (4 * κ + 1)) - 1)) ≠ 0 := by610      intro h0; have := congrArg Fin.val h0; rw [h1] at this; exact one_ne_zero this611    have := congrArg Fin.val h612    simp only [Fin.val_neg, h0, ite_false, h1] at this613    omega614  have := congrFun (congrFun hJ 1) (-1)615  rw [Matrix.one_apply_ne hne] at this616  simp [FRC.DFT.J] at this617618/-- 10:D3 — the Carrier face of the lift: the crossing quantum `ħ` with `ħ² ≡ −1 (mod Ω)` has `ħ⁴ = 1` and619`ħ² ≠ 1` — two crossings the half-turn, four the identity, never two (`Ω > 2`). -/620theorem crossing_order_four {Ω : ℕ} [Fact (2 < Ω)] (hbar : ZMod Ω) (h : hbar ^ 2 = -1) :621    hbar ^ 4 = 1 ∧ hbar ^ 2 ≠ 1 := by622  refine ⟨by rw [show (4 : ℕ) = 2 * 2 from rfl, pow_mul, h]; norm_num, ?_⟩623  rw [h]; exact ZMod.neg_one_ne_one624625end lift626627/-! ## Window covariance (10:C5) -/628section covariance629630variable (κ : ℕ) [NeZero κ]631632/-- 10:C5, 10:D3 — invariance under the pushforward `u ↦ εu` of every unit `ε` of `C_{4κ}` holds exactly on633the cardinal pair `{0, 2κ}`: `ε = −1` is always admissible and forces `2u = 0`; conversely every unit is634odd, so it fixes the half-period. -/635theorem invariant_iff (u : ZMod (4 * κ)) :636    (∀ ε : (ZMod (4 * κ))ˣ, (ε : ZMod (4 * κ)) * u = u) ↔ u = 0 ∨ u = 2 * (κ : ZMod (4 * κ)) := by637  constructor638  · intro h639    have := h (-1)640    rw [Units.val_neg, Units.val_one, neg_one_mul] at this641    exact (two_mul_eq_zero_iff κ u).mp (by linear_combination -this)642  · rintro (rfl | rfl) ε643    · exact mul_zero _644    · obtain ⟨m, hm⟩ := unit_mul κ ε (2 * (κ : ZMod (4 * κ)))645      rw [hm]646      have : ((2 * m + 1 : ℕ) : ZMod (4 * κ)) * (2 * (κ : ZMod (4 * κ)))647          = ((m * (4 * κ) : ℕ) : ZMod (4 * κ)) + 2 * (κ : ZMod (4 * κ)) := by push_cast; ring648      rw [this, Nat.cast_mul, ZMod.natCast_self, mul_zero, zero_add]649650/-- 10:C5 — the sharpness of the window bound: the half-period label `(0, π)`, `π = 2κ`, is invariant under651every re-presentation and is not neutral. -/652theorem half_period_invariant_not_neutral :653    (∀ ε : (ZMod (4 * κ))ˣ, (ε : ZMod (4 * κ)) * (2 * (κ : ZMod (4 * κ))) = 2 * (κ : ZMod (4 * κ))) ∧654    2 * (κ : ZMod (4 * κ)) ≠ 0 :=655  ⟨(invariant_iff κ _).mpr (Or.inr rfl), two_kappa_ne_zero κ⟩656657/-- 10:C5 — the flagged label `(0, 0; 1)` moves under `ε = −1`: its realization `κ` goes to `3κ ≠ κ`, so658the flag-free restriction of window covariance cannot be dropped. -/659theorem flag_moves : -(κ : ZMod (4 * κ)) ≠ (κ : ZMod (4 * κ)) := by660  intro h661  exact two_kappa_ne_zero κ (by linear_combination -h)662663/-- 10:C5, 10:D2 — the quarter-turn labels `±κ` are fixed or exchanged by the pushforward exactly as664`ε mod 4 ∈ {1, 3}`: `ε κ ≡ (ε mod 4) κ (mod 4κ)`, so `εκ = κ` for `ε ≡ 1` and `εκ = 3κ = −κ` for665`ε ≡ 3`; the flag subgroup is preserved and its generator fixed or conjugated, as the residue quarter-turn666`±i` is. -/667theorem quarter_turn_law (ε : (ZMod (4 * κ))ˣ) :668    ((ε : ZMod (4 * κ)).val % 4 = 1 ∧ (ε : ZMod (4 * κ)) * κ = κ) ∨669    ((ε : ZMod (4 * κ)).val % 4 = 3 ∧ (ε : ZMod (4 * κ)) * κ = -(κ : ZMod (4 * κ))) := by670  obtain ⟨m, hm⟩ := unit_odd κ ε671  rcases Nat.even_or_odd m with ⟨k, hk⟩ | ⟨k, hk⟩672  · left673    refine ⟨by omega, ?_⟩674    rw [← ZMod.natCast_zmod_val (ε : ZMod (4 * κ)), hm, hk]675    have : ((2 * (k + k) + 1 : ℕ) : ZMod (4 * κ)) * κ676        = ((k * (4 * κ) : ℕ) : ZMod (4 * κ)) + κ := by push_cast; ring677    rw [this, Nat.cast_mul, ZMod.natCast_self, mul_zero, zero_add]678  · right679    refine ⟨by omega, ?_⟩680    rw [← ZMod.natCast_zmod_val (ε : ZMod (4 * κ)), hm, hk]681    have : ((2 * (2 * k + 1) + 1 : ℕ) : ZMod (4 * κ)) * κ682        = ((k * (4 * κ) : ℕ) : ZMod (4 * κ)) + 3 * κ := by push_cast; ring683    rw [this, Nat.cast_mul, ZMod.natCast_self, mul_zero, zero_add, three_kappa]684685omit [NeZero κ] in686/-- 10:C5 — the `σ`-twisted lift of the pushforward: for `4 ∣ ε − σ` (so `σ = ±1` as `ε ≡ 1, 3 (mod 4)`),687`ε(s + jκ) ≡ εs + σ jκ (mod 4κ)` — the integer formula `(r, s; j) ↦ (r, εs; σ(ε) j)` is a lift688representative of the action `u ↦ εu` on the realized coordinate `u = s + jκ`, exact as a congruence. -/689theorem sigma_twist (ε σ s j : ℤ) (hσ : (4 : ℤ) ∣ ε - σ) :690    ((ε * (s + j * κ) : ℤ) : ZMod (4 * κ)) = ((ε * s + σ * j * κ : ℤ) : ZMod (4 * κ)) := by691  rw [ZMod.intCast_eq_intCast_iff_dvd_sub]692  obtain ⟨m, hm⟩ := hσ693  have hσ' : σ = ε - 4 * m := by linear_combination -hm694  subst hσ'695  exact ⟨-(m * j), by push_cast; ring⟩696697omit [NeZero κ] in698/-- 10:C5 — the dilation character on the lift: for a primitive `m` (of order `p − 1`), `m^{−r} = 1` iff699`(p − 1) ∣ r`; on a window `|r| ≤ H < 2κ < p − 1` this forces `r = 0` — in-window invariance under every700dilation is `r = 0`. -/701theorem dilation_character (m : (ZMod (4 * κ + 1))ˣ) (hm : orderOf m = 4 * κ) (r : ℤ) :702    (m ^ (-r) = 1 ↔ ((4 * κ : ℕ) : ℤ) ∣ r) ∧703    (∀ H : ℕ, H < 2 * κ → |r| ≤ H → m ^ (-r) = 1 → r = 0) := by704  have key : m ^ (-r) = 1 ↔ ((4 * κ : ℕ) : ℤ) ∣ r := by705    rw [← orderOf_dvd_iff_zpow_eq_one, hm, dvd_neg]706  refine ⟨key, fun H hH hr h => ?_⟩707  have hd := key.mp h708  have hb := abs_le.mp hr709  refine Int.eq_zero_of_abs_lt_dvd hd (abs_lt.mpr ⟨?_, ?_⟩) <;> push_cast <;> omega710711/-- 10:C5 — the boundary witnesses on `F_13` (`κ = 3`, `2⁻¹ = 7`, `5⁻¹ = 8`): the naive character is712ill-defined on the modular projection (`7³ ≠ 7¹⁶` although `3 ≡ 16 (mod 13)`), and the would-be temporal713character fails composition (`5² ≡ 1` in `Z_12^×` while `(5⁻¹)² ≠ 1` in `F_13`). -/714theorem witnesses13 :715    (2 : ZMod 13) * 7 = 1 ∧ (7 : ZMod 13) ^ 3 ≠ (7 : ZMod 13) ^ 16 ∧ (3 : ZMod 13) = 16 ∧716    (5 : ZMod 12) * 5 = 1 ∧ (5 : ZMod 13) * 8 = 1 ∧ (8 : ZMod 13) ^ 2 ≠ 1 := by717  decide718719end covariance720721/-! ## The unit face of the quartet (10:E1–E3) -/722section unitface723724variable {K : Type*} [Field K]725726/-- 10:E1, 10:E2, 10:X3 — one crossing, one action: with the dual horizons the crossed images `p_P = ħ/ℓ_P`,727`E_P = ħ/t_P`, the quartet satisfies the single identity `ℓ_P p_P = t_P E_P = ħ`. -/728theorem action_identity (l t hbar : K) (hl : l ≠ 0) (ht : t ≠ 0) :729    l * (hbar / l) = hbar ∧ t * (hbar / t) = hbar :=730  ⟨mul_div_cancel₀ hbar hl, mul_div_cancel₀ hbar ht⟩731732/-- 10:E2, 10:X1 — the relation lattice has rank `4 − 1 = 3`: a quartet `(ℓ, t, p, E)` of scales with `ℓ, t ≠ 0`733satisfies `ℓp = tE` exactly when it is `(ℓ, t, ħ/ℓ, ħ/t)` for the one value `ħ = ℓp` — three free scales,734in bijection with the primitive triple `(ℓ_P, t_P, ħ)`. -/735theorem quartet_param (l t p E : K) (hl : l ≠ 0) (ht : t ≠ 0) :736    l * p = t * E ↔ (p = (l * p) / l ∧ E = (l * p) / t) := by737  constructor738  · intro h739    refine ⟨by rw [mul_div_cancel_left₀ p hl], ?_⟩740    rw [h, mul_div_cancel_left₀ E ht]741  · rintro ⟨-, hE⟩742    rw [hE, mul_div_cancel₀ _ ht]743744/-- 10:E2 — pairing closure: the cross-domain relations reduce to `c` and `ħ` — the two faces of `c` agree,745`ℓ/t = E/p`; the mixed products are their monomials, `|k_B| = p t = ħ/c` and `ℓE = ħ c`. -/746theorem pairing_closure (l t p E : K) (hl : l ≠ 0) (ht : t ≠ 0) (hp : p ≠ 0) (h : l * p = t * E) :747    l / t = E / p ∧ p * t = (l * p) / (l / t) ∧ l * E = (l * p) * (l / t) := by748  refine ⟨?_, ?_, ?_⟩749  · rw [div_eq_div_iff ht hp]; linear_combination h750  · rw [eq_div_iff (div_ne_zero hl ht), mul_div_assoc', div_eq_iff ht]; ring751  · rw [mul_div_assoc', eq_div_iff ht]; linear_combination (-l) * h752753/-- 10:E3, 10:X1, 10:X2 — the cancellation identity `|k_B| c = ħ` at the unit face, `(p t)(ℓ/t) = ℓ p`; mass derived,754`m_P = p/c = E/c²`; the temperature horizon `Θ_P = E/|k_B| = E c/ħ`. -/755theorem cancellation (l t p E : K) (hl : l ≠ 0) (ht : t ≠ 0) (hp : p ≠ 0) (h : l * p = t * E) :756    (p * t) * (l / t) = l * p ∧ p / (l / t) = E / (l / t) ^ 2 ∧ E / (p * t) = E * (l / t) / (l * p) := by757  have hc : l / t ≠ 0 := div_ne_zero hl ht758  refine ⟨?_, ?_, ?_⟩759  · rw [mul_div_assoc', div_eq_iff ht]; ring760  · rw [div_eq_div_iff hc (pow_ne_zero 2 hc), div_pow, mul_div_assoc', mul_div_assoc',761      div_eq_div_iff (pow_ne_zero 2 ht) ht]762    linear_combination (l * t) * h763  · rw [mul_div_assoc', div_div, div_eq_div_iff (mul_ne_zero hp ht) (mul_ne_zero ht (mul_ne_zero hl hp))]764    ring765766/-- 10:E2 — the normalisation to the totality, `G = ħ c / m_P² = ℓ² c³ / ħ`, and the recovery of the free767scale, `ℓ² = G ħ / c³`, `t = ℓ/c`, `p = ħ/ℓ`, `E = ħ c/ℓ`: `(c, ħ, G)` and `(ℓ_P, t_P, ħ)` carry the same768three scales, monomially in one direction and by the square of `ℓ` in the other. -/769theorem normalisation (l t p E : K) (hl : l ≠ 0) (ht : t ≠ 0) (hp : p ≠ 0) (h : l * p = t * E) :770    (l * p) * (l / t) / (p / (l / t)) ^ 2 = l ^ 2 * (l / t) ^ 3 / (l * p) ∧771    l ^ 2 = ((l * p) * (l / t) / (p / (l / t)) ^ 2) * (l * p) / (l / t) ^ 3 ∧772    t = l / (l / t) ∧ p = (l * p) / l ∧ E = (l * p) * (l / t) / l := by773  refine ⟨?_, ?_, ?_, ?_, ?_⟩774  · field_simp775  · field_simp776  · rw [div_div_eq_mul_div, mul_div_cancel_left₀ t hl]777  · rw [mul_div_cancel_left₀ p hl]778  · rw [mul_div_assoc', eq_div_iff hl, eq_div_iff ht]; linear_combination (-l) * h779780/-- 10:E2 — the sublattice `⟨c, ħ, G⟩` has index two in the free lattice on `{ℓ_P, t_P, ħ}`: the exponent781matrix of `c = ℓ t⁻¹`, `ħ`, `G = ℓ⁵ t⁻³ ħ⁻¹` has determinant `−2`. -/782theorem index_two : Matrix.det !![(1 : ℤ), -1, 0; 0, 0, 1; 5, -3, -1] = -2 := by783  rw [Matrix.det_fin_three]; simp784785/-- 10:E2, 10:X1 — the positive root closes the bijection: for `c, ħ, G > 0` there is exactly one `ℓ > 0` with786`ℓ² = G ħ / c³`. -/787theorem scale_from_constants (c hbar G : ℝ) (hc : 0 < c) (hh : 0 < hbar) (hG : 0 < G) :788    ∃! l : ℝ, 0 < l ∧ l ^ 2 = G * hbar / c ^ 3 := by789  have hpos : 0 < G * hbar / c ^ 3 := by positivity790  refine ⟨Real.sqrt (G * hbar / c ^ 3), ⟨Real.sqrt_pos.mpr hpos, Real.sq_sqrt hpos.le⟩, ?_⟩791  rintro l ⟨hl, hl2⟩792  rw [← hl2, Real.sqrt_sq hl.le]793794/-- 10:E2 — the exponent vectors over `(ℓ, t, p, E)`: the two faces of `c` differ by the relation795`ℓ − t + p − E` (`ℓp = tE`), as do the two faces of `ħ`; `ℓE = ħ c` and `p t = ħ/c` as exponent identities. -/796theorem exponent_faces :797    (![1, -1, 0, 0] : Fin 4 → ℤ) - ![0, 0, -1, 1] = ![1, -1, 1, -1] ∧798    (![1, 0, 1, 0] : Fin 4 → ℤ) - ![0, 1, 0, 1] = ![1, -1, 1, -1] ∧799    (![1, 0, 0, 1] : Fin 4 → ℤ) = ![0, 1, 0, 1] + ![1, -1, 0, 0] ∧800    (![0, 1, 1, 0] : Fin 4 → ℤ) = ![0, 1, 0, 1] - ![0, 0, -1, 1] := by801  refine ⟨?_, ?_, ?_, ?_⟩ <;> (ext i; fin_cases i <;> rfl)802803end unitface804805/-! ## The defining congruences at pair level (10:E4, 10:E5) -/806section carrier807808variable {K : Type*} [Field K]809810/-- 10:E4, 21:C2 — the linear defining congruence: on the Carrier chart (`4S + 1 = 0`, `2 ≠ 0`), `2G + 1 = 0`811has the unique solution `G = 2S`, the half-cycle. -/812theorem G_unique (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) (h2 : (2 : K) ≠ 0) (x : K) :813    2 * x + 1 = 0 ↔ x = ((2 * S : ℕ) : K) := by814  push_cast at hΩ ⊢815  constructor816  · intro h817    apply mul_left_cancel₀ h2818    linear_combination h - hΩ819  · rintro rfl; linear_combination hΩ820821/-- 10:E4 — the linkage derived at pair level: `k_B² = −2` and `2c² = 1` give `(k_B c)² = −1`, so822`k_B c ∈ {ħ, −ħ}` for any root `ħ` of `−1`: `{±k_B}{±c} = {±ħ}`. -/823theorem linkage (k c h : K) (hk : k ^ 2 = -2) (hc : 2 * c ^ 2 = 1) (hh : h ^ 2 = -1) :824    (k * c) ^ 2 = -1 ∧ (k * c = h ∨ k * c = -h) := by825  have h1 : (k * c) ^ 2 = -1 := by rw [mul_pow, hk]; linear_combination -hc826  exact ⟨h1, sq_eq_sq_iff_eq_or_eq_neg.mp (h1.trans hh.symm)⟩827828/-- 10:E5 — the pair consequences, by field arithmetic from the defining congruences: `G = −c²`,829`G² = 4⁻¹`, `ħ⁴ = 1`, `(k_B c)² = −1`, and `(ħ c G⁻¹)² = −2`, so the monomial `ħ c G⁻¹` lands in the830pair `{±k_B}`. -/831theorem pair_consequences (G c h k : K) (h2 : (2 : K) ≠ 0) (hG : 2 * G + 1 = 0) (hc : 2 * c ^ 2 = 1)832    (hh : h ^ 2 = -1) (hk : k ^ 2 = -2) :833    G = -c ^ 2 ∧ G ^ 2 = 4⁻¹ ∧ h ^ 4 = 1 ∧ (k * c) ^ 2 = -1 ∧ (h * c * G⁻¹) ^ 2 = -2 ∧834    (h * c * G⁻¹ = k ∨ h * c * G⁻¹ = -k) := by835  have h4 : (4 : K) * G ^ 2 = 1 := by linear_combination (2 * G - 1) * hG836  have hG2 : G ^ 2 = 4⁻¹ := eq_inv_of_mul_eq_one_right h4837  have hm : (h * c * G⁻¹) ^ 2 = -2 := by838    rw [mul_pow, mul_pow, hh, inv_pow, hG2, inv_inv]; linear_combination (-2) * hc839  refine ⟨?_, hG2, ?_, (linkage k c h hk hc hh).1, hm, ?_⟩840  · apply mul_left_cancel₀ h2; linear_combination hG + hc841  · rw [show (4 : ℕ) = 2 * 2 from rfl, pow_mul, hh]; norm_num842  · exact sq_eq_sq_iff_eq_or_eq_neg.mp (hm.trans hk.symm)843844/-- 10:E5 — representative inertness: the quadratics are sign-blind, and with `k_B c = −ħ` at one845assignment the sign assignment `(σ_c, σ_ħ, σ_k)` keeps the linkage iff `σ_ħ = σ_c σ_k` — so exactly the846four assignments with `σ_ħ = σ_c σ_k` are admissible (`σ_c, σ_k` free), a `(Z/2)²`; every identity of847`pair_consequences` holds on each, and the `ħ`-flip relabels within `{ħ, h}`. -/848theorem sign_assignments (c h k sc sh sk : K) (hh0 : h ≠ 0) (hl : k * c = -h)849    (hsc : sc = 1 ∨ sc = -1) (hsh : sh = 1 ∨ sh = -1) (hsk : sk = 1 ∨ sk = -1) :850    ((sk * k) * (sc * c) = -(sh * h) ↔ sh = sc * sk) ∧851    (sc * c) ^ 2 = c ^ 2 ∧ (sh * h) ^ 2 = h ^ 2 ∧ (sk * k) ^ 2 = k ^ 2 := by852  refine ⟨?_, ?_, ?_, ?_⟩853  · have : (sk * k) * (sc * c) = -(sc * sk * h) := by linear_combination (sk * sc) * hl854    rw [this, neg_inj]855    constructor856    · intro e; exact (mul_right_cancel₀ hh0 e).symm857    · intro e; rw [e]858  · rcases hsc with rfl | rfl <;> ring859  · rcases hsh with rfl | rfl <;> ring860  · rcases hsk with rfl | rfl <;> ring861862/-- `−2` is a square when `−1` and `2` are (any commutative ring). -/863theorem isSquare_neg_two {R : Type*} [CommRing R] (h1 : IsSquare (-1 : R)) (h2 : IsSquare (2 : R)) :864    IsSquare (-2 : R) := by865  obtain ⟨a, ha⟩ := h1866  obtain ⟨b, hb⟩ := h2867  exact ⟨a * b, by linear_combination 2 * ha + (a * a) * hb⟩868869/-- 10:E4 — the `h`-form: `h = 2π ħ` with `2π = 4S ≡ −1` on the Carrier chart, so `h = −ħ` — the root870pair of `−1` is `{ħ, h}`. -/871theorem h_form (S : ℕ) (hΩ : ((4 * S + 1 : ℕ) : K) = 0) (hbar : K) :872    ((2 * (2 * S) : ℕ) : K) * hbar = -hbar := by873  push_cast at hΩ ⊢874  linear_combination hbar * hΩ875876end carrier877878section carrierZ879880variable (S : ℕ) [hΩ : Fact (Nat.Prime (4 * S + 1))]881882theorem omega_two_ne_zero : (2 : ZMod (4 * S + 1)) ≠ 0 := by883  rw [show (2 : ZMod (4 * S + 1)) = ((2 : ℕ) : ZMod (4 * S + 1)) by norm_cast, Ne,884    ZMod.natCast_eq_zero_iff]885  intro hd886  have h1 : 4 * S + 1 ≤ 2 := Nat.le_of_dvd (by norm_num) hd887  have h2 : 2 ≤ 4 * S + 1 := hΩ.out.two_le888  omega889890/-- 10:E4 — existence on every admissible Carrier: `Ω = 4S + 1 ≡ 1 (mod 4)` makes `−1` a square891unconditionally; `S` even is `Ω ≡ 1 (mod 8)`, which makes `2` and hence `2⁻¹` squares; `−2` is the product.892So the four defining congruences are solvable, and `G = 2S` is their linear solution. -/893theorem residues_exist (hS : Even S) :894    IsSquare (-1 : ZMod (4 * S + 1)) ∧ IsSquare (2 : ZMod (4 * S + 1)) ∧895    IsSquare ((2 : ZMod (4 * S + 1))⁻¹) ∧ IsSquare (-2 : ZMod (4 * S + 1)) ∧896    2 * ((2 * S : ℕ) : ZMod (4 * S + 1)) + 1 = 0 := by897  have h1 : IsSquare (-1 : ZMod (4 * S + 1)) := ZMod.exists_sq_eq_neg_one_iff.mpr (by omega)898  have h2 : IsSquare (2 : ZMod (4 * S + 1)) := by899    obtain ⟨m, hm⟩ := hS900    exact (ZMod.exists_sq_eq_two_iff (by omega)).mpr (Or.inl (by omega))901  refine ⟨h1, h2, h2.inv, ?_, ?_⟩902  · exact isSquare_neg_two h1 h2903  · have : ((4 * S + 1 : ℕ) : ZMod (4 * S + 1)) = 0 := ZMod.natCast_self _904    push_cast at this ⊢; linear_combination this905906omit [Fact (Nat.Prime (4 * S + 1))] in907/-- 10:E4 — the admissibility residues: `Ω = 4S + 1 ≡ 1 (mod 4)` for every `S`, and `S` even iff908`Ω ≡ 1 (mod 8)`. -/909theorem admissibility_residues : (4 * S + 1) % 4 = 1 ∧ (Even S ↔ (4 * S + 1) % 8 = 1) := by910  refine ⟨by omega, ?_⟩911  constructor912  · rintro ⟨m, hm⟩; omega913  · intro h; exact ⟨S / 2, by omega⟩914915end carrierZ916917/-- 10:E4, 10:E5 — the Carrier `Ω = 233` (`S = 58`, admissible: `58` even, `58 ≡ 1 (mod 3)`, `233` prime):918`G = 116 = 2S`, `ħ = 89`, `k_B = 124`, `c = 159`, `h = 144 = −ħ` satisfy the defining congruences, the919linkage `k_B c = −ħ`, `G = −c²`, `G² = 4⁻¹`, `ħ⁴ = 1`, and `ħ c = k_B G` (the monomial on the `k_B` residue);920the partner root `109 = −124` fails the linkage; decided in `ZMod 233`. -/921theorem carrier233 :922    Nat.Prime 233 ∧ 233 = 4 * 58 + 1 ∧ 58 % 2 = 0 ∧ 58 % 3 = 1 ∧923    2 * (116 : ZMod 233) + 1 = 0 ∧ (89 : ZMod 233) ^ 2 = -1 ∧ (124 : ZMod 233) ^ 2 = -2 ∧924    2 * (159 : ZMod 233) ^ 2 = 1 ∧ (124 : ZMod 233) * 159 = -89 ∧ (144 : ZMod 233) = -89 ∧925    (116 : ZMod 233) = -(159 : ZMod 233) ^ 2 ∧ 4 * (116 : ZMod 233) ^ 2 = 1 ∧926    (89 : ZMod 233) ^ 4 = 1 ∧ (89 : ZMod 233) * 159 = 124 * 116 ∧927    (109 : ZMod 233) = -124 ∧ (109 : ZMod 233) * 159 ≠ -89 := by928  refine ⟨by norm_num, ?_⟩; decide929930/-- 10:E4, 10:E5, 21:C5 — the laboratory Carrier `Ω = 2 408 561` (`S = 602 140`, admissible):931`G = 1 204 280 = 2S`, `ħ = 18 688`, `k_B = 1 880 160`, `c = 171 106`, `h = 2 389 873 = −ħ` satisfy the defining932congruences, the linkage, `G = −c²`, `G² = 4⁻¹`, `ħ⁴ = 1`, `ħ c = k_B G`; decided in `ZMod 2408561`. -/933theorem carrierLab :934    Nat.Prime 2408561 ∧ 2408561 = 4 * 602140 + 1 ∧ 602140 % 2 = 0 ∧ 602140 % 3 = 1 ∧935    2 * (1204280 : ZMod 2408561) + 1 = 0 ∧ (18688 : ZMod 2408561) ^ 2 = -1 ∧936    (1880160 : ZMod 2408561) ^ 2 = -2 ∧ 2 * (171106 : ZMod 2408561) ^ 2 = 1 ∧937    (1880160 : ZMod 2408561) * 171106 = -18688 ∧ (2389873 : ZMod 2408561) = -18688 ∧938    (1204280 : ZMod 2408561) = -(171106 : ZMod 2408561) ^ 2 ∧939    4 * (1204280 : ZMod 2408561) ^ 2 = 1 ∧ (18688 : ZMod 2408561) ^ 4 = 1 ∧940    (18688 : ZMod 2408561) * 171106 = 1880160 * 1204280 := by941  refine ⟨by norm_num, ?_⟩; decide942943/-! ## The lifted labels and the derived domains (10:D4, 10:F2–F4) -/944section labels945946/-- 10:D4 — the full label `(r, s; j)`: the two exponents and the integer crossing degree `j`. -/947abbrev Lab := ℤ × ℤ × ℤ948949/-- 10:D4 — the realization of the full label on the shell, `(r, s; j) ↦ U_{r, s + jκ}`. -/950def realize (κ : ℕ) : Lab →+ Dom κ where951  toFun x := ((x.1 : ZMod (4 * κ + 1)), ((x.2.1 + x.2.2 * κ : ℤ) : ZMod (4 * κ)))952  map_zero' := by simp953  map_add' x y := by ext <;> simp; ring954955/-- 10:D4 — realization is a homomorphism: the sector of a product is the sum of the sectors. -/956theorem realize_add (κ : ℕ) (x y : Lab) : realize κ (x + y) = realize κ x + realize κ y :=957  map_add _ x y958959/-- 10:D4 — the realized flag: `(0, 0; 1) ↦ I_q`. -/960theorem realize_flag (κ : ℕ) : realize κ (0, 0, 1) = flag κ := by961  ext <;> simp [realize, flag]962963/-- The labels of the paper's Table (lifted): speed `[L][T]⁻¹`; energy `I_q[T]⁻¹`; the flag; time. -/964def speedL : Lab := (1, -1, 0)965def timeL : Lab := (0, 1, 0)966def spaceL : Lab := (1, 0, 0)967def flagL : Lab := (0, 0, 1)968def energyL : Lab := (0, -1, 1)969def massL : Lab := (-2, 1, 1)970def accelL : Lab := (1, -2, 0)971def forceL : Lab := (-1, -1, 1)972def momL : Lab := (-1, 0, 1)973def actionL : Lab := (0, 0, 1)974def powerL : Lab := (0, -2, 1)975def pressureL : Lab := (-3, -1, 1)976def gravL : Lab := (5, -3, -1)977def kBL : Lab := (-1, 1, 1)978def thetaL : Lab := (1, -2, 0)979980/-- 10:F2, 10:X1 — the mechanical and gravitational domains from `[E] = I_q[T]⁻¹` and `[v] = [L][T]⁻¹`:981`[m] = [E][v]⁻² = I_q[L]⁻²[T]`, `[a] = [v][T]⁻¹`, `[F] = [m][a] = I_q[L]⁻¹[T]⁻¹`, `[p] = [m][v] = I_q[L]⁻¹`982(the flagged wavenumber `I_q[L]⁻¹` again), `[S] = [E][T] = I_q`, `[P] = [E][T]⁻¹ = I_q[T]⁻²`,983`[pressure] = [F][L]⁻² = I_q[L]⁻³[T]⁻¹`, `[G] = [F][L]²[m]⁻² = I_q⁻¹[L]⁵[T]⁻³`, and the quartet face984`[ħ][c][m]⁻² = [G]`; mass is derived, not primitive. -/985theorem mechanical_domains :986    massL = energyL - (2 : ℤ) • speedL ∧ massL = (-2, 1, 1) ∧987    accelL = speedL - timeL ∧ forceL = massL + accelL ∧ forceL = (-1, -1, 1) ∧988    momL = massL + speedL ∧ momL = flagL - spaceL ∧989    actionL = energyL + timeL ∧ actionL = flagL ∧990    powerL = energyL - timeL ∧ powerL = (0, -2, 1) ∧991    pressureL = forceL - (2 : ℤ) • spaceL ∧ pressureL = (-3, -1, 1) ∧992    gravL = forceL + (2 : ℤ) • spaceL - (2 : ℤ) • massL ∧ gravL = (5, -3, -1) ∧993    gravL = flagL + speedL - (2 : ℤ) • massL := by994  decide995996/-- 10:F2 — the geometric conversions are flag-free: `[Għ/c³] = [L]²`, `[Gm/c²] = [L]`, `[Gm/c³] = [T]`,997`[Gρ_m] = [T]⁻²`, `[Gρ_E/c⁴] = [L]⁻²` (the curvature domain), and the Compton closure `[mc/ħ] = [L]⁻¹`. -/998theorem geometric_conversions :999    gravL + flagL - (3 : ℤ) • speedL = (2, 0, 0) ∧1000    gravL + massL - (2 : ℤ) • speedL = (1, 0, 0) ∧1001    gravL + massL - (3 : ℤ) • speedL = (0, 1, 0) ∧1002    gravL + (massL - (3 : ℤ) • spaceL) = (0, -2, 0) ∧1003    gravL - (4 : ℤ) • speedL + (energyL - (3 : ℤ) • spaceL) = (-2, 0, 0) ∧1004    massL + speedL - flagL = (-1, 0, 0) := by1005  decide10061007/-- 10:F3, 10:X2 — temperature carries the acceleration domain: with `[k_B] = [p_P t_P] = I_q[L]⁻¹[T]`,1008`[Θ] = [E][k_B]⁻¹ = [L][T]⁻² = [a]`, flag-free; and the Unruh combination `[ħ a / (c k_B)] = [Θ]` closes1009flag-free. -/1010theorem temperature_domain :1011    thetaL = energyL - kBL ∧ thetaL = accelL ∧ thetaL.2.2 = 0 ∧1012    flagL + accelL - speedL - kBL = thetaL := by1013  decide10141015/-- 10:E3 — the flag positions of the quartet `(ℓ_P, t_P, p_P, E_P)` are `(0, 0, 1, 1)` — the dual horizons1016`p_P = ħ/ℓ_P`, `E_P = ħ/t_P` are the crossed images `[p] = I_q[L]⁻¹`, `[E] = I_q[T]⁻¹` — and every quartet1017relation closes on the flag component: `ħ = ℓ_P p_P` at `0 + 1 = 1`, `c = ℓ_P/t_P` at `0`, `c = E_P/p_P` at1018`1 − 1 = 0`, `|k_B| = p_P t_P` at `1`, `G = ℓ_P² c³/ħ` at `−1` (the inverse flag, `[G]`). -/1019theorem quartet_flags :1020    spaceL.2.2 = 0 ∧ timeL.2.2 = 0 ∧ momL.2.2 = 1 ∧ energyL.2.2 = 1 ∧1021    spaceL + momL = flagL ∧ (spaceL - timeL).2.2 = 0 ∧ (energyL - momL).2.2 = 0 ∧1022    momL + timeL = kBL ∧ (2 : ℤ) • spaceL + (3 : ℤ) • (spaceL - timeL) - (spaceL + momL) = gravL ∧1023    gravL.2.2 = -1 := by1024  decide10251026/-- 10:F4 — count-valued comparisons are flag-free: the ratio of two labels of equal crossing degree has1027crossing degree zero — the flag enters unitful measures only. -/1028theorem equal_crossing_flag_free (x y : Lab) (h : x.2.2 = y.2.2) : (x - y).2.2 = 0 := by1029  simp [h]10301031/-- 10:F4, 10:G3 — the examples: the phase exponent `[E][T]/[ħ]` neutral; the gravitational frequency1032`[Gm/r³] = [T]⁻²` flag-free; and the scope witness — `F/a = [m]` has crossing degree `1` (the degrees `1`1033and `0` are not equal), so the equal-crossing-degree hypothesis cannot be dropped. -/1034theorem comparison_examples :1035    energyL + timeL - flagL = 0 ∧ gravL + massL - (3 : ℤ) • spaceL = (0, -2, 0) ∧1036    (gravL + massL - (3 : ℤ) • spaceL).2.2 = 0 ∧1037    forceL - accelL = massL ∧ (forceL - accelL).2.2 = 1 ∧ forceL.2.2 ≠ accelL.2.2 := by1038  decide10391040end labels10411042/-! ## Local recovery, the window ladder, the examples and Buckingham's count (10:G1–G4) -/1043section recovery10441045/-- 10:G1 — local recovery of classical exponent bookkeeping: for `4κ > 2H`, two conventional pairs1046`(r, s)`, `(r', s')` with `|r|, |r'|, |s|, |s'| ≤ H` and the same modular label are equal. -/1047theorem local_recovery (κ H : ℕ) (hH : 2 * H < 4 * κ) (r r' s s' : ℤ) (hr : |r| ≤ H) (hr' : |r'| ≤ H)1048    (hs : |s| ≤ H) (hs' : |s'| ≤ H)1049    (h : ((r : ZMod (4 * κ + 1)), (s : ZMod (4 * κ))) = ((r' : ZMod (4 * κ + 1)), (s' : ZMod (4 * κ)))) :1050    r = r' ∧ s = s' := by1051  obtain ⟨h1, h2⟩ := Prod.ext_iff.mp h1052  rw [ZMod.intCast_eq_intCast_iff_dvd_sub] at h1 h21053  have hb := abs_le.mp hr; have hb' := abs_le.mp hr'1054  have hc := abs_le.mp hs; have hc' := abs_le.mp hs'1055  have e1 := Int.eq_zero_of_abs_lt_dvd h1 (abs_lt.mpr ⟨by push_cast; omega, by push_cast; omega⟩)1056  have e2 := Int.eq_zero_of_abs_lt_dvd h2 (abs_lt.mpr ⟨by push_cast; omega, by push_cast; omega⟩)1057  omega10581059/-- 10:G1 — the crossing embedding of classical `M`-`L`-`T` bookkeeping, `M^u L^a T^b ↦ (a − 2u, b + u; u)`. -/1060def embed (u a b : ℤ) : Lab := (a - 2 * u, b + u, u)10611062/-- 10:G1, 10:G4 — the embedding is injective on `Z³` (triangular with unit diagonal): the crossing degree1063carries the mass exponent exactly; the map being linear by its formula, the lifted label matrix of quantities1064with classical `M`-`L`-`T` dimensions has the kernel, hence the rank, of the classical one (G4). -/1065theorem embed_injective (u a b u' a' b' : ℤ) (h : embed u a b = embed u' a' b') :1066    u = u' ∧ a = a' ∧ b = b' := by1067  simp only [embed, Prod.ext_iff] at h1068  omega10691070/-- 10:G1 — windowed faithfulness of the realization: on `|r|, |s| ≤ H` with `2H < κ` and `|j| ≤ 1`, two1071full labels with the same realization `(r, s + jκ)` are equal — `r` from the meridian factor, and1072`(j − j')κ ≡ s' − s (mod 4κ)` with `|j − j'| ≤ 2`, `|s − s'| < κ` forces `j = j'` and then `s = s'`;1073beyond the window the sector saturates, `4 • I_q = 0`. -/1074theorem realize_faithful (κ H : ℕ) [NeZero κ] (hH : 2 * H < κ) (r r' s s' j j' : ℤ)1075    (hr : |r| ≤ H) (hr' : |r'| ≤ H) (hs : |s| ≤ H) (hs' : |s'| ≤ H) (hj : |j| ≤ 1) (hj' : |j'| ≤ 1)1076    (h : realize κ (r, s, j) = realize κ (r', s', j')) : r = r' ∧ s = s' ∧ j = j' := by1077  obtain ⟨h1, h2⟩ := Prod.ext_iff.mp h1078  simp only [realize, AddMonoidHom.coe_mk, ZeroHom.coe_mk] at h1 h21079  rw [ZMod.intCast_eq_intCast_iff_dvd_sub] at h1 h21080  have hb := abs_le.mp hr; have hb' := abs_le.mp hr'1081  have hc := abs_le.mp hs; have hc' := abs_le.mp hs'1082  have hd := abs_le.mp hj; have hd' := abs_le.mp hj'1083  have hκ : (0 : ℤ) < κ := by exact_mod_cast NeZero.pos κ1084  have e1 := Int.eq_zero_of_abs_lt_dvd h1 (abs_lt.mpr ⟨by push_cast; omega, by push_cast; omega⟩)1085  obtain ⟨m, hm⟩ := h21086  push_cast at hm1087  -- `(s' − s) + (j' − j)κ = 4κ m` with `|s' − s| < κ` and `|j' − j| ≤ 2` forces `m = 0`1088  have hm0 : m = 0 := by1089    rcases lt_trichotomy m 0 with hlt | heq | hgt1090    · exfalso1091      have : (4 : ℤ) * κ * m ≤ -4 * κ := by nlinarith1092      nlinarith1093    · exact heq1094    · exfalso1095      have : (4 : ℤ) * κ ≤ 4 * κ * m := by nlinarith1096      nlinarith1097  subst hm01098  -- now `(j' − j)κ = s − s'` with `|s − s'| < κ`, so `j = j'`1099  have hjj : j' - j = 0 := by1100    rcases lt_trichotomy (j' - j) 0 with hlt | heq | hgt1101    · exfalso1102      have : (j' - j) * κ ≤ -κ := by nlinarith1103      nlinarith1104    · exact heq1105    · exfalso1106      have : (κ : ℤ) ≤ (j' - j) * κ := by nlinarith1107      nlinarith1108  refine ⟨by omega, ?_, by omega⟩1109  have : (j' - j) * κ = 0 := by rw [hjj]; ring1110  nlinarith11111112/-- 10:G2 — the window ladder `2√κ < κ/2 < κ < 2κ`, by integer squares: `16κ < κ²` iff `κ > 16`, and1113`κ/2 < κ < 2κ` for `κ > 0` — nested for every `κ ≥ 17`, failing for the toy `κ = 3`; the coherence identity1114`(2√κ)² = 4κ = p − 1` and the totality closure `(2√S)² = 4S = Ω − 1`. -/1115theorem window_ladder (κ S : ℕ) :1116    (16 * κ < κ ^ 2 ↔ 16 < κ) ∧ (0 < κ → κ / 2 < κ ∧ κ < 2 * κ) ∧ ¬ (16 * 3 < 3 ^ 2) ∧1117    (2 * 2 * κ = 4 * κ ∧ 4 * κ = (4 * κ + 1) - 1) ∧ 4 * S = (4 * S + 1) - 1 := by1118  refine ⟨⟨fun h => ?_, fun h => ?_⟩, fun h => ⟨by omega, by omega⟩, by norm_num, ⟨by ring, by omega⟩,1119    by omega⟩1120  · by_contra hc; have hc' : κ ≤ 16 := Nat.le_of_not_lt hc; nlinarith1121  · nlinarith11221123instance fact13 : Fact (Nat.Prime (4 * 3 + 1)) := ⟨by norm_num⟩11241125/-- 10:G3 — the worked examples on the shell of capacity `κ = 3` (`p = 13`, phase cycle `12`): `12 > 10 = 2H`1126at `H = 5`; kinetic energy `[m][v]² = [E]`; `Q + Q²` inhomogeneous (`[L] ≠ [L]²`); the phase exponent1127neutral; flag arithmetic — `Għ/c³` flag-free, `I_q² = [T]^π = (0, 6)`; the Schwarzschild length1128`[Gm/c²] = [L]`; the gravitational frequency `[Gm/r³] = [T]⁻²`; the realized mass `(11, 4) = (−2, 1 + κ)`. -/1129theorem examples13 :1130    12 > 2 * 5 ∧ massL + (2 : ℤ) • speedL = energyL ∧ L 3 ≠ 2 • L 3 ∧1131    energyL + timeL - flagL = 0 ∧ (gravL + flagL - (3 : ℤ) • speedL).2.2 = 0 ∧1132    2 • flag 3 = ((0 : ZMod 13), (6 : ZMod 12)) ∧1133    gravL + massL - (2 : ℤ) • speedL = (1, 0, 0) ∧ gravL + massL - (3 : ℤ) • spaceL = (0, -2, 0) ∧1134    realize 3 massL = ((11 : ZMod 13), (4 : ZMod 12)) := by1135  refine ⟨by norm_num, by decide, by decide, by decide, by decide, ?_, by decide, by decide, ?_⟩1136  · rw [two_smul_flag]; decide1137  · ext <;> simp [realize, massL] <;> decide11381139/-- 10:G3 — local recovery on `κ = 3` at `H = 5`: the instance of the theorem. -/1140theorem recovery13 (r r' s s' : ℤ) (hr : |r| ≤ 5) (hr' : |r'| ≤ 5) (hs : |s| ≤ 5) (hs' : |s'| ≤ 5)1141    (h : ((r : ZMod 13), (s : ZMod 12)) = ((r' : ZMod 13), (s' : ZMod 12))) : r = r' ∧ s = s' :=1142  local_recovery 3 5 (by norm_num) r r' s s' hr hr' hs hs' h11431144/-- 10:G3 — the energy–momentum relation `E² = p²c² + m²c⁴` is homogeneous on the lift: the three labels1145`[E]²`, `[p]²[c]²`, `[m]²[c]⁴` coincide, `(0, −2; 2)`, one fibre at crossing degree two; its massless case1146`E = pc` at crossing degree one, and `E = mc²` on the energy fibre; realized on `κ = 3`, `[E]² = (0, 4)`,1147the lifted and the shell computation agreeing. -/1148theorem energy_momentum :1149    (2 : ℤ) • energyL = (2 : ℤ) • (momL + speedL) ∧ (2 : ℤ) • energyL = (2 : ℤ) • (massL + (2 : ℤ) • speedL) ∧1150    (2 : ℤ) • energyL = (0, -2, 2) ∧ ((2 : ℤ) • energyL).2.2 = 2 ∧1151    energyL = momL + speedL ∧ energyL.2.2 = 1 ∧ energyL = massL + (2 : ℤ) • speedL ∧1152    realize 3 ((2 : ℤ) • energyL) = ((0 : ZMod 13), (4 : ZMod 12)) ∧1153    2 • energy 3 = ((0 : ZMod 13), (4 : ZMod 12)) := by1154  decide11551156/-- 10:G4 — the window coincidence: on `|r|, |s| ≤ H` with `2H < κ` and `|j| ≤ 1`, a lifted label realizes to1157the neutral label iff it is `(0, 0; 0)` — lifted and realized neutrality coincide on the window (the1158instance of `realize_faithful` against the neutral label). -/1159theorem window_neutrality (κ H : ℕ) [NeZero κ] (hH : 2 * H < κ) (r s j : ℤ)1160    (hr : |r| ≤ H) (hs : |s| ≤ H) (hj : |j| ≤ 1) :1161    realize κ (r, s, j) = 0 ↔ (r, s, j) = (0, 0, 0) := by1162  constructor1163  · intro h1164    obtain ⟨h1, h2, h3⟩ := realize_faithful κ H hH r 0 s 0 j 0 hr (by simp) hs (by simp) hj (by simp)1165      (by rw [h]; exact (map_zero _).symm)1166    rw [h1, h2, h3]1167  · rintro ⟨⟩; exact map_zero _11681169/-- 10:G4 — Buckingham's count on the pendulum `(T, ℓ, g, m)`: the classical dimensions lie in `M`-`L`-`T`1170and embed to the lifted labels `[T] = (0, 1; 0)`, `[ℓ] = (1, 0; 0)`, `[g] = (1, −2; 0)`, `[m] = (−2, 1; 1)`;1171a monomial `T^{k₁} ℓ^{k₂} g^{k₃} m^{k₄}` is neutral on the lift iff `(k₁, k₂, k₃, k₄) = t·(2, −1, 1, 0)` —1172the kernel of the `4 × 3` label matrix is the line of `T²g/ℓ`, one dimensionless product, so the rank is1173`3 = 4 − 1` (the mass, alone in carrying crossing degree, enters no neutral product, `k₄ = 0`); the minor1174of the label matrix on the rows `(ℓ, g, m)` is `−2 ≠ 0`. -/1175theorem pendulum_kernel :1176    embed 0 0 1 = timeL ∧ embed 0 1 0 = spaceL ∧ embed 0 1 (-2) = accelL ∧ embed 1 0 0 = massL ∧1177    (∀ k₁ k₂ k₃ k₄ : ℤ, k₁ • timeL + k₂ • spaceL + k₃ • accelL + k₄ • massL = 0 ↔1178      ∃ t : ℤ, k₁ = 2 * t ∧ k₂ = -t ∧ k₃ = t ∧ k₄ = 0) ∧1179    (2 : ℤ) • timeL - spaceL + accelL = 0 ∧1180    Matrix.det !![spaceL.1, spaceL.2.1, spaceL.2.2; accelL.1, accelL.2.1, accelL.2.2;1181      massL.1, massL.2.1, massL.2.2] = -2 := by1182  refine ⟨by decide, by decide, by decide, by decide, fun k₁ k₂ k₃ k₄ => ?_, by decide, ?_⟩1183  · simp only [timeL, spaceL, accelL, massL, Prod.smul_mk, smul_eq_mul, Prod.mk_add_mk, Prod.mk_eq_zero]1184    constructor1185    · rintro ⟨h1, h2, h3⟩; exact ⟨k₃, by omega, by omega, rfl, by omega⟩1186    · rintro ⟨t, rfl, rfl, rfl, rfl⟩; omega1187  · rw [Matrix.det_fin_three]; simp [spaceL, accelL, massL]11881189end recovery11901191end11921193/-! ## Old names (ledger migration, task LM17): the declarations moved to the themes, each under its old name -/11941195section field_aliases1196variable {K : Type*} [Field K]11971198/-- 10:E4 — each quadratic defining congruence has exactly two roots, the pair `{x, −x}`: if `x² = a` with1199`x ≠ 0` (`2 ≠ 0`), then `y² = a` iff `y = x` or `y = −x`, and `−x ≠ x`. -/1200theorem root_pair (a x : K) (hx : x ^ 2 = a) (hx0 : x ≠ 0) (h2 : (2 : K) ≠ 0) :1201    (∀ y : K, y ^ 2 = a ↔ y = x ∨ y = -x) ∧ -x ≠ x :=1202  FRC.Frame.root_pair a x hx hx0 h212031204end field_aliases12051206-- Ledger predicates of 10-dimensions (generated by make_predicates.py from docs/10-dimensions/10-dimensions-ledger.json; edit the ledger, not this section)1207/-- 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')}$. -/1208theorem p10012 : (∀ (κ : ℕ) (a b : FRC.Dimensions.Dom κ), FRC.Dimensions.U κ a * FRC.Dimensions.U κ b = FRC.Dimensions.U κ (a + b)) ∧ (∀ (κ : ℕ) [NeZero κ], Function.Injective ⇑(FRC.Dimensions.Uhom κ)) ∧ ∀ (κ : ℕ) {x y : FRC.Dimensions.QA κ} {a b : FRC.Dimensions.Dom κ}, x ∈ AddMonoidAlgebra.grade (ZMod ((4 : ℕ) * κ + (1 : ℕ))) a → y ∈ AddMonoidAlgebra.grade (ZMod ((4 : ℕ) * κ + (1 : ℕ))) b → x * y ∈ AddMonoidAlgebra.grade (ZMod ((4 : ℕ) * κ + (1 : ℕ))) (a + b) :=1209  And.intro @FRC.Dimensions.U_mul (And.intro @FRC.Dimensions.Uhom_injective (@FRC.Dimensions.graded))1210/-- 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$. -/1211theorem p10013 : (∀ (κ : ℕ) (a : FRC.Dimensions.Dom κ) (q q' : ZMod ((4 : ℕ) * κ + (1 : ℕ))), AddMonoidAlgebra.single a q + AddMonoidAlgebra.single a q' = AddMonoidAlgebra.single a (q + q')) ∧ (∀ (κ : ℕ) {ι : Type u_1} (s : Finset ι) (m : ι → FRC.Dimensions.Dom κ) (q : ι → ZMod ((4 : ℕ) * κ + (1 : ℕ))) (a : FRC.Dimensions.Dom κ), (∑ j ∈ s, AddMonoidAlgebra.single (m j) (q j)).coeff a = ∑ j ∈ s with m j = a, q j) ∧ (∀ (κ : ℕ) {ι : Type u_2} (s : Finset ι) (m : ι → FRC.Dimensions.Dom κ) (k : ι → ℤ), ∏ j ∈ s, (FRC.Dimensions.Uhom κ) (Multiplicative.ofAdd (m j)) ^ k j = (FRC.Dimensions.Uhom κ) (Multiplicative.ofAdd (∑ j ∈ s, k j • m j))) ∧ ∀ (κ : ℕ) (a b : FRC.Dimensions.Dom κ) {c : ZMod ((4 : ℕ) * κ + (1 : ℕ))}, c ≠ (0 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) → (AddMonoidAlgebra.single a c ∈ AddMonoidAlgebra.grade (ZMod ((4 : ℕ) * κ + (1 : ℕ))) b ↔ a = b) :=1212  And.intro @FRC.Dimensions.fibre_add (And.intro @FRC.Dimensions.coeff_sum_single (And.intro @FRC.Dimensions.monomial_units (@FRC.Dimensions.single_mem_grade_iff)))1213set_option linter.defProp false in1214/-- 10:C5 (p10015) — Window covariance: on a bounded window $|r|,|s|\le H<2\kap$ in the flag-free sector the labels are covariant under every admissible reframing; the bound is sharp (the label $(0,\pi)$ is pushforward-invariant yet non-neutral); the naive character is ill-defined on the modular projection and the would-be temporal character fails composition ($5^{2}\equiv1$ in $\Z_{12}^{\times}$); on the realized lattice the invariant labels are exactly $\{0,2\kap\}$; the $\sigma$-twisted action is equivariant by full sweep on $\p=13$ and $229$; the flagged label $(0,0;1)$ moves under $\eps=-1$. -/1215def p10015 := And.intro @FRC.Dimensions.dilation_character (And.intro @FRC.Dimensions.invariant_iff (And.intro @FRC.Dimensions.quarter_turn_law (And.intro @FRC.Dimensions.sigma_twist (And.intro @FRC.Dimensions.half_period_invariant_not_neutral (And.intro @FRC.Dimensions.flag_moves (@FRC.Dimensions.witnesses13))))))1216/-- 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. -/1217theorem p10016 : ∀ (κ : ℕ), ((4 : ℕ) * κ + (1 : ℕ)) • (FRC.Dimensions.L κ + κ • FRC.Dimensions.T κ) = FRC.Dimensions.flag κ :=1218  @FRC.Dimensions.meridian_transport1219/-- 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$. -/1220theorem p10017 : (∀ (κ : ℕ) (a : FRC.Dimensions.Dom κ), (FRC.Dimensions.deltaS κ) ((FRC.Dimensions.deltaS κ) a) = a) ∧ (∀ (κ : ℕ) [NeZero κ], FRC.Dimensions.L κ ≠ -FRC.Dimensions.L κ ∧ FRC.Dimensions.T κ ≠ -FRC.Dimensions.T κ ∧ FRC.Dimensions.L κ ≠ FRC.Dimensions.T κ ∧ FRC.Dimensions.L κ ≠ -FRC.Dimensions.T κ ∧ -FRC.Dimensions.L κ ≠ FRC.Dimensions.T κ ∧ -FRC.Dimensions.L κ ≠ -FRC.Dimensions.T κ) ∧ (∀ (κ : ℕ) (a : FRC.Dimensions.Dom κ), 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 κ :=1221  And.intro @FRC.Dimensions.deltaS_involutive (And.intro @FRC.Dimensions.four_domains (And.intro @FRC.Dimensions.deltaC_involutive (@FRC.Dimensions.deltaC_generators)))1222set_option linter.defProp false in1223/-- 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. -/1224def p10018 := And.intro @FRC.Dimensions.order_four_iff (And.intro @FRC.Dimensions.unique_order_four_subgroup (And.intro @FRC.Dimensions.no_flag_of_space (And.intro @FRC.Dimensions.order_two_iff (And.intro @FRC.Dimensions.meridian_transport (@FRC.Dimensions.quarter_turn_law)))))1225set_option linter.defProp false in1226/-- 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$. -/1227def p10019 := And.intro @FRC.Dimensions.operator_four_cycle (And.intro @FRC.Dimensions.record_injective (And.intro @FRC.Dimensions.record_range (And.intro @FRC.Dimensions.record_mem_parity_iff (@FRC.Dimensions.crossing_order_four))))1228/-- 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$. -/1229theorem p10022 : And (∀ (κ : Nat), And (@Eq (FRC.Dimensions.Dom κ) (FRC.Dimensions.energy κ) (@Prod.mk (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@OfNat.ofNat (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (nat_lit 0) (@Zero.toOfNat0 (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@MulZeroClass.toZero (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instMulZeroClassOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))))) (@HSub.hSub (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@instHSub (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@SubNegMonoid.toSub (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroup.toSubNegMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddGroup (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))) (@Nat.cast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toNatCast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))) κ) (@OfNat.ofNat (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (nat_lit 1) (@One.toOfNat1 (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))))))))) (And (@Eq (FRC.Dimensions.Dom κ) (FRC.Dimensions.mom κ) (@Prod.mk (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Neg.neg (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@NegZeroClass.toNeg (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@SubNegZeroMonoid.toNegZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@SubtractionMonoid.toSubNegZeroMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@SubtractionCommMonoid.toSubtractionMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddCommGroup.toDivisionAddCommMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddCommGroup (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))))) (@OfNat.ofNat (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (nat_lit 1) (@One.toOfNat1 (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddMonoidWithOne.toOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))))) (@Nat.cast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toNatCast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))) κ))) (And (@Eq (FRC.Dimensions.Dom κ) (@HAdd.hAdd (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (@instHAdd (FRC.Dimensions.Dom κ) (@Prod.instAdd (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Distrib.toAdd (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instDistribOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))) (@Distrib.toAdd (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@instDistribOfSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommSemiring.toSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toCommSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))) (FRC.Dimensions.energy κ) (FRC.Dimensions.T κ)) (FRC.Dimensions.flag κ)) (And (@Eq (FRC.Dimensions.Dom κ) (@HSub.hSub (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (@instHSub (FRC.Dimensions.Dom κ) (@Prod.instSub (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@SubNegMonoid.toSub (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroup.toSubNegMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddGroup (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))) (@SubNegMonoid.toSub (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroup.toSubNegMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddGroup (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))))))) (@HAdd.hAdd (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (@instHAdd (FRC.Dimensions.Dom κ) (@Prod.instAdd (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Distrib.toAdd (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instDistribOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))) (@Distrib.toAdd (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@instDistribOfSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommSemiring.toSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toCommSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))) (FRC.Dimensions.energy κ) (FRC.Dimensions.T κ)) (FRC.Dimensions.flag κ)) (@OfNat.ofNat (FRC.Dimensions.Dom κ) (nat_lit 0) (@Zero.toOfNat0 (FRC.Dimensions.Dom κ) (@Prod.instZero (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@MulZeroClass.toZero (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instMulZeroClassOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))) (@MulZeroClass.toZero (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@instMulZeroClassOfSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommSemiring.toSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toCommSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))))) (@Eq (FRC.Dimensions.Dom κ) (@HSub.hSub (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (@instHSub (FRC.Dimensions.Dom κ) (@Prod.instSub (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@SubNegMonoid.toSub (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroup.toSubNegMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddGroup (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))) (@SubNegMonoid.toSub (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroup.toSubNegMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddGroup (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))))))) (@HAdd.hAdd (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (FRC.Dimensions.Dom κ) (@instHAdd (FRC.Dimensions.Dom κ) (@Prod.instAdd (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Distrib.toAdd (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instDistribOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))) (@Distrib.toAdd (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@instDistribOfSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommSemiring.toSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toCommSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))) (FRC.Dimensions.mom κ) (FRC.Dimensions.L κ)) (FRC.Dimensions.flag κ)) (@OfNat.ofNat (FRC.Dimensions.Dom κ) (nat_lit 0) (@Zero.toOfNat0 (FRC.Dimensions.Dom κ) (@Prod.instZero (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@MulZeroClass.toZero (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instMulZeroClassOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))) (@MulZeroClass.toZero (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@instMulZeroClassOfSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommSemiring.toSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toCommSemiring (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))))))))) (∀ (κ H : Nat), @LT.lt Nat instLTNat H κ → ∀ (r s : Int), @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup s) (@Nat.cast Int instNatCastInt H) → And (@Ne (Prod (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))) (@Prod.mk (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Int.cast (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toIntCast (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))) r) (@Int.cast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toIntCast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))) s)) (FRC.Dimensions.flag κ)) (@Eq (Prod (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))) (@Prod.mk (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@OfNat.ofNat (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (nat_lit 0) (@Zero.toOfNat0 (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@MulZeroClass.toZero (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@instMulZeroClassOfSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommSemiring.toSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toCommSemiring (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))))))))) (@Int.cast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toIntCast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))) (@Nat.cast Int instNatCastInt κ))) (FRC.Dimensions.flag κ))) :=1230  And.intro @FRC.Dimensions.flagged_readings (@FRC.Dimensions.flag_inaccessible)1231/-- 10:E2 (p10025) — One crossing, one action, and pairing closure: $\lP\pP=\tPl\EP=\hbar$ (the two faces of $c$ and $\hbar$ differ by the single relation $\ell p=tE$); the cross-domain relations reduce to the two generators $c$, $\hbar$, the mixed products their monomials, $|k_B|=\hbar/c$ derived; the relation lattice over $\{\lP,\tPl,\hbar\}$ has rank two and $k_B$, $\lP\EP$ add nothing; $4-1=3$ free scales in bijection with $\{c,\hbar,G\}$, the classical arity derived. -/1232theorem p10025 : (∀ {K : Type u_1} [Field K] (l t hbar : K), l ≠ (0 : K) → t ≠ (0 : K) → l * (hbar / l) = hbar ∧ t * (hbar / t) = hbar) ∧ (∀ {K : Type u_2} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → (l * p = t * E ↔ p = l * p / l ∧ E = l * p / t)) ∧ (∀ {K : Type u_3} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → p ≠ (0 : K) → l * p = t * E → l / t = E / p ∧ p * t = l * p / (l / t) ∧ l * E = l * p * (l / t)) ∧ (∀ {K : Type u_4} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → p ≠ (0 : K) → l * p = t * E → l * p * (l / t) / (p / (l / t)) ^ (2 : ℕ) = l ^ (2 : ℕ) * (l / t) ^ (3 : ℕ) / (l * p) ∧ l ^ (2 : ℕ) = l * p * (l / t) / (p / (l / t)) ^ (2 : ℕ) * (l * p) / (l / t) ^ (3 : ℕ) ∧ t = l / (l / t) ∧ p = l * p / l ∧ E = l * p * (l / t) / l) ∧ !![(1 : ℤ), (-1 : ℤ), (0 : ℤ); (0 : ℤ), (0 : ℤ), (1 : ℤ); (5 : ℤ), (-3 : ℤ), (-1 : ℤ)].det = (-2 : ℤ) ∧ (∀ (c hbar G : ℝ), (0 : ℝ) < c → (0 : ℝ) < hbar → (0 : ℝ) < G → ∃! l, (0 : ℝ) < l ∧ l ^ (2 : ℕ) = G * hbar / c ^ (3 : ℕ)) ∧ ![(1 : ℤ), (-1 : ℤ), (0 : ℤ), (0 : ℤ)] - ![(0 : ℤ), (0 : ℤ), (-1 : ℤ), (1 : ℤ)] = ![(1 : ℤ), (-1 : ℤ), (1 : ℤ), (-1 : ℤ)] ∧ ![(1 : ℤ), (0 : ℤ), (1 : ℤ), (0 : ℤ)] - ![(0 : ℤ), (1 : ℤ), (0 : ℤ), (1 : ℤ)] = ![(1 : ℤ), (-1 : ℤ), (1 : ℤ), (-1 : ℤ)] ∧ ![(1 : ℤ), (0 : ℤ), (0 : ℤ), (1 : ℤ)] = ![(0 : ℤ), (1 : ℤ), (0 : ℤ), (1 : ℤ)] + ![(1 : ℤ), (-1 : ℤ), (0 : ℤ), (0 : ℤ)] ∧ ![(0 : ℤ), (1 : ℤ), (1 : ℤ), (0 : ℤ)] = ![(0 : ℤ), (1 : ℤ), (0 : ℤ), (1 : ℤ)] - ![(0 : ℤ), (0 : ℤ), (-1 : ℤ), (1 : ℤ)] :=1233  And.intro @FRC.Dimensions.action_identity (And.intro @FRC.Dimensions.quartet_param (And.intro @FRC.Dimensions.pairing_closure (And.intro @FRC.Dimensions.normalisation (And.intro @FRC.Dimensions.index_two (And.intro @FRC.Dimensions.scale_from_constants (@FRC.Dimensions.exponent_faces))))))1234/-- 10:E3 (p10026) — The cancellation identity $|k_B|c=\hbar$ at the unit face, $(\pP\tPl)(\lP/\tPl)=\lP\pP$; mass derived, $m_P=\pP/c=\EP/c^{2}$; the temperature horizon $\Theta_P=\EP/|k_B|$; the flag positions $(0,0,1,1)$ and the closure of every quartet relation on the flag component; no $\hbar$ of space and time. -/1235theorem p10026 : (∀ {K : Type u_1} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → p ≠ (0 : K) → l * p = t * E → p * t * (l / t) = l * p ∧ p / (l / t) = E / (l / t) ^ (2 : ℕ) ∧ E / (p * t) = E * (l / t) / (l * p)) ∧ FRC.Dimensions.spaceL.2.2 = (0 : ℤ) ∧ FRC.Dimensions.timeL.2.2 = (0 : ℤ) ∧ FRC.Dimensions.momL.2.2 = (1 : ℤ) ∧ FRC.Dimensions.energyL.2.2 = (1 : ℤ) ∧ FRC.Dimensions.spaceL + FRC.Dimensions.momL = FRC.Dimensions.flagL ∧ (FRC.Dimensions.spaceL - FRC.Dimensions.timeL).2.2 = (0 : ℤ) ∧ (FRC.Dimensions.energyL - FRC.Dimensions.momL).2.2 = (0 : ℤ) ∧ FRC.Dimensions.momL + FRC.Dimensions.timeL = FRC.Dimensions.kBL ∧ (2 : ℤ) • FRC.Dimensions.spaceL + (3 : ℤ) • (FRC.Dimensions.spaceL - FRC.Dimensions.timeL) - (FRC.Dimensions.spaceL + FRC.Dimensions.momL) = FRC.Dimensions.gravL ∧ FRC.Dimensions.gravL.2.2 = (-1 : ℤ) :=1236  And.intro @FRC.Dimensions.cancellation (@FRC.Dimensions.quartet_flags)1237/-- 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. -/1238theorem p10027 : (∀ {K : Type u_1} [Field K] (S : ℕ), ↑((4 : ℕ) * S + (1 : ℕ)) = (0 : K) → (2 : K) ≠ (0 : K) → ∀ (x : K), (2 : K) * x + (1 : K) = (0 : K) ↔ x = ↑((2 : ℕ) * S)) ∧ (∀ {K : Type u_2} [Field K] (a x : K), x ^ (2 : ℕ) = a → x ≠ (0 : K) → (2 : K) ≠ (0 : K) → (∀ (y : K), y ^ (2 : ℕ) = a ↔ y = x ∨ y = -x) ∧ -x ≠ x) ∧ (∀ {K : Type u_3} [Field K] (k c h : K), k ^ (2 : ℕ) = (-2 : K) → (2 : K) * c ^ (2 : ℕ) = (1 : K) → h ^ (2 : ℕ) = (-1 : K) → (k * c) ^ (2 : ℕ) = (-1 : K) ∧ (k * c = h ∨ k * c = -h)) ∧ (∀ (S : ℕ) [hΩ : Fact (Nat.Prime ((4 : ℕ) * S + (1 : ℕ)))], Even S → IsSquare (-1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ IsSquare (2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ IsSquare (2 : ZMod ((4 : ℕ) * S + (1 : ℕ)))⁻¹ ∧ IsSquare (-2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) ∧ (2 : ZMod ((4 : ℕ) * S + (1 : ℕ))) * ↑((2 : ℕ) * S) + (1 : ZMod ((4 : ℕ) * S + (1 : ℕ))) = (0 : ZMod ((4 : ℕ) * S + (1 : ℕ)))) ∧ (∀ {K : Type u_4} [Field K] (S : ℕ), ↑((4 : ℕ) * S + (1 : ℕ)) = (0 : K) → ∀ (hbar : K), ↑((2 : ℕ) * ((2 : ℕ) * S)) * hbar = -hbar) ∧ (Nat.Prime (233 : ℕ) ∧ (233 : ℕ) = (4 : ℕ) * (58 : ℕ) + (1 : ℕ) ∧ (58 : ℕ) % (2 : ℕ) = (0 : ℕ) ∧ (58 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ (2 : ZMod (233 : ℕ)) * (116 : ZMod (233 : ℕ)) + (1 : ZMod (233 : ℕ)) = (0 : ZMod (233 : ℕ)) ∧ (89 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (233 : ℕ)) ∧ (124 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (-2 : ZMod (233 : ℕ)) ∧ (2 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (233 : ℕ)) ∧ (124 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) = (-89 : ZMod (233 : ℕ)) ∧ (144 : ZMod (233 : ℕ)) = (-89 : ZMod (233 : ℕ)) ∧ (116 : ZMod (233 : ℕ)) = -(159 : ZMod (233 : ℕ)) ^ (2 : ℕ) ∧ (4 : ZMod (233 : ℕ)) * (116 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (233 : ℕ)) ∧ (89 : ZMod (233 : ℕ)) ^ (4 : ℕ) = (1 : ZMod (233 : ℕ)) ∧ (89 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) = (124 : ZMod (233 : ℕ)) * (116 : ZMod (233 : ℕ)) ∧ (109 : ZMod (233 : ℕ)) = (-124 : ZMod (233 : ℕ)) ∧ (109 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) ≠ (-89 : ZMod (233 : ℕ))) ∧ Nat.Prime (2408561 : ℕ) ∧ (2408561 : ℕ) = (4 : ℕ) * (602140 : ℕ) + (1 : ℕ) ∧ (602140 : ℕ) % (2 : ℕ) = (0 : ℕ) ∧ (602140 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ (2 : ZMod (2408561 : ℕ)) * (1204280 : ZMod (2408561 : ℕ)) + (1 : ZMod (2408561 : ℕ)) = (0 : ZMod (2408561 : ℕ)) ∧ (18688 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (2408561 : ℕ)) ∧ (1880160 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (-2 : ZMod (2408561 : ℕ)) ∧ (2 : ZMod (2408561 : ℕ)) * (171106 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (2408561 : ℕ)) ∧ (1880160 : ZMod (2408561 : ℕ)) * (171106 : ZMod (2408561 : ℕ)) = (-18688 : ZMod (2408561 : ℕ)) ∧ (2389873 : ZMod (2408561 : ℕ)) = (-18688 : ZMod (2408561 : ℕ)) ∧ (1204280 : ZMod (2408561 : ℕ)) = -(171106 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) ∧ (4 : ZMod (2408561 : ℕ)) * (1204280 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (2408561 : ℕ)) ∧ (18688 : ZMod (2408561 : ℕ)) ^ (4 : ℕ) = (1 : ZMod (2408561 : ℕ)) ∧ (18688 : ZMod (2408561 : ℕ)) * (171106 : ZMod (2408561 : ℕ)) = (1880160 : ZMod (2408561 : ℕ)) * (1204280 : ZMod (2408561 : ℕ)) :=1239  And.intro @FRC.Dimensions.G_unique (And.intro @FRC.Dimensions.root_pair (And.intro @FRC.Dimensions.linkage (And.intro @FRC.Dimensions.residues_exist (And.intro @FRC.Dimensions.h_form (And.intro @FRC.Dimensions.carrier233 (@FRC.Dimensions.carrierLab))))))1240/-- 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. -/1241theorem p10028 : (∀ {K : Type u_1} [Field K] (G c h k : K), (2 : K) ≠ (0 : K) → (2 : K) * G + (1 : K) = (0 : K) → (2 : K) * c ^ (2 : ℕ) = (1 : K) → h ^ (2 : ℕ) = (-1 : K) → k ^ (2 : ℕ) = (-2 : K) → G = -c ^ (2 : ℕ) ∧ G ^ (2 : ℕ) = (4 : K)⁻¹ ∧ h ^ (4 : ℕ) = (1 : K) ∧ (k * c) ^ (2 : ℕ) = (-1 : K) ∧ (h * c * G⁻¹) ^ (2 : ℕ) = (-2 : K) ∧ (h * c * G⁻¹ = k ∨ h * c * G⁻¹ = -k)) ∧ (∀ {K : Type u_2} [Field K] (c h k sc sh sk : K), h ≠ (0 : K) → k * c = -h → sc = (1 : K) ∨ sc = (-1 : K) → sh = (1 : K) ∨ sh = (-1 : K) → sk = (1 : K) ∨ sk = (-1 : K) → (sk * k * (sc * c) = -(sh * h) ↔ sh = sc * sk) ∧ (sc * c) ^ (2 : ℕ) = c ^ (2 : ℕ) ∧ (sh * h) ^ (2 : ℕ) = h ^ (2 : ℕ) ∧ (sk * k) ^ (2 : ℕ) = k ^ (2 : ℕ)) ∧ (Nat.Prime (233 : ℕ) ∧ (233 : ℕ) = (4 : ℕ) * (58 : ℕ) + (1 : ℕ) ∧ (58 : ℕ) % (2 : ℕ) = (0 : ℕ) ∧ (58 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ (2 : ZMod (233 : ℕ)) * (116 : ZMod (233 : ℕ)) + (1 : ZMod (233 : ℕ)) = (0 : ZMod (233 : ℕ)) ∧ (89 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (233 : ℕ)) ∧ (124 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (-2 : ZMod (233 : ℕ)) ∧ (2 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (233 : ℕ)) ∧ (124 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) = (-89 : ZMod (233 : ℕ)) ∧ (144 : ZMod (233 : ℕ)) = (-89 : ZMod (233 : ℕ)) ∧ (116 : ZMod (233 : ℕ)) = -(159 : ZMod (233 : ℕ)) ^ (2 : ℕ) ∧ (4 : ZMod (233 : ℕ)) * (116 : ZMod (233 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (233 : ℕ)) ∧ (89 : ZMod (233 : ℕ)) ^ (4 : ℕ) = (1 : ZMod (233 : ℕ)) ∧ (89 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) = (124 : ZMod (233 : ℕ)) * (116 : ZMod (233 : ℕ)) ∧ (109 : ZMod (233 : ℕ)) = (-124 : ZMod (233 : ℕ)) ∧ (109 : ZMod (233 : ℕ)) * (159 : ZMod (233 : ℕ)) ≠ (-89 : ZMod (233 : ℕ))) ∧ Nat.Prime (2408561 : ℕ) ∧ (2408561 : ℕ) = (4 : ℕ) * (602140 : ℕ) + (1 : ℕ) ∧ (602140 : ℕ) % (2 : ℕ) = (0 : ℕ) ∧ (602140 : ℕ) % (3 : ℕ) = (1 : ℕ) ∧ (2 : ZMod (2408561 : ℕ)) * (1204280 : ZMod (2408561 : ℕ)) + (1 : ZMod (2408561 : ℕ)) = (0 : ZMod (2408561 : ℕ)) ∧ (18688 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (-1 : ZMod (2408561 : ℕ)) ∧ (1880160 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (-2 : ZMod (2408561 : ℕ)) ∧ (2 : ZMod (2408561 : ℕ)) * (171106 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (2408561 : ℕ)) ∧ (1880160 : ZMod (2408561 : ℕ)) * (171106 : ZMod (2408561 : ℕ)) = (-18688 : ZMod (2408561 : ℕ)) ∧ (2389873 : ZMod (2408561 : ℕ)) = (-18688 : ZMod (2408561 : ℕ)) ∧ (1204280 : ZMod (2408561 : ℕ)) = -(171106 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) ∧ (4 : ZMod (2408561 : ℕ)) * (1204280 : ZMod (2408561 : ℕ)) ^ (2 : ℕ) = (1 : ZMod (2408561 : ℕ)) ∧ (18688 : ZMod (2408561 : ℕ)) ^ (4 : ℕ) = (1 : ZMod (2408561 : ℕ)) ∧ (18688 : ZMod (2408561 : ℕ)) * (171106 : ZMod (2408561 : ℕ)) = (1880160 : ZMod (2408561 : ℕ)) * (1204280 : ZMod (2408561 : ℕ)) :=1242  And.intro @FRC.Dimensions.pair_consequences (And.intro @FRC.Dimensions.sign_assignments (And.intro @FRC.Dimensions.carrier233 (@FRC.Dimensions.carrierLab)))1243/-- 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. -/1244theorem p10034 : (FRC.Dimensions.massL = FRC.Dimensions.energyL - (2 : ℤ) • FRC.Dimensions.speedL ∧ FRC.Dimensions.massL = ((-2 : ℤ), (1 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.accelL = FRC.Dimensions.speedL - FRC.Dimensions.timeL ∧ FRC.Dimensions.forceL = FRC.Dimensions.massL + FRC.Dimensions.accelL ∧ FRC.Dimensions.forceL = ((-1 : ℤ), (-1 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.momL = FRC.Dimensions.massL + FRC.Dimensions.speedL ∧ FRC.Dimensions.momL = FRC.Dimensions.flagL - FRC.Dimensions.spaceL ∧ FRC.Dimensions.actionL = FRC.Dimensions.energyL + FRC.Dimensions.timeL ∧ FRC.Dimensions.actionL = FRC.Dimensions.flagL ∧ FRC.Dimensions.powerL = FRC.Dimensions.energyL - FRC.Dimensions.timeL ∧ FRC.Dimensions.powerL = ((0 : ℤ), (-2 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.pressureL = FRC.Dimensions.forceL - (2 : ℤ) • FRC.Dimensions.spaceL ∧ FRC.Dimensions.pressureL = ((-3 : ℤ), (-1 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.gravL = FRC.Dimensions.forceL + (2 : ℤ) • FRC.Dimensions.spaceL - (2 : ℤ) • FRC.Dimensions.massL ∧ FRC.Dimensions.gravL = ((5 : ℤ), (-3 : ℤ), (-1 : ℤ)) ∧ FRC.Dimensions.gravL = FRC.Dimensions.flagL + FRC.Dimensions.speedL - (2 : ℤ) • FRC.Dimensions.massL) ∧ FRC.Dimensions.gravL + FRC.Dimensions.flagL - (3 : ℤ) • FRC.Dimensions.speedL = ((2 : ℤ), (0 : ℤ), (0 : ℤ)) ∧ FRC.Dimensions.gravL + FRC.Dimensions.massL - (2 : ℤ) • FRC.Dimensions.speedL = ((1 : ℤ), (0 : ℤ), (0 : ℤ)) ∧ FRC.Dimensions.gravL + FRC.Dimensions.massL - (3 : ℤ) • FRC.Dimensions.speedL = ((0 : ℤ), (1 : ℤ), (0 : ℤ)) ∧ FRC.Dimensions.gravL + (FRC.Dimensions.massL - (3 : ℤ) • FRC.Dimensions.spaceL) = ((0 : ℤ), (-2 : ℤ), (0 : ℤ)) ∧ FRC.Dimensions.gravL - (4 : ℤ) • FRC.Dimensions.speedL + (FRC.Dimensions.energyL - (3 : ℤ) • FRC.Dimensions.spaceL) = ((-2 : ℤ), (0 : ℤ), (0 : ℤ)) ∧ FRC.Dimensions.massL + FRC.Dimensions.speedL - FRC.Dimensions.flagL = ((-1 : ℤ), (0 : ℤ), (0 : ℤ)) :=1245  And.intro @FRC.Dimensions.mechanical_domains (@FRC.Dimensions.geometric_conversions)1246/-- 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. -/1247theorem p10035 : FRC.Dimensions.thetaL = FRC.Dimensions.energyL - FRC.Dimensions.kBL ∧ FRC.Dimensions.thetaL = FRC.Dimensions.accelL ∧ FRC.Dimensions.thetaL.2.2 = (0 : ℤ) ∧ FRC.Dimensions.flagL + FRC.Dimensions.accelL - FRC.Dimensions.speedL - FRC.Dimensions.kBL = FRC.Dimensions.thetaL :=1248  @FRC.Dimensions.temperature_domain1249/-- 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. -/1250theorem p10036 : (∀ (x y : FRC.Dimensions.Lab), x.2.2 = y.2.2 → (x - y).2.2 = (0 : ℤ)) ∧ FRC.Dimensions.energyL + FRC.Dimensions.timeL - FRC.Dimensions.flagL = (0 : FRC.Dimensions.Lab) ∧ FRC.Dimensions.gravL + FRC.Dimensions.massL - (3 : ℤ) • FRC.Dimensions.spaceL = ((0 : ℤ), (-2 : ℤ), (0 : ℤ)) ∧ (FRC.Dimensions.gravL + FRC.Dimensions.massL - (3 : ℤ) • FRC.Dimensions.spaceL).2.2 = (0 : ℤ) ∧ FRC.Dimensions.forceL - FRC.Dimensions.accelL = FRC.Dimensions.massL ∧ (FRC.Dimensions.forceL - FRC.Dimensions.accelL).2.2 = (1 : ℤ) ∧ FRC.Dimensions.forceL.2.2 ≠ FRC.Dimensions.accelL.2.2 :=1251  And.intro @FRC.Dimensions.equal_crossing_flag_free (@FRC.Dimensions.comparison_examples)1252/-- 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. -/1253theorem p10037 : And (∀ (κ H : Nat), @LT.lt Nat instLTNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) H) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) → ∀ (r r' s s' : Int), @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup r) (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup r') (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup s) (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup s') (@Nat.cast Int instNatCastInt H) → @Eq (Prod (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))) (@Prod.mk (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Int.cast (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toIntCast (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))) r) (@Int.cast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toIntCast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))) s)) (@Prod.mk (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Int.cast (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toIntCast (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))) r') (@Int.cast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toIntCast (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ))))) s')) → And (@Eq Int r r') (@Eq Int s s')) (And (∀ (u a b u' a' b' : Int), @Eq FRC.Dimensions.Lab (FRC.Dimensions.embed u a b) (FRC.Dimensions.embed u' a' b') → And (@Eq Int u u') (And (@Eq Int a a') (@Eq Int b b'))) (∀ (κ H : Nat) [@NeZero Nat (@MulZeroClass.toZero Nat Nat.instMulZeroClass) κ], @LT.lt Nat instLTNat (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) H) κ → ∀ (r r' s s' j j' : Int), @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup r) (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup r') (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup s) (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup s') (@Nat.cast Int instNatCastInt H) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup j) (@OfNat.ofNat Int (nat_lit 1) (@instOfNat (nat_lit 1))) → @LE.le Int Int.instLEInt (@abs Int instLatticeInt Int.instAddGroup j') (@OfNat.ofNat Int (nat_lit 1) (@instOfNat (nat_lit 1))) → @Eq (FRC.Dimensions.Dom κ) (@DFunLike.coe (@AddMonoidHom FRC.Dimensions.Lab (FRC.Dimensions.Dom κ) (@AddZeroClass.toAddZero FRC.Dimensions.Lab (@Prod.instAddZeroClass Int (Prod Int Int) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@Prod.instAddZeroClass Int Int (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid)))) (@AddZeroClass.toAddZero (FRC.Dimensions.Dom κ) (@Prod.instAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoid.toAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddMonoidWithOne.toAddMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))) (@AddMonoid.toAddZeroClass (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toAddMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))))) FRC.Dimensions.Lab (fun x => FRC.Dimensions.Dom κ) (@AddMonoidHom.instFunLike FRC.Dimensions.Lab (FRC.Dimensions.Dom κ) (@AddZeroClass.toAddZero FRC.Dimensions.Lab (@Prod.instAddZeroClass Int (Prod Int Int) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@Prod.instAddZeroClass Int Int (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid)))) (@AddZeroClass.toAddZero (FRC.Dimensions.Dom κ) (@Prod.instAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoid.toAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddMonoidWithOne.toAddMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))) (@AddMonoid.toAddZeroClass (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toAddMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))))) (FRC.Dimensions.realize κ) (@Prod.mk Int (Prod Int Int) r (@Prod.mk Int Int s j))) (@DFunLike.coe (@AddMonoidHom FRC.Dimensions.Lab (FRC.Dimensions.Dom κ) (@AddZeroClass.toAddZero FRC.Dimensions.Lab (@Prod.instAddZeroClass Int (Prod Int Int) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@Prod.instAddZeroClass Int Int (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid)))) (@AddZeroClass.toAddZero (FRC.Dimensions.Dom κ) (@Prod.instAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoid.toAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddMonoidWithOne.toAddMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))) (@AddMonoid.toAddZeroClass (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toAddMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))))) FRC.Dimensions.Lab (fun x => FRC.Dimensions.Dom κ) (@AddMonoidHom.instFunLike FRC.Dimensions.Lab (FRC.Dimensions.Dom κ) (@AddZeroClass.toAddZero FRC.Dimensions.Lab (@Prod.instAddZeroClass Int (Prod Int Int) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@Prod.instAddZeroClass Int Int (@AddMonoid.toAddZeroClass Int Int.instAddMonoid) (@AddMonoid.toAddZeroClass Int Int.instAddMonoid)))) (@AddZeroClass.toAddZero (FRC.Dimensions.Dom κ) (@Prod.instAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoid.toAddZeroClass (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddMonoidWithOne.toAddMonoid (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@Ring.toAddGroupWithOne (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (@CommRing.toRing (ZMod (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))) (ZMod.commRing (@HAdd.hAdd Nat Nat Nat (@instHAdd Nat instAddNat) (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ) (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))))))) (@AddMonoid.toAddZeroClass (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddMonoidWithOne.toAddMonoid (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@AddGroupWithOne.toAddMonoidWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@Ring.toAddGroupWithOne (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (@CommRing.toRing (ZMod (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)) (ZMod.commRing (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 4) (instOfNatNat (nat_lit 4))) κ)))))))))) (FRC.Dimensions.realize κ) (@Prod.mk Int (Prod Int Int) r' (@Prod.mk Int Int s' j'))) → And (@Eq Int r r') (And (@Eq Int s s') (@Eq Int j j')))) :=1254  And.intro @FRC.Dimensions.local_recovery (And.intro @FRC.Dimensions.embed_injective (@FRC.Dimensions.realize_faithful))1255/-- 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$. -/1256theorem p10038 : ∀ (κ S : ℕ), ((16 : ℕ) * κ < κ ^ (2 : ℕ) ↔ (16 : ℕ) < κ) ∧ ((0 : ℕ) < κ → κ / (2 : ℕ) < κ ∧ κ < (2 : ℕ) * κ) ∧ ¬(16 : ℕ) * (3 : ℕ) < (3 : ℕ) ^ (2 : ℕ) ∧ ((2 : ℕ) * (2 : ℕ) * κ = (4 : ℕ) * κ ∧ (4 : ℕ) * κ = (4 : ℕ) * κ + (1 : ℕ) - (1 : ℕ)) ∧ (4 : ℕ) * S = (4 : ℕ) * S + (1 : ℕ) - (1 : ℕ) :=1257  @FRC.Dimensions.window_ladder1258set_option linter.defProp false in1259/-- 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. -/1260def p10039 := And.intro @FRC.Dimensions.examples13 (And.intro @FRC.Dimensions.recovery13 (@FRC.Dimensions.energy_momentum))1261/-- 10:G4 (p10046) — Buckingham's count: on the integer lift the neutral monomials of $N$ quantities are the kernel of their $N\times3$ label matrix, $N-\operatorname{rank}$ independent dimensionless products with rank $\le3$, the classical count for quantities whose classical dimensions lie in $M$-$L$-$T$ and the derived-$k_B$ count for thermal ones; on the window $2H<\kap$, $|j|\le1$ lifted and realized neutrality coincide; the pendulum $(T,\ell,g,m)$: rank $3$, one product. -/1262theorem p10046 : (∀ (κ : ℕ) {ι : Type u_1} (s : Finset ι) (m : ι → FRC.Dimensions.Dom κ) (k : ι → ℤ), ∏ j ∈ s, (FRC.Dimensions.Uhom κ) (Multiplicative.ofAdd (m j)) ^ k j = (FRC.Dimensions.Uhom κ) (Multiplicative.ofAdd (∑ j ∈ s, k j • m j))) ∧ (∀ (u a b u' a' b' : ℤ), FRC.Dimensions.embed u a b = FRC.Dimensions.embed u' a' b' → u = u' ∧ a = a' ∧ b = b') ∧ (∀ (κ H : ℕ) [NeZero κ], (2 : ℕ) * H < κ → ∀ (r s j : ℤ), |r| ≤ ↑H → |s| ≤ ↑H → |j| ≤ (1 : ℤ) → ((FRC.Dimensions.realize κ) (r, s, j) = (0 : FRC.Dimensions.Dom κ) ↔ (r, s, j) = ((0 : ℤ), (0 : ℤ), (0 : ℤ)))) ∧ FRC.Dimensions.embed (0 : ℤ) (0 : ℤ) (1 : ℤ) = FRC.Dimensions.timeL ∧ FRC.Dimensions.embed (0 : ℤ) (1 : ℤ) (0 : ℤ) = FRC.Dimensions.spaceL ∧ FRC.Dimensions.embed (0 : ℤ) (1 : ℤ) (-2 : ℤ) = FRC.Dimensions.accelL ∧ FRC.Dimensions.embed (1 : ℤ) (0 : ℤ) (0 : ℤ) = FRC.Dimensions.massL ∧ (∀ (k₁ k₂ k₃ k₄ : ℤ), k₁ • FRC.Dimensions.timeL + k₂ • FRC.Dimensions.spaceL + k₃ • FRC.Dimensions.accelL + k₄ • FRC.Dimensions.massL = (0 : FRC.Dimensions.Lab) ↔ ∃ t, k₁ = (2 : ℤ) * t ∧ k₂ = -t ∧ k₃ = t ∧ k₄ = (0 : ℤ)) ∧ (2 : ℤ) • FRC.Dimensions.timeL - FRC.Dimensions.spaceL + FRC.Dimensions.accelL = (0 : FRC.Dimensions.Lab) ∧ !![FRC.Dimensions.spaceL.1, FRC.Dimensions.spaceL.2.1, FRC.Dimensions.spaceL.2.2; FRC.Dimensions.accelL.1, FRC.Dimensions.accelL.2.1, FRC.Dimensions.accelL.2.2; FRC.Dimensions.massL.1, FRC.Dimensions.massL.2.1, FRC.Dimensions.massL.2.2].det = (-2 : ℤ) :=1263  And.intro @FRC.Dimensions.monomial_units (And.intro @FRC.Dimensions.embed_injective (And.intro @FRC.Dimensions.window_neutrality (@FRC.Dimensions.pendulum_kernel)))1264/-- 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. -/1265theorem p10048 : (∀ {K : Type u_1} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → (l * p = t * E ↔ p = l * p / l ∧ E = l * p / t)) ∧ (∀ (c hbar G : ℝ), (0 : ℝ) < c → (0 : ℝ) < hbar → (0 : ℝ) < G → ∃! l, (0 : ℝ) < l ∧ l ^ (2 : ℕ) = G * hbar / c ^ (3 : ℕ)) ∧ (∀ {K : Type u_2} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → p ≠ (0 : K) → l * p = t * E → p * t * (l / t) = l * p ∧ p / (l / t) = E / (l / t) ^ (2 : ℕ) ∧ E / (p * t) = E * (l / t) / (l * p)) ∧ FRC.Dimensions.massL = FRC.Dimensions.energyL - (2 : ℤ) • FRC.Dimensions.speedL ∧ FRC.Dimensions.massL = ((-2 : ℤ), (1 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.accelL = FRC.Dimensions.speedL - FRC.Dimensions.timeL ∧ FRC.Dimensions.forceL = FRC.Dimensions.massL + FRC.Dimensions.accelL ∧ FRC.Dimensions.forceL = ((-1 : ℤ), (-1 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.momL = FRC.Dimensions.massL + FRC.Dimensions.speedL ∧ FRC.Dimensions.momL = FRC.Dimensions.flagL - FRC.Dimensions.spaceL ∧ FRC.Dimensions.actionL = FRC.Dimensions.energyL + FRC.Dimensions.timeL ∧ FRC.Dimensions.actionL = FRC.Dimensions.flagL ∧ FRC.Dimensions.powerL = FRC.Dimensions.energyL - FRC.Dimensions.timeL ∧ FRC.Dimensions.powerL = ((0 : ℤ), (-2 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.pressureL = FRC.Dimensions.forceL - (2 : ℤ) • FRC.Dimensions.spaceL ∧ FRC.Dimensions.pressureL = ((-3 : ℤ), (-1 : ℤ), (1 : ℤ)) ∧ FRC.Dimensions.gravL = FRC.Dimensions.forceL + (2 : ℤ) • FRC.Dimensions.spaceL - (2 : ℤ) • FRC.Dimensions.massL ∧ FRC.Dimensions.gravL = ((5 : ℤ), (-3 : ℤ), (-1 : ℤ)) ∧ FRC.Dimensions.gravL = FRC.Dimensions.flagL + FRC.Dimensions.speedL - (2 : ℤ) • FRC.Dimensions.massL :=1266  And.intro @FRC.Dimensions.quartet_param (And.intro @FRC.Dimensions.scale_from_constants (And.intro @FRC.Dimensions.cancellation (@FRC.Dimensions.mechanical_domains)))1267/-- 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. -/1268theorem p10049 : (∀ {K : Type u_1} [Field K] (l t p E : K), l ≠ (0 : K) → t ≠ (0 : K) → p ≠ (0 : K) → l * p = t * E → p * t * (l / t) = l * p ∧ p / (l / t) = E / (l / t) ^ (2 : ℕ) ∧ E / (p * t) = E * (l / t) / (l * p)) ∧ FRC.Dimensions.thetaL = FRC.Dimensions.energyL - FRC.Dimensions.kBL ∧ FRC.Dimensions.thetaL = FRC.Dimensions.accelL ∧ FRC.Dimensions.thetaL.2.2 = (0 : ℤ) ∧ FRC.Dimensions.flagL + FRC.Dimensions.accelL - FRC.Dimensions.speedL - FRC.Dimensions.kBL = FRC.Dimensions.thetaL :=1269  And.intro @FRC.Dimensions.cancellation (@FRC.Dimensions.temperature_domain)1270/-- 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. -/1271theorem p10050 : (∀ (κ : ℕ) [NeZero κ] [hp : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] (H : AddSubgroup (FRC.Dimensions.Dom κ)), Nat.card ↥H = (4 : ℕ) → H = AddSubgroup.zmultiples (FRC.Dimensions.flag κ)) ∧ (∀ (κ : ℕ) [hp : Fact (Nat.Prime ((4 : ℕ) * κ + (1 : ℕ)))] (r : ZMod ((4 : ℕ) * κ + (1 : ℕ))), (4 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) * r = (0 : ZMod ((4 : ℕ) * κ + (1 : ℕ))) → r = (0 : ZMod ((4 : ℕ) * κ + (1 : ℕ)))) ∧ ∀ {K : Type u_1} [Field K] (l t hbar : K), l ≠ (0 : K) → t ≠ (0 : K) → l * (hbar / l) = hbar ∧ t * (hbar / t) = hbar :=1272  And.intro @FRC.Dimensions.unique_order_four_subgroup (And.intro @FRC.Dimensions.no_flag_of_space (@FRC.Dimensions.action_identity))1273-- end ledger predicates12741275end FRC.Dimensions1276