lemma proved term proof

`f_gap_def`

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

formal statement (Lean)

  31@[simp] lemma f_gap_def : f_gap = Real.log (1 + 1 / phi) := rfl

proof body

Term-mode proof.

  32
  33end GapSeries
  34
  35namespace Curvature
  36
  37/-- Curvature-closure constant δ_κ used in the α pipeline.
  38Defined here as the exact rational/π expression from the voxel seam count. -/

depends on (7)

Lean names referenced from this declaration's body.

f_gap in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
f_gap in IndisputableMonolith.Constants.GapWeight decl_use
voxel in IndisputableMonolith.Constants.RSNativeUnits decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
f_gap in IndisputableMonolith.Pipelines decl_use
constant in IndisputableMonolith.Relativity.Fields.Scalar decl_use