def definition def or abbrev

`phiInterval`

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

formal statement (Lean)

  50def phiInterval : Interval where
  51  lo := 1618 / 1000

Definition body.

  52  hi := 1619 / 1000
  53  valid := by norm_num
  54
  55/-- φ is in phiInterval - PROVEN using sqrt bounds -/

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

phi_lo_pos in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_pow_140_in_interval in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_pow_140_lt_ratio in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_pow_142_lt_ratio_1_3 in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_pow_2_interval in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_pow_2_lo_pos in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_pow_38_interval in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
ratio_0_7_lt_phi_pow_142 in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
ratio_lt_phi_pow_145 in IndisputableMonolith.Numerics.Interval.GalacticBounds decl_use
phi_in_phiInterval in IndisputableMonolith.Numerics.Interval.Pow decl_use
phi_gt_161 in IndisputableMonolith.Numerics.Interval.Tactic decl_use
phi_interval_contains in IndisputableMonolith.Numerics.Interval.Tactic decl_use
phi_lt_162 in IndisputableMonolith.Numerics.Interval.Tactic decl_use

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Interval in IndisputableMonolith.Numerics.Interval.Basic decl_use
Interval in IndisputableMonolith.Recognition.Certification decl_use