def definition def or abbrev

`f_gap`

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

formal statement (Lean)

  98def f_gap (w8 : ℝ) : ℝ := w8 * Real.log φ where

proof body

Definition body.

  99  φ := (1 + Real.sqrt 5) / 2
 100
 101/-- First-order curvature correction. -/

used by (40)

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
alphaInv_derived in IndisputableMonolith.Constants.AlphaDerivation decl_use
alphaInv_derived_eq_formula in IndisputableMonolith.Constants.AlphaDerivation decl_use
curvature_term_eq in IndisputableMonolith.Constants.AlphaDerivation decl_use
alphaInv_def in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alphaInv_linear_rate 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_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
deriv_alphaInv_of_gap in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
exp_factor_bounded in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
exponential_form_uniqueness_ode_principle 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
exp_minus_add_pos in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
exponential_residual in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
f_gap in IndisputableMonolith.Constants.GapWeight decl_use
f_gap_bounds_hypothesis in IndisputableMonolith.Constants.GapWeight decl_use
alphaInv_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alphaInv_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
alpha_seed_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
f_gap_gt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
f_gap_gt_strong in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
f_gap_lt in IndisputableMonolith.Numerics.Interval.AlphaBounds decl_use
f_gap in IndisputableMonolith.Pipelines decl_use

… and 10 more

depends on (3)

Lean names referenced from this declaration's body.

f_gap in IndisputableMonolith.Constants.GapWeight decl_use
correction in IndisputableMonolith.Information.QuantumChannelCapacityFromPhi decl_use
f_gap in IndisputableMonolith.Pipelines decl_use