def
definition
C_ilg_prefactor
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Gravity.CoerciveProjection on GitHub at line 132.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
129
130/-- The ILG kernel prefactor C = phi^(-3/2) from the CPM and Dark-Energy papers.
131 This replaces the earlier phi^(-5) = cLagLock in the galactic-scale kernel. -/
132noncomputable def C_ilg_prefactor : ℝ := phi ^ (-(3/2 : ℝ))
133
134theorem C_ilg_prefactor_pos : 0 < C_ilg_prefactor := by
135 unfold C_ilg_prefactor
136 exact Real.rpow_pos_of_pos phi_pos _
137
138/-- The ILG alpha exponent: alpha = (1 - 1/phi) / 2 = alphaLock. -/
139theorem ilg_alpha_is_alphaLock : alphaLock = (1 - 1/phi) / 2 := rfl
140
141/-! ## Certificate -/
142
143structure CoerciveProjectionCert where
144 coercivity_positive : (0 : ℚ) < c_coercive
145 net_above_one : (1 : ℚ) < K_net
146 operator_positive : ∀ w f : ℝ, 1 ≤ w → 0 ≤ w * f ^ 2
147 prefactor_positive : 0 < C_ilg_prefactor
148
149theorem coercive_projection_cert : CoerciveProjectionCert where
150 coercivity_positive := c_coercive_pos
151 net_above_one := K_net_gt_one
152 operator_positive := fun w f hw => energy_bounded_below w f hw (sq_nonneg f)
153 prefactor_positive := C_ilg_prefactor_pos
154
155end
156
157end CoerciveProjection
158end Gravity
159end IndisputableMonolith