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

channel_weight_eq

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)

 231theorem channel_weight_eq : channel_weight = phi - 1 := by

proof body

Term-mode proof.

 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 = φ⁻²`. -/

depends on (4)

Lean names referenced from this declaration's body.