def
definition
predict_mass_sdgt
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.AnchorPolicy on GitHub at line 72.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
69 | _ => 0
70
71/-- SDGT mass prediction: m = A_s × φ^(r_sdgt - 8 + gap(Z) + shift). -/
72noncomputable def predict_mass_sdgt (sector : Anchor.Sector) (name : String) : ℝ :=
73 Anchor.yardstick sector *
74 Constants.phi ^ (rung_sdgt sector name + gap sector name - 8 + cross_sector_shift sector)
75
76structure AnchorPolicy where
77 lambda : ℝ
78 kappa : ℝ
79
80/-- Canonical anchor policy: `(λ, κ) = (ln φ, φ)` with coherence energy. -/
81@[simp] noncomputable def canonicalPolicy : AnchorPolicy :=
82 { lambda := Real.log Constants.phi
83 , kappa := Constants.phi }
84
85noncomputable abbrev E_coh : ℝ := Anchor.E_coh
86noncomputable abbrev yardstick := Anchor.yardstick
87abbrev Z_index := ChargeIndex.Z
88abbrev r_lepton := Integers.r_lepton
89abbrev r_up := Integers.r_up
90abbrev r_down := Integers.r_down
91abbrev r_boson := Integers.r_boson
92
93structure ResidueLaw where
94 f : ℝ → ℝ
95
96structure SectorLaw where
97 params : SectorParams
98 residue : ResidueLaw
99
100end Masses
101end IndisputableMonolith