structure
definition
AnchorPolicy
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Masses.AnchorPolicy on GitHub at line 76.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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