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)
204noncomputable def gap45CrossoverModes : ℝ :=
proof body
Definition body.
205 criticalModes tau_bio 1.0
206
207/-- Approximation of Gap-45 crossover modes as a rational.
208 N ≈ ln(τ_bio/τ₀) / ln(φ) ≈ ln(1/(5.4e-44)) / 0.48
209 ≈ 99.3 / 0.48 ≈ 207
210
211 Since τ₀ ≈ 5.4×10⁻⁴⁴ s, τ_bio = 1 s:
212 ln(1/5.4e-44) ≈ 44 × ln(10) ≈ 44 × 2.3 ≈ 101
213 ln(φ) ≈ 0.48
214 N ≈ 101/0.48 ≈ 210 -/
depends on (9)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
modes
in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
criticalModes
in IndisputableMonolith.QFT.Decoherence
decl_use
-
tau_bio
in IndisputableMonolith.QFT.Decoherence
decl_use