`three_point_closure`

proved

show as: view math explainer →

module: IndisputableMonolith.RSBridge.GapFunctionForcing
domain: RSBridge
line: 218 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RSBridge.GapFunctionForcing on GitHub at line 218.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 215  collapses_to_gap : ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z
 216
 217/-- Build the closure certificate from calibration data. -/
 218theorem three_point_closure
 219    {a b c : ℝ}
 220    (hb : 1 < b)
 221    (h0 : gapAffineLogR a b c 0 = 0)
 222    (h1 : gapAffineLogR a b c 1 = 1)
 223    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 224    ThreePointClosure a b c := by
 225  have hparams := affine_log_parameters_forced hb h0 h1 hneg1
 226  exact ⟨hparams.1, hparams.2.1, hparams.2.2,
 227         three_point_forces_canonical_gap hb h0 h1 hneg1⟩
 228
 229end
 230end GapFunctionForcing
 231end RSBridge
 232end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.