The core module lean/FrcCore/Keys/Domain.lean — the substrate from first principles, no Mathlib, no axioms; one of the core's 137 modules (the index); it rests on 1 module: Theme/Domain: 1 theorems (0 definitions): 1 with no axioms, 0 at tier 1 (propext, Quot.sound), 0 at tier 2 (Classical.choice), 0 red; the mark's colour is the library's (green, the core; red a proof the gate rejects), each declaration's axioms on hover; the small plain glyph marks a definition (no proof, no axioms; on the ledger pages the plain glyph is instead a module cited as a whole). Each declaration is anchored; the ledger predicates cite them by name. ▶ open in Lean Live · axioms.log.
1import FrcCore.Theme.Domain23/-!4# FrcCore.Keys.Domain — the keyed theorems of the domain theme (ledger migration, task LM19)56One declaration per key, `FRC.Ledger.p<key>`, generated by `make_keys.py` from the ledgers' Lean bindings: the theorem7that every row carrying the key asserts, proved from the themes alone. The paper's module keeps its declaration8`FRC.<Module>.p<key>` as an alias. Every declaration has no axioms (`check_core_axioms.py`).9-/1011namespace FRC.Ledger1213-- Keys of the domain theme (generated by make_keys.py from the ledgers' Lean bindings; edit the ledgers, not this file)14/-- p00032 — 7:A32, 00:C12. \textbf{Temperature and the classical arity, derived}: the temperature domain is acceleration, $[\Theta]=[E][k_B]^{-1}=[L][T]^{-2}$, flag-free, $\Theta_P=E_P/|k_B|$, Unruh closing as a domain identity; neither mass nor temperature is primitive --- $M$-$L$-$T$-plus-thermal is the torsion-free shadow of the two-generators-plus-flag system (the mass primitive standing in for the flag, the thermal for $k_B$), classical dimensional analysis recovered in exponents and arity. -/15
theorem p00032 : (FRC.Domain.Lift.temp = FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.temp = { r := (1 : Int), s := (-2 : Int), j := (0 : Int) } ∧ FRC.Domain.Lift.kB = { r := (-1 : Int), s := (1 : Int), j := (1 : Int) }) ∧ (FRC.Domain.Lift.temp.j = (0 : Int) ∧ FRC.Domain.Lift.energy.j = (1 : Int) ∧ FRC.Domain.Lift.hbar.j = (1 : Int) ∧ FRC.Domain.Lift.kB.j = (1 : Int)) ∧ (FRC.Domain.Lift.unruh = FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.unruh.j = (0 : Int)) ∧ (FRC.Domain.Lift.mass = { r := (-2 : Int), s := (1 : Int), j := (1 : Int) } ∧ FRC.Domain.Lift.temp = FRC.Domain.Lift.L * FRC.Domain.Lift.T⁻¹ * FRC.Domain.Lift.T⁻¹ ∧ FRC.Domain.Lift.energy * (FRC.Domain.Lift.hbar * FRC.Domain.Lift.speed⁻¹)⁻¹ = FRC.Domain.Lift.accel ∧ (FRC.Domain.Lift.energy * (FRC.Domain.Lift.hbar * FRC.Domain.Lift.speed⁻¹)⁻¹).j = (0 : Int)) ∧ (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int) = FRC.Domain.Lift.mass ∧ FRC.Domain.Lift.classical (0 : Int) (1 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.speed ∧ FRC.Domain.Lift.classical (0 : Int) (1 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.energy ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.hbar ∧ FRC.Domain.Lift.classical (1 : Int) (1 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.force ∧ FRC.Domain.Lift.classical (1 : Int) (1 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.momentum ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-3 : Int) (0 : Int) = FRC.Domain.Lift.power ∧ FRC.Domain.Lift.classical (1 : Int) (-1 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.pressure ∧ FRC.Domain.Lift.classical (-1 : Int) (3 : Int) (-2 : Int) (0 : Int) = FRC.Domain.Lift.G ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-2 : Int) (-1 : Int) = FRC.Domain.Lift.kB ∧ FRC.Domain.Lift.classical (0 : Int) (0 : Int) (0 : Int) (1 : Int) = FRC.Domain.Lift.temp) ∧ (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int) = FRC.Domain.Lift.L ∧ FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int) = FRC.Domain.Lift.T ∧ FRC.Domain.Lift.classical (1 : Int) (2 : Int) (-1 : Int) (0 : Int) = FRC.Domain.Lift.flag ∧ FRC.Domain.Lift.classical (0 : Int) (0 : Int) (0 : Int) (1 : Int) = FRC.Domain.Lift.classical (0 : Int) (1 : Int) (-2 : Int) (0 : Int) ∧ FRC.Domain.Lift.classical (0 : Int) (-1 : Int) (2 : Int) (1 : Int) = (1 : FRC.Domain.Lift) ∧ (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int)).r * ((FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).s * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).j - (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).j * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).s) - (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int)).s * ((FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).r * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).j - (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).j * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).r) + (FRC.Domain.Lift.classical (1 : Int) (0 : Int) (0 : Int) (0 : Int)).j * ((FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).r * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).s - (FRC.Domain.Lift.classical (0 : Int) (1 : Int) (0 : Int) (0 : Int)).s * (FRC.Domain.Lift.classical (0 : Int) (0 : Int) (1 : Int) (0 : Int)).r) = (1 : Int) ∧ FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag ≠ (1 : FRC.Domain.Lift)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.temp = FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.unruh = FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.temp = ((1 : Int), (10 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.flag = ((0 : Int), (3 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.T * FRC.Domain.Lift.T * FRC.Domain.Lift.T) = ((0 : Int), (3 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.flag ≠ ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) ≠ ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) ≠ ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (13 : Nat) (3 : Nat) FRC.Domain.Lift.mass = ((11 : Int), (4 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.temp = FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.unruh = FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.temp = ((1 : Int), (170 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.flag = ((0 : Int), (43 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (86 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (129 : Int)) ∧ FRC.Domain.Lift.reduce (173 : Nat) (43 : Nat) FRC.Domain.Lift.mass = ((171 : Int), (44 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.temp = FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.accel ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.unruh = FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.temp ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.flag = ((0 : Int), (343 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (0 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (686 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) (FRC.Domain.Lift.flag * FRC.Domain.Lift.flag * FRC.Domain.Lift.flag) = ((0 : Int), (1029 : Int)) ∧ FRC.Domain.Lift.reduce (1373 : Nat) (343 : Nat) FRC.Domain.Lift.mass = ((1371 : Int), (344 : Int)) :=16 And.intro @FRC.Domain.Lift.temp_eq_accel (And.intro @FRC.Domain.Lift.temp_flag_free (And.intro @FRC.Domain.Lift.unruh_closes (And.intro @FRC.Domain.Lift.not_primitive (And.intro @FRC.Domain.Lift.classical_exponents (And.intro @FRC.Domain.Lift.classical_arity (@FRC.Domain.Lift.modular_shadow))))))17-- end keys1819end FRC.Ledger20