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)
211theorem lambda_rec_SI_pos : lambda_rec_SI > 0 := by
proof body
Term-mode proof.
212 unfold lambda_rec_SI
213 apply sqrt_pos.mpr
214 apply div_pos
215 · exact mul_pos hbar_pos G_pos
216 · exact mul_pos Real.pi_pos (pow_pos c_pos 3)
217
218/-- **THE 0.564 FACTOR**:
219
220λ_rec/ℓ_P = 1/√π ≈ 0.564.
221
222This is the key result of Conjecture C8. -/
depends on (18)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
c_pos
in IndisputableMonolith.Constants
decl_use
-
G_pos
in IndisputableMonolith.Constants
decl_use
-
hbar_pos
in IndisputableMonolith.Constants
decl_use
-
c_pos
in IndisputableMonolith.Constants.Codata
decl_use
-
G_pos
in IndisputableMonolith.Constants.Codata
decl_use
-
hbar_pos
in IndisputableMonolith.Constants.Codata
decl_use
-
lambda_rec_SI
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
c_pos
in IndisputableMonolith.Foundation.ConstantDerivations
decl_use
-
G_pos
in IndisputableMonolith.Foundation.ConstantDerivations
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
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
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use