theorem proved term proof

`octagon_bounds`

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

formal statement (Lean)

  90theorem octagon_bounds :
  91    -- 3.06 < π < 3.31 from 8-gon
  92    True := trivial

proof body

Term-mode proof.

  93
  94/-! ## The 8-Tick Connection -/
  95
  96/-- Why 8 is special for approximating π:
  97
  98    sin(π/8) = √((1 - cos(π/4))/2) = √((1 - 1/√2)/2)
  99
 100    This involves √2, which has nice properties.
 101
 102    The 8-tick structure gives π/4 = 45° as a fundamental angle.
 103    This relates to the 8th roots of unity. -/

depends on (19)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
tick in IndisputableMonolith.Constants decl_use
tick in IndisputableMonolith.Constants.RSNativeUnits decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Tick in IndisputableMonolith.Foundation.TimeEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
Tick in IndisputableMonolith.Masses.Ribbons decl_use
Tick in IndisputableMonolith.Masses.Ribbons.Tick decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Tick in IndisputableMonolith.Measurement.RSNative.Core decl_use