def definition def or abbrev

`lambda`

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

formal statement (Lean)

  92def lambda : ℝ := Real.log phi

proof body

Definition body.

  93
  94/-- λ is positive. -/

used by (40)

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

balance_determines_lambda in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
balanceResidual in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
balance_unique_positive_root in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
J_curv in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
J_curv_derivation 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_unique_root in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
totalCost in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
darkEnergyDensity in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
diagonal_continuous_on_range in IndisputableMonolith.Foundation.PolynomialityFromLogic decl_use
coupling_from_spectral in IndisputableMonolith.Gravity.CaldeiraLeggett decl_use
christoffel_symmetric in IndisputableMonolith.Gravity.Connection decl_use
metric_compatibility in IndisputableMonolith.Gravity.Connection decl_use
algebraic_bianchi in IndisputableMonolith.Gravity.RiemannTensor decl_use
riemann_tensor in IndisputableMonolith.Gravity.RiemannTensor decl_use
AnchorPolicy in IndisputableMonolith.Masses.AnchorPolicy decl_use
canonicalPolicy in IndisputableMonolith.Masses.AnchorPolicy decl_use
AnchorSpec in IndisputableMonolith.Physics.AnchorPolicy decl_use
canonicalAnchor in IndisputableMonolith.Physics.AnchorPolicy decl_use
stationary_at_anchor in IndisputableMonolith.Physics.AnchorPolicy decl_use
integratedResidue in IndisputableMonolith.Physics.RGTransport decl_use
lambda_pos in IndisputableMonolith.Physics.RGTransport decl_use
mass_ratio_phi_power in IndisputableMonolith.Physics.RGTransport decl_use
residueDerivative in IndisputableMonolith.Physics.RGTransport decl_use
stationarity_iff_gamma_zero in IndisputableMonolith.Physics.RGTransport decl_use
amplitude in IndisputableMonolith.Quantum.DoubleSlit decl_use
bright_fringes in IndisputableMonolith.Quantum.DoubleSlit decl_use
dark_fringes in IndisputableMonolith.Quantum.DoubleSlit decl_use
DoubleSlitSetup in IndisputableMonolith.Quantum.DoubleSlit decl_use

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.

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