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)
287structure PlanckScaleMatchingCert where
288 /-- J_bit is well-defined and positive -/
289 J_bit_ok : J_bit_val > 0
290 /-- J_bit ≈ 0.118 -/
291 J_bit_numerical : 0.11 < J_bit_val ∧ J_bit_val < 0.12
292 /-- The extremum determines λ_rec -/
293 extremum_determines : J_curv lambda_rec_from_Jbit = J_bit_val
294 /-- The Planck ratio is 1/√π -/
295 planck_ratio : lambda_rec_SI / ell_P = 1 / sqrt Real.pi
296
297/-- The Planck-Scale Matching Certificate is verified. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (11)
Lean names referenced from this declaration's body.
-
J_curv
in IndisputableMonolith.Constants.LambdaRecDerivation
decl_use
-
ell_P
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
J_bit_val
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
J_curv
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
lambda_rec_from_Jbit
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
lambda_rec_SI
in IndisputableMonolith.Constants.PlanckScaleMatching
decl_use
-
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
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use