lemma proved term proof

`lambda_rec_dimensionless_id_physical`

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

formal statement (Lean)

  63lemma lambda_rec_dimensionless_id_physical (B : BridgeData) (H : Physical B) :
  64  (B.c ^ 3) * (lambda_rec B) ^ 2 / (B.hbar * B.G) = 1 / Real.pi :=

proof body

Term-mode proof.

  65  lambda_rec_dimensionless_id B H.c_pos H.hbar_pos H.G_pos
  66
  67/-- Positivity of λ_rec under physical assumptions. -/

depends on (29)

Lean names referenced from this declaration's body.

H in IndisputableMonolith.Algebra.CostAlgebra decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
BridgeData in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id in IndisputableMonolith.Bridge.DataCore decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
c_pos in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants decl_use
G_pos in IndisputableMonolith.Constants decl_use
hbar in IndisputableMonolith.Constants decl_use
hbar_pos in IndisputableMonolith.Constants decl_use
lambda_rec in IndisputableMonolith.Constants decl_use
c_pos in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G_pos in IndisputableMonolith.Constants.Codata decl_use
hbar in IndisputableMonolith.Constants.Codata decl_use
hbar_pos in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
H in IndisputableMonolith.Cost.FunctionalEquation 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
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
BridgeData in IndisputableMonolith.Gravity.ILG decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
hbar in IndisputableMonolith.Information.ComputationLimitsStructure decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
hbar in IndisputableMonolith.Quantum.EntanglementEntropy decl_use