theorem
proved
C_kernel_competing_pos
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.ILGSpatialKernel on GitHub at line 198.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
195def C_kernel_competing : ℝ := phi ^ (-(3 / 2 : ℝ))
196
197/-- `C'` is positive. -/
198theorem C_kernel_competing_pos : 0 < C_kernel_competing := by
199 unfold C_kernel_competing
200 exact Real.rpow_pos_of_pos phi_pos _
201
202/-- The competing amplitude is strictly larger than the structurally
203 forced amplitude. -/
204theorem C_competing_gt_C_kernel :
205 C_kernel < C_kernel_competing := by
206 unfold C_kernel C_kernel_competing
207 -- phi^(-2) < phi^(-3/2) since phi > 1 and -2 < -3/2
208 have hphi_gt_one : 1 < phi := one_lt_phi
209 exact Real.rpow_lt_rpow_of_exponent_lt hphi_gt_one (by norm_num : (-(2 : ℝ)) < -(3/2 : ℝ))
210
211/-- The competing amplitude `C'` PLUS `J(φ)` exceeds the half-rung
212 budget, violating the structural identity `J(φ) + C = 1/2`. -/
213theorem C_competing_violates_budget :
214 Jphi_penalty + C_kernel_competing > 1 / 2 := by
215 have h1 : Jphi_penalty + C_kernel = 1 / 2 := half_rung_budget
216 have h2 : C_kernel < C_kernel_competing := C_competing_gt_C_kernel
217 linarith
218
219/-! ## §6. Structural three-channel factorization sketch
220
221The amplitude `C = φ⁻²` admits the structural decomposition
222 `C = (longitudinal weight) × (transverse-collective weight) = φ⁻¹ · φ⁻¹`
223in `D = 3` spatial dimensions. We record the per-channel weight and
224the product as named definitions for transparency.
225-/
226
227/-- The per-channel ladder weight: `φ⁻¹`. One step on the φ-ladder. -/
228def channel_weight : ℝ := phi ^ (-(1 : ℝ))