three_channel_factorization

formal source

 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).
 2626. **competing_excluded**: `C' = φ⁻³ᐟ²` violates the budget identity.
 263-/
 264structure ILGSpatialKernelCert where
 265  closed_form : C_kernel = 2 - phi
 266  positivity : 0 < C_kernel
 267  budget : Jphi_penalty + C_kernel = 1 / 2
 268  band : (0.380 : ℝ) < C_kernel ∧ C_kernel < (0.390 : ℝ)
 269  factorization : C_kernel = channel_weight * channel_weight
 270  competing_excluded : Jphi_penalty + C_kernel_competing > 1 / 2
 271
 272/-- The master certificate is inhabited. -/
 273def ilgSpatialKernelCert : ILGSpatialKernelCert where
 274  closed_form := C_kernel_eq_two_minus_phi
 275  positivity := C_kernel_pos