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

kappa_calibration_positive

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)

 290theorem kappa_calibration_positive : 0 < Constants.kappa_einstein :=

proof body

Term-mode proof.

 291  jcost_to_regge_factor_eq_kappa_einstein ▸ jcost_to_regge_factor_pos
 292
 293/-! ## §6. Certificate
 294
 295The certificate packages (a) the independently-defined bridge theorem,
 296(b) the flat-vacuum consistency check, and (c) the dictionary from ψ to ε.
 297It makes the distinction from `ContinuumBridge.ContinuumBridgeCert` explicit:
 298the present certificate's bridge is *not* a definitional identity; it is
 299conditioned on `ReggeDeficitLinearizationHypothesis`. -/
 300

depends on (17)

Lean names referenced from this declaration's body.