C_competing_gt_C_kernel

formal source

 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 : ℝ))
 229
 230/-- `channel_weight = 1/φ = φ - 1`. -/
 231theorem channel_weight_eq : channel_weight = phi - 1 := by
 232  unfold channel_weight
 233  rw [show (-(1 : ℝ)) = ((-1) : ℤ) from by norm_num]
 234  rw [Real.rpow_intCast]