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)
157theorem Jcost_is_calibrated : FunctionalEquation.IsCalibrated Jcost := by
proof body
Term-mode proof.
158 change deriv (deriv (fun t : ℝ => Jcost (Real.exp t))) 0 = 1
159 exact IndisputableMonolith.CPM.LawOfExistence.RS.Jcost_log_second_deriv_normalized
160
161/-- Axiom-free uniqueness theorem on the paper's RCL theorem surface.
162
163This is the main unconditional IM-facing T5 statement: the caller supplies
164the reciprocal, normalization, composition, calibration, continuity, and
165explicit d'Alembert regularity hypotheses, and the conclusion is `F = Jcost`
166on `(0, ∞)`. -/
depends on (16)
Lean names referenced from this declaration's body.
-
reciprocal
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
IsCalibrated
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
main
in IndisputableMonolith.CPM.AuditMain
decl_use
-
Jcost_log_second_deriv_normalized
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
main
in IndisputableMonolith.Exports.Virtues
decl_use
-
reciprocal
in IndisputableMonolith.Foundation.LedgerForcing
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
calibration
in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
F
in IndisputableMonolith.Physics.AnchorPolicy
decl_use
-
F
in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation
decl_use
-
F
in IndisputableMonolith.Pipelines
decl_use
-
main
in IndisputableMonolith.URCAdapters.Audit
decl_use