`yardstick`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.Anchor
domain: Masses
line: 123 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.Anchor on GitHub at line 123.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 120  norm_num
 121
 122/-- Sector yardstick `A_s = 2^{B_pow} * E_coh * φ^{r0}`. -/
 123@[simp] noncomputable def yardstick (s : Sector) : ℝ :=
 124  (2 : ℝ) ^ (B_pow s) * E_coh * Constants.phi ^ (r0 s)
 125
 126end Anchor
 127
 128namespace Integers
 129
 130/-- Generation torsion (global, representation-independent).
 131    τ(0) = 0, τ(1) = E_passive = 11, τ(2) = W = 17 -/
 132@[simp] def tau (gen : ℕ) : ℤ :=
 133  match gen with
 134  | 0 => 0
 135  | 1 => (Anchor.E_passive : ℤ)  -- = 11
 136  | _ => (Anchor.W : ℤ)          -- = 17
 137
 138/-- Verify tau values. -/
 139theorem tau_values : tau 0 = 0 ∧ tau 1 = 11 ∧ tau 2 = 17 := by
 140  simp only [tau, Anchor.E_passive, Anchor.W, passive_field_edges, cube_edges,
 141             active_edges_per_tick, D, wallpaper_groups]
 142  norm_num
 143
 144/-- Rung integers for charged leptons.
 145    e: 2 (baseline), mu: 2 + tau(1) = 13, tau: 2 + tau(2) = 19 -/
 146@[simp] def r_lepton : String → ℤ
 147  | "e"   => 2
 148  | "mu"  => 2 + tau 1  -- = 2 + 11 = 13
 149  | "tau" => 2 + tau 2  -- = 2 + 17 = 19
 150  | _     => 0
 151
 152/-- Verify r_lepton values. -/
 153theorem r_lepton_values : r_lepton "e" = 2 ∧ r_lepton "mu" = 13 ∧ r_lepton "tau" = 19 := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.