Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration

show as:
view Lean formalization →

Isolates continuum one-act log-curvature as the calibration datum for the recognition cost: the second derivative at the identity ratio, living in the real-delta protocol layer rather than the discrete rational carrier. Proves the discrete carrier alone cannot force the unit, while a normalized one-act interface forces J and is necessary and sufficient to close the calibration gap. Downstream native-analysis, objecthood, and physical one-act modules import this layer. Mix of interface definitions and forcing lemmas.

claimOne-act log-curvature of a cost member with unit $c$ is $\partial_t^2$ of the cost at the limit ratio $t=0$ (a continuum-interface quantity). The discrete rational carrier does not force the unit. A normalized one-act continuum interface forces the unique cost $J(x)=(x+x^{-1})/2-1$, and that calibration datum is necessary and sufficient to close the gap.

background

Primitive Recognition Calculus separates a discrete rational carrier from a continuum protocol layer $\mathbb{R}_\delta$. The cost functional on positive reals is pinned in the forcing chain by T5 to $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), subject to the Recognition Composition Law. Calibration asks which minimal continuum datum selects the unit and forces that $J$.

This module introduces one-act log-curvature: the second derivative of the cost member at the identity ratio $t=0$. That quantity is intrinsically continuum (a second derivative), so it cannot be read off the discrete carrier alone. Sibling structures package a normalized one-act interface and a canonical interface against which necessity and sufficiency of the calibration datum are stated.

Upstream dependency is the PRC calibration-target module, which supplies the target shape this layer fills.

proof idea

Definition spine first: one-act curvature as the $t=0$ second derivative, equality lemmas relating presentations, and the normalized one-act interface structure (plus a canonical interface). Forcing direction: the normalized interface implies uniqueness of $J$. Separation: a discrete-only argument is shown not to force the unit, so calibration is genuinely one continuum act. Closure: the calibration datum is proved necessary and sufficient, and the calibration gap is discharged by the normalized interface. No single master tactic proof; the module is a short chain of definitions plus forcing and separation lemmas.

why it matters in Recognition Science

Closes the continuum side of PRC calibration before native analysis and physical reading. Downstream importers are DeltaNativeAnalysis, DeltaNativeStrongClosure, ObjecthoodRegistry, and PhysicalOneActCalibration: they treat the one-act curvature and normalized interface as the fixed calibration layer rather than re-deriving the unit. Ties directly to T5 J-uniqueness in the unified forcing chain: once the normalized one-act interface is in place, $J$ is forced and the calibration gap is closed. Without this separation, discrete carrier arguments could be mistaken for a full unit-fixing proof.

scope and limits

used by (4)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (10)