theorem proved term proof

`alphaInv_def`

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

formal statement (Lean)

  57theorem alphaInv_def : alphaInv = alpha_seed * Real.exp (-(f_gap / alpha_seed)) := rfl

Term-mode proof.

  58
  59/-- The seed is positive: α_seed = 4π·11 > 0. -/

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

exponential_form_uniqueness_ode_principle in IndisputableMonolith.Constants.AlphaExponentialForm decl_use

Lean names referenced from this declaration's body.

alphaInv in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
f_gap in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
f_gap in IndisputableMonolith.Constants.GapWeight decl_use
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
f_gap in IndisputableMonolith.Pipelines decl_use