def definition def or abbrev

`lambda_rec`

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

formal statement (Lean)

 425noncomputable def lambda_rec : ℝ := ell0

proof body

Definition body.

used by (21)

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

lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id_physical in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
G in IndisputableMonolith.Constants decl_use
kappa_einstein_eq in IndisputableMonolith.Constants decl_use
lambda_rec_pos in IndisputableMonolith.Constants decl_use
GDerivationChain in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
lambda_rec_is_forced in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
lambda_rec_is_root in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
lambda_rec_unique_root in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
one_over_sqrt_pi_approx in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
planck_gate_identity in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
planck_gate_normalized in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
G_div_hbar in IndisputableMonolith.Masses.AlphaGScoreCard decl_use
alpha_locked in IndisputableMonolith.Physics.CouplingLockIn decl_use
pbh_shadow_detectable in IndisputableMonolith.Relativity.Lensing.ShadowPredictions decl_use
shadow_diameter_correction in IndisputableMonolith.Relativity.Lensing.ShadowPredictions decl_use
G_derived in IndisputableMonolith.RRF.Foundation.Constants decl_use
G_eq_inv_pi_hbar in IndisputableMonolith.Unification.QuantumGravityOctaveDuality decl_use

depends on (3)

Lean names referenced from this declaration's body.

lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
ell0 in IndisputableMonolith.Constants decl_use
ell0 in IndisputableMonolith.Constants.Derivation decl_use