alpha_seed — Recognition explainer

formal statement (Lean)

  95def alpha_seed : ℝ := 4 * π * passive_edges

proof body

Definition body.

  96
  97/-- Gap weight (from DFT-8 projection — see Constants.GapWeight). -/

used by (36)

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

alpha_components_derived in IndisputableMonolith.Constants.Alpha decl_use
alphaInv in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alphaInv_def in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_linear_term in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_of_gap in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_seed_ratio in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alpha_seed_positive in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
deriv_alphaInv_of_gap in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
exp_factor_bounded in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
exponential_form_from_constant_log_derivative 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
logarithmic_derivative_constant in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
additive_residual in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
AlphaPrecisionHypothesis in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
exp_minus_add_pos in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
exponential_residual in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
AlphaPrecisionCert in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed_eq in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed_gt_132 in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed_lt_176 in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed_positive in IndisputableMonolith.Constants.AlphaPrecision decl_use
alphaInv_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alphaInv_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alpha_seed_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alpha_seed_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alpha_pos_aux in IndisputableMonolith.StandardModel.WeakCoupling decl_use
WeakCouplingCert in IndisputableMonolith.StandardModel.WeakCoupling decl_use

… and 6 more

depends on (5)

Lean names referenced from this declaration's body.

alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
passive_edges in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
Constants in IndisputableMonolith.CPM.LawOfExistence decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use