theorem proved term proof

`passive_fraction_eq_phi_sq_inv`

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

formal statement (Lean)

 145theorem passive_fraction_eq_phi_sq_inv :
 146    passive_fraction = phi_inv ^ 2 := by

proof body

Term-mode proof.

 147  unfold passive_fraction
 148  have h := phi_inv_fibonacci_fixed_point
 149  linarith
 150
 151/-- **σ-CONSERVATION ON LEXICON.** Active + passive = 1. -/

depends on (6)

Lean names referenced from this declaration's body.

phi_inv in IndisputableMonolith.Algebra.PhiRing decl_use
phi_inv in IndisputableMonolith.Foundation.Inequalities decl_use
phi_inv in IndisputableMonolith.Foundation.PhiForcing decl_use
passive_fraction in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_fibonacci_fixed_point in IndisputableMonolith.Linguistics.LexiconRatio decl_use