The core module lean/FrcCore/Theme/Domain.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on no other module: 7 theorems (22 definitions): 7 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1/-!2# FrcCore.Theme.Domain — the unit-domain lattice: the torsion-free lift of the Subject's domain group (00:C12)34The Subject's quantity algebra is graded by the modular domain group `D_p = C_p × C_{p−1}` of the labels5`U_{r,s} = L^r T^s` (10-dimensions C1, C2): `L` attached to the additive meridian chart, `T` to the drive's phase chart,6and the flag `Iq = T^κ` of order four. This file is the lattice above it — exponent triples `(r, s, j)` of `L`, `T`7and the flag over the integers, the torsion-free shadow in which classical dimensional analysis lives — and the8domain identities the master's row C12 states: the temperature domain is acceleration, `[Θ] = [E][k_B]⁻¹ = L T⁻²`,9flag-free; the Unruh combination `ħ a/(c k_B)` closes on it; neither mass nor temperature is primitive, each a monomial10in the two generators and the flag; and the classical `M`-`L`-`T`-`Θ` exponents of the mechanical, gravitational and11thermal quantities (10:F2, F3) map to their domains under `M ↦ Iq L⁻² T`, `Θ ↦ L T⁻²`. Every statement is closed and12decided by the kernel. No axioms.13-/1415namespace FRC.Domain1617/-- An exponent triple `L^r T^s Iq^j` of the lift lattice. -/18
structure Lift where19 r : Int20 s : Int21 j : Int22deriving DecidableEq2324namespace Lift2526/-- The product of domains adds exponents. -/27def mul (a b : Lift) : Lift := ⟨a.r + b.r, a.s + b.s, a.j + b.j⟩28/-- The inverse domain. -/29def inv (a : Lift) : Lift := ⟨-a.r, -a.s, -a.j⟩30/-- The dimensionless domain. -/31def one : Lift := ⟨0, 0, 0⟩3233instance : Mul Lift := ⟨mul⟩34instance : Inv Lift := ⟨inv⟩35instance : OfNat Lift 1 := ⟨one⟩3637/-- The length generator `L` (10:C1). -/38def L : Lift := ⟨1, 0, 0⟩39/-- The time generator `T` (10:C1). -/40def T : Lift := ⟨0, 1, 0⟩41/-- The flag `Iq = T^κ` (10:C4), the third coordinate of the lift. -/42def flag : Lift := ⟨0, 0, 1⟩4344/-- `[v] = L T⁻¹` (10:F1). -/45def speed : Lift := L * T⁻¹46/-- `[a] = L T⁻²` (10:F2). -/47def accel : Lift := L * T⁻¹ * T⁻¹48/-- `[E] = Iq T⁻¹` (10:E, the energy face of the flag). -/49def energy : Lift := flag * T⁻¹50/-- `[ħ] = [E][T] = Iq`. -/51def hbar : Lift := energy * T52/-- `[k_B] = [ħ][c]⁻¹`: the Carrier linkage `k_B c = −ħ` (00:B7) read in domains, `Iq L⁻¹ T`. -/53def kB : Lift := hbar * speed⁻¹54/-- `[Θ] = [E][k_B]⁻¹` (10:F3). -/55def temp : Lift := energy * kB⁻¹56/-- `[m] = Iq L⁻² T` (10:F2), mass derived. -/57def mass : Lift := flag * L⁻¹ * L⁻¹ * T58/-- `[F] = [m][a]`. -/59def force : Lift := mass * accel60/-- `[p] = [m][v]`. -/61def momentum : Lift := mass * speed62/-- `[P] = [E][T]⁻¹`. -/63def power : Lift := energy * T⁻¹64/-- `[pressure] = [F][L]⁻²`. -/65def pressure : Lift := force * L⁻¹ * L⁻¹66/-- `[G] = [a][L]²[m]⁻¹`, from `a = G m / r²`. -/67def G : Lift := accel * L * L * mass⁻¹68/-- The Unruh combination `ħ a/(c k_B)`. -/69def unruh : Lift := hbar * accel * speed⁻¹ * kB⁻¹7071/-- The classical dictionary: the exponent vector `M^a L^b T^c Θ^d` of classical dimensional analysis, read in the72lift under `M ↦ Iq L⁻² T` (the mass primitive standing in for the flag) and `Θ ↦ L T⁻²`. -/73def classical (a b c d : Int) : Lift := ⟨-2 * a + b + d, a + c - 2 * d, a⟩7475/-- 00:C12, 10:F3, 7:A32 — the temperature domain is acceleration: `[Θ] = [E][k_B]⁻¹ = L T⁻² = [a]`, and `[k_B] = Iq L⁻¹ T`. -/76
theorem temp_eq_accel : temp = accel ∧ temp = ⟨1, -2, 0⟩ ∧ kB = ⟨-1, 1, 1⟩ := by decide7778/-- 00:C12, 7:A32 — flag-free: the flag exponent of the temperature domain is zero, while energy, `ħ` and `k_B` each carry79the flag once. -/80theorem temp_flag_free : temp.j = 0 ∧ energy.j = 1 ∧ hbar.j = 1 ∧ kB.j = 1 := by decide8182/-- 00:C12, 7:A32 — the Unruh combination `ħ a/(c k_B)` closes as a domain identity: it is the temperature domain, flag-free. -/83theorem unruh_closes : unruh = temp ∧ unruh.j = 0 := by decide8485/-- 00:C12, 7:A32 — neither mass nor temperature is primitive: each is a monomial in the two generators and the flag, and86the Planck temperature `Θ_P = E_P/|k_B|`, written out from the energy and the linkage `[k_B] = [ħ][c]⁻¹`, is the87acceleration domain, flag-free. -/88theorem not_primitive : mass = ⟨-2, 1, 1⟩ ∧ temp = L * T⁻¹ * T⁻¹ ∧89 energy * (hbar * speed⁻¹)⁻¹ = accel ∧ (energy * (hbar * speed⁻¹)⁻¹).j = 0 := by decide9091/-- 00:C12, 7:A32 — classical dimensional analysis recovered in exponents: the classical `M`-`L`-`T`-`Θ` exponents of the92mechanical, gravitational and thermal quantities (10:F2, F3) map to their domains under the dictionary. -/93theorem classical_exponents :94 classical 1 0 0 0 = mass ∧ classical 0 1 (-1) 0 = speed ∧ classical 0 1 (-2) 0 = accel ∧95 classical 1 2 (-2) 0 = energy ∧ classical 1 2 (-1) 0 = hbar ∧ classical 1 1 (-2) 0 = force ∧96 classical 1 1 (-1) 0 = momentum ∧ classical 1 2 (-3) 0 = power ∧ classical 1 (-1) (-2) 0 = pressure ∧97 classical (-1) 3 (-2) 0 = G ∧ classical 1 2 (-2) (-1) = kB ∧ classical 0 0 0 1 = temp := by decide9899/-- 00:C12, 7:A32 — recovered in arity: the classical four symbols generate the lift's three (two generators and the100flag) — `L`, `T` and the flag are classical monomials, the kernel's generator `Θ L⁻¹ T²` maps to the trivial domain,101and the `M`-`L`-`T` block of the dictionary, the determinant of the images of `M`, `L`, `T`, is unimodular (determinant 1) — with the one relation `Θ = L T⁻²`, so102temperature is not a fourth generator; the flag's fourth power is the trivial domain only modulo `4κ`, which the103lift does not carry: `flag⁴ ≠ 1` in the lattice. -/104theorem classical_arity :105 classical 0 1 0 0 = L ∧ classical 0 0 1 0 = T ∧ classical 1 2 (-1) 0 = flag ∧106 classical 0 0 0 1 = classical 0 1 (-2) 0 ∧ classical 0 (-1) 2 1 = 1 ∧107 (classical 1 0 0 0).r * ((classical 0 1 0 0).s * (classical 0 0 1 0).j - (classical 0 1 0 0).j * (classical 0 0 1 0).s)108 - (classical 1 0 0 0).s * ((classical 0 1 0 0).r * (classical 0 0 1 0).j - (classical 0 1 0 0).j * (classical 0 0 1 0).r)109 + (classical 1 0 0 0).j * ((classical 0 1 0 0).r * (classical 0 0 1 0).s - (classical 0 1 0 0).s * (classical 0 0 1 0).r) = 1 ∧110 flag * flag * flag * flag ≠ 1 := by decide111112/-- The modular image of a lift triple in the Subject's domain group `D_p = C_p × C_{4κ}`: `(r mod p, s + κj mod 4κ)`,113the flag `Iq = T^κ` folded into the time exponent. -/114def reduce (p κ : Nat) (a : Lift) : Int × Int := (a.r % (p : Int), (a.s + (κ : Int) * a.j) % (4 * κ : Int))115116/-- 00:C12, 7:A32 — the torsion-free shadow: on the three Subjects `p = 13, 173, 1373` (`κ = 3, 43, 343`) the identities hold117in the modular group `C_p × C_{4κ}` of 10-dimensions, the flag reduces to `T^κ`, its fourth power to the trivial domain118while its first three powers reduce to `(0, κ)`, `(0, 2κ)`, `(0, 3κ)`, and the mass and temperature domains reduce to their119residues. -/120theorem modular_shadow :121 reduce 13 3 temp = reduce 13 3 accel ∧ reduce 13 3 unruh = reduce 13 3 temp ∧ reduce 13 3 temp = (1, 10) ∧122 reduce 13 3 flag = (0, 3) ∧ reduce 13 3 (T * T * T) = (0, 3) ∧ reduce 13 3 (flag * flag * flag * flag) = (0, 0) ∧123 reduce 13 3 flag ≠ (0, 0) ∧ reduce 13 3 (flag * flag) ≠ (0, 0) ∧ reduce 13 3 (flag * flag * flag) ≠ (0, 0) ∧124 reduce 13 3 mass = (11, 4) ∧125 reduce 173 43 temp = reduce 173 43 accel ∧ reduce 173 43 unruh = reduce 173 43 temp ∧ reduce 173 43 temp = (1, 170) ∧126 reduce 173 43 flag = (0, 43) ∧ reduce 173 43 (flag * flag * flag * flag) = (0, 0) ∧ reduce 173 43 (flag * flag) = (0, 86) ∧127 reduce 173 43 (flag * flag * flag) = (0, 129) ∧ reduce 173 43 mass = (171, 44) ∧128 reduce 1373 343 temp = reduce 1373 343 accel ∧ reduce 1373 343 unruh = reduce 1373 343 temp ∧129 reduce 1373 343 flag = (0, 343) ∧ reduce 1373 343 (flag * flag * flag * flag) = (0, 0) ∧ reduce 1373 343 (flag * flag) = (0, 686) ∧130 reduce 1373 343 (flag * flag * flag) = (0, 1029) ∧ reduce 1373 343 mass = (1371, 344) := by decide131132end Lift133134end FRC.Domain135