Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaRealCalibration

show as:
view Lean formalization →

Calibrates the continuum real-delta interface of primitive recognition calculus via one-act log-curvature of the cost. A single continuum second derivative at the identity ratio forces the unit scale; the discrete rational carrier does not. Normalized one-act interfaces are necessary and sufficient to force J and close the calibration gap. Downstream native analysis, objecthood registry, and physical one-act calibration import this layer. Structure mixes curvature definitions with forcing and uniqueness lemmas.

claimOne-act log-curvature of a cost with unit $c$ is the second derivative at the limit ratio $t=0$ in the $\mathbb{R}_\delta$ protocol layer. A normalized one-act continuum interface forces the unique cost $J(x)=(x+x^{-1})/2-1$, is necessary and sufficient as calibration datum, and closes the calibration gap; the discrete rational carrier alone does not force the unit.

background

Primitive recognition calculus separates a discrete rational carrier from a continuum protocol layer $\mathbb{R}_\delta$. Cost members live on positive ratios; the classical RS cost is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced uniquely under the Recognition Composition Law in the T5 step of the forcing chain.

This module works at the continuum interface. One-act log-curvature is the second derivative of the cost member (with unit $c$) evaluated at the limit ratio $t=0$. That quantity is intrinsically continuum: second derivatives are not native to the discrete carrier. The imported calibration-target module supplies the target shape that a successful continuum calibration must hit.

Sibling material introduces a normalized one-act interface structure, a canonical interface, and the claim that a single continuum act is the right calibration datum. The contrast theorem is that discreteness alone does not force the unit scale.

proof idea

Definition layer first: one-act curvature as the $t=0$ second derivative, with an equality lemma tying the abstract name to that derivative. Forcing lemmas then show the unit is recovered from one continuum act, while a parallel negative result shows the discrete carrier does not force the unit. Calibration is identified with one continuum act.

A normalized one-act interface structure is introduced; lemmas prove it forces $J$, that the calibration datum is necessary and sufficient, and that the canonical interface closes the calibration gap. Overall shape is definition-plus-forcing, not a single deep induction.

why it matters in Recognition Science

Closes the continuum side of PRC calibration: without a one-act real interface, the discrete skeleton cannot pin the unit or force $J$. That is the local counterpart of T5 J-uniqueness, specialized to the $\mathbb{R}_\delta$ protocol rather than the abstract functional equation alone.

Four downstream modules import it: DeltaNativeAnalysis and DeltaNativeStrongClosure (native $\delta$-layer consequences), ObjecthoodRegistry (what counts as an object once calibrated), and PhysicalOneActCalibration (physical reading of the one-act datum). Parent use is therefore both analytic closure in the delta calculus and the bridge into physical one-act calibration.

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)