channel_weight_eq

formal source

 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
 244    `C = φ⁻²`. -/
 245theorem three_channel_factorization :
 246    C_kernel = channel_weight * channel_weight := by
 247  unfold C_kernel channel_weight
 248  rw [show ((-2 : ℝ)) = ((-1 : ℝ)) + ((-1 : ℝ)) from by ring]
 249  exact Real.rpow_add phi_pos _ _
 250
 251/-! ## §7. Master certificate -/
 252
 253/-- **ILG SPATIAL-KERNEL AMPLITUDE MASTER CERTIFICATE.**
 254
 255Six clauses, all derived from the RCL and `φ² = φ + 1`:
 256
 2571. **closed_form**: `C = 2 - φ` (from `φ⁻¹ = φ - 1`).
 2582. **positivity**: `0 < C`.
 2593. **budget**: `J(φ) + C = 1/2` (the half-rung budget identity).
 2604. **band**: `C ∈ (0.380, 0.385)` from `φ ∈ (1.61, 1.62)`.
 2615. **factorization**: `C = (1/φ) · (1/φ)` (three-channel decomposition).