structure definition def or abbrev

`ThreePointAffineLogClosure`

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

formal statement (Lean)

 229structure ThreePointAffineLogClosure (a b c : ℝ) where
 230  shift_forced : b = phi
 231  scale_forced : a = 1 / Real.log phi
 232  offset_forced : c = 0
 233  collapses_to_gap : ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z
 234
 235/-- Build the closure certificate from three-point calibration data. -/

used by (1)

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

three_point_affine_log_closure in IndisputableMonolith.Masses.GapFunctionForcing decl_use

depends on (12)

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
point in IndisputableMonolith.Numerics.Interval.Basic 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