theorem proved term proof

`G_pos`

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

formal statement (Lean)

 152theorem G_pos : G_rs > 0 := by

Term-mode proof.

 153  unfold G_rs
 154  exact pow_pos phi_pos 5
 155
 156/-- G is algebraic in φ. -/

From the project-wide theorem graph. These declarations reference this one in their body.

lambda_rec_dimensionless_id_physical in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
G_pos in IndisputableMonolith.Constants decl_use
kappa_einstein_pos in IndisputableMonolith.Constants decl_use
G_ne_zero in IndisputableMonolith.Constants.Codata decl_use
G_pos in IndisputableMonolith.Constants.Codata decl_use
ell_P_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_over_ell_P in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
lambda_rec_SI_pos in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
planck_gate_normalized in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
rs_entropy_pos in IndisputableMonolith.Gravity.UltramassiveBH decl_use
potential_negative in IndisputableMonolith.Gravity.ZeroParameterGravity decl_use
planckConstantCert in IndisputableMonolith.Physics.PlanckConstantFromRS decl_use
PlanckConstantCert in IndisputableMonolith.Physics.PlanckConstantFromRS decl_use
temperature_from_surface_gravity in IndisputableMonolith.Quantum.BekensteinHawking decl_use
hbar_over_G in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G_pos in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G_pos in IndisputableMonolith.Constants.Codata decl_use
G_rs in IndisputableMonolith.Constants.GravitationalConstant decl_use
G in IndisputableMonolith.Cost.FunctionalEquation decl_use
G_rs in IndisputableMonolith.Foundation.ConstantDerivations decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
G_rs in IndisputableMonolith.Papers.GCIC.BekensteinFromLedger decl_use