structure definition def or abbrev

`CalibrationFromUnitChoice`

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

formal statement (Lean)

  78structure CalibrationFromUnitChoice (J : ℝ → ℝ) : Prop where
  79  calibration : (deriv (deriv (fun t => J (Real.exp t)))) 0 = 1
  80
  81/-- Explicit split version of the regularity seam.
  82
  83Instead of a single broad `RegularityCert`, the reconstruction theorem now
  84tracks continuity, convexity, and calibration as independently auditable
  85obligations. -/

used by (1)

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

FiniteDescriptionRegularity in IndisputableMonolith.Foundation.ClosedObservableFramework decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
RegularityCert in IndisputableMonolith.Foundation.ClosedObservableFramework decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
calibration in IndisputableMonolith.Measurement.RSNative.Calibration.SingleAnchor decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use