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)
51theorem row_alphaG_pred_eq : row_alphaG_pred = G * electron_structural_mass ^ 2 / (hbar * c) := rfl
proof body
Term-mode proof.
52
53/-! ## Helper algebra (native units) -/
54
depends on (11)
Lean names referenced from this declaration's body.
-
G
in IndisputableMonolith.Constants
decl_use
-
hbar
in IndisputableMonolith.Constants
decl_use
-
G
in IndisputableMonolith.Constants.Codata
decl_use
-
hbar
in IndisputableMonolith.Constants.Codata
decl_use
-
G
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
G
in IndisputableMonolith.Gravity.JCostInflaton
decl_use
-
hbar
in IndisputableMonolith.Information.ComputationLimitsStructure
decl_use
-
row_alphaG_pred
in IndisputableMonolith.Masses.AlphaGScoreCard
decl_use
-
electron_structural_mass
in IndisputableMonolith.Physics.ElectronMass.Defs
decl_use
-
hbar
in IndisputableMonolith.Quantum.EntanglementEntropy
decl_use
-
electron_structural_mass
in IndisputableMonolith.RRF.Physics.ElectronMass.Defs
decl_use