structure definition def or abbrev

`ThreePointClosure`

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

formal statement (Lean)

 211structure ThreePointClosure (a b c : ℝ) where
 212  shift_forced : b = phi
 213  scale_forced : a = 1 / Real.log phi
 214  offset_forced : c = 0
 215  collapses_to_gap : ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z
 216
 217/-- Build the closure certificate from calibration data. -/

used by (1)

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

three_point_closure in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use

depends on (11)

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
gap in IndisputableMonolith.Gap45.Derivation decl_use
Z in IndisputableMonolith.Masses.Anchor decl_use
gap in IndisputableMonolith.Masses.AnchorPolicy decl_use
gapAffineLog in IndisputableMonolith.Masses.GapFunctionForcing decl_use
gap in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
calibration in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
Z in IndisputableMonolith.Physics.AnchorPolicyCertified decl_use
RSBridge in IndisputableMonolith.RecogSpec.RSBridge decl_use
gap in IndisputableMonolith.RSBridge.Anchor decl_use
gapAffineLog in IndisputableMonolith.RSBridge.GapFunctionForcing decl_use