pith. machine review for the scientific record. sign in
theorem proved term proof

three_channel_factorization

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 245theorem three_channel_factorization :
 246    C_kernel = channel_weight * channel_weight := by

proof body

Term-mode proof.

 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-/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.