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)
215theorem euler_phi_connection :
216 -- cos(π/5) = φ/2 (the real part of e^(iπ/5))
217 Real.cos (Real.pi / 5) = phi / 2 := by
proof body
Term-mode proof.
218 rw [Real.cos_pi_div_five]
219 -- phi / 2 = (1 + sqrt 5) / 2 / 2 = (1 + sqrt 5) / 4
220 unfold phi
221 ring
222
223/-! ## RS Interpretation -/
224
225/-- RS interpretation of e:
226
227 1. **J-cost decay**: Probabilities involve e^(-J)
228 2. **Continuous time**: e^(iωt) for oscillations
229 3. **Growth rate**: Maximum sustainable rate is e
230 4. **8-tick phases**: exp(2πik/8) uses e
231
232 e is the natural base for ledger dynamics. -/
depends on (14)
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
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
cost
in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
decl_use
-
cost
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use