def definition def or abbrev

`gapAffineLog`

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

formal statement (Lean)

  43def gapAffineLog (a b c : ℝ) (Z : ℤ) : ℝ :=

Definition body.

  44  gapAffineLogR a b c (Z : ℝ)
  45
  46/-- `φ = 1 + 1/φ` (golden ratio identity). -/

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

affine_log_collapses_from_three_point_calibration in IndisputableMonolith.Masses.GapFunctionForcing decl_use
affine_log_collapses_to_canonical_gap in IndisputableMonolith.Masses.GapFunctionForcing decl_use
affine_log_unique_under_normalizations in IndisputableMonolith.Masses.GapFunctionForcing decl_use
gapAffineLog in IndisputableMonolith.Masses.GapFunctionForcing decl_use
ThreePointAffineLogClosure in IndisputableMonolith.Masses.GapFunctionForcing decl_use
affine_log_collapses_to_gap in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use
ThreePointClosure in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use
three_point_forces_canonical_gap in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use

Lean names referenced from this declaration's body.