pith. machine review for the scientific record. sign in
theorem proved term proof

three_point_affine_log_closure

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 236theorem three_point_affine_log_closure
 237    {a b c : ℝ}
 238    (hb : 1 < b)
 239    (h0 : gapAffineLogR a b c 0 = 0)
 240    (h1 : gapAffineLogR a b c 1 = 1)
 241    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 242    ThreePointAffineLogClosure (a := a) (b := b) (c := c) := by

proof body

Term-mode proof.

 243  have hparams : b = phi ∧ a = 1 / Real.log phi ∧ c = 0 :=
 244    affine_log_parameters_forced_by_three_point_calibration hb h0 h1 hneg1
 245  refine ⟨hparams.1, hparams.2.1, hparams.2.2, ?_⟩
 246  exact affine_log_collapses_from_three_point_calibration hb h0 h1 hneg1
 247
 248end
 249end GapFunctionForcing
 250end Masses
 251end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.