alphaInv — Recognition explainer

formal statement (Lean)

  35@[simp] def alphaInv : ℝ := alpha_seed * Real.exp (-(f_gap / alpha_seed))

proof body

Definition body.

  36
  37/-- Fine-structure constant (α_EM). -/

used by (40)

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

alphaInv_dimensionless in IndisputableMonolith.Bridge.GaugeVsParams decl_use
alphaInv_gauge_invariant in IndisputableMonolith.Bridge.GaugeVsParams decl_use
gap3_resolved in IndisputableMonolith.Bridge.GaugeVsParams decl_use
alpha in IndisputableMonolith.Constants.Alpha decl_use
alpha_components_derived in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alphaInv_def in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_of_gap in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_of_gap_at_canonical in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_positive in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_seed_ratio in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
exp_factor_bounded in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
log_alphaInv_eq in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
log_alphaInv_seed_ratio in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_predicted_range_check in IndisputableMonolith.Constants.AlphaNumericsScaffold decl_use
alphaInv_pos in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
HartreeRydbergScoreCardCert in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_bohr_over_reduced_compton in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_bohr_over_reduced_compton_eq in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_hartree_over_rest_eq in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_hartree_over_rest_lower in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_hartree_over_rest_upper in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_rydberg_over_rest_eq in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_rydberg_over_rest_lower in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
row_rydberg_over_rest_upper in IndisputableMonolith.Constants.HartreeRydbergScoreCard decl_use
alphaInv_rs in IndisputableMonolith.Constants.RSNativeUnits decl_use
NumericalPredictionsCert in IndisputableMonolith.Masses.NumericalPredictions decl_use
alphaInv_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alphaInv_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alphaInv_lt_strong in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use

… and 10 more

depends on (7)

Lean names referenced from this declaration's body.

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
f_gap in IndisputableMonolith.Pipelines decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use