C_competing_violates_budget

formal source

 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]
 235  rw [zpow_neg, zpow_one, ← one_div]
 236  have h_phi_ne : phi ≠ 0 := ne_of_gt phi_pos
 237  have h_sq := phi_sq_eq
 238  field_simp
 239  linarith
 240
 241/-- **THEOREM.** The three-channel factorization product
 242    `C = (longitudinal weight) × (transverse-collective weight)`
 243    with each weight equal to `channel_weight = φ⁻¹` reproduces