def definition def or abbrev

`phi_inv`

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

formal statement (Lean)

  70def phi_inv : ℝ := 1 / Constants.phi

Definition body.

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

phi_inv in IndisputableMonolith.Algebra.PhiRing decl_use
phi_inv in IndisputableMonolith.Foundation.Inequalities decl_use
phi_inv_eq in IndisputableMonolith.Foundation.PhiEmergence decl_use
J_phi in IndisputableMonolith.Foundation.PhiForcing decl_use
phi_inv in IndisputableMonolith.Foundation.PhiForcing decl_use
fractions_sum_to_one in IndisputableMonolith.Linguistics.LexiconRatio decl_use
lexicon_ratio in IndisputableMonolith.Linguistics.LexiconRatio decl_use
passive_fraction in IndisputableMonolith.Linguistics.LexiconRatio decl_use
passive_fraction_eq_phi_sq_inv in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_band in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_fibonacci_fixed_point in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_lt_one in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_pos in IndisputableMonolith.Linguistics.LexiconRatio decl_use
phi_inv_unique in IndisputableMonolith.Linguistics.LexiconRatio decl_use
ConstantsPredictionsCert in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use

Lean names referenced from this declaration's body.