Pith. sign in
module module moderate

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationTarget

show as:
view Lean formalization →

Defines the residual gauge freedom in the primitive recognition cost family: the log-curvature of cosh(c·t)−1 at the unit is c², read as a second derivative. Supplies the calibration target and the one-real-parameter torsor of cost gauges. Downstream PRC calibration, independence, chain-bridge, and certificate modules import this target. The development is definitional plus elementary real-analytic identities for curvature and gauge action.

claimFor the one-parameter cost family $C_c(t)=\cosh(c\cdot t)-1$, the log-curvature at the unit $t=0$ equals $c^2$. This $c$ is the residual gauge parameter. The module identifies the calibration unit as a gauge, shows the gauge action is transitive, and exhibits cost freedom as a one-real-parameter torsor; curvature one recovers the canonical $J$-cost.

background

Primitive Recognition Calculus works with cost functionals on a multiplicative line, normalized so the identity has zero cost. The Recognition Composition Law forces the shape $J(x)=\cosh(\log x)-1$ up to gauge; the residual freedom is a real scale in the logarithm.

This module isolates that residual as log-curvature: differentiate $C_c(t)=\cosh(c\cdot t)-1$ twice at $t=0$ to read $c^2$. Sibling material includes injectivity of complex log on the relevant branch, the equivalence of unit curvature with the canonical $J$, and the identification of the $\lambda=1$ cost with $J$.

The local setting is foundation-level gauge bookkeeping before any physical constant is fixed: one real torsor of calibrations, not yet pinned to $\phi$ or the eight-tick chain.

proof idea

Definition-heavy module with short analytic lemmas. logCurvature is the second derivative (or equivalent limit) of the log-parameterized cost at the unit. clog_inj and curvature identities reduce unit-curvature-one to the standard $J$. Gauge lemmas show the calibration unit generates a transitive $\mathbb{R}$-action, so cost freedom is a one-real torsor. No deep forcing; elementary real calculus and group action facts.

why it matters in Recognition Science

Feeds the four PRC modules that import it: DeltaRealCalibration, PRCCalibrationIndependence, PRCChainBridge, and PRCShrunkCertificate. Those layers need a named residual gauge before they can prove calibration independence or shrink certificates along the forcing chain.

In the broader RS picture this sits under T5 $J$-uniqueness: once RCL forces the cosh-log shape, only the log-scale $c$ remains. Later work pins $c$ via self-similarity ($\phi$) and discrete octave structure; this module only exposes the torsor and the curvature readout.

Without a clean calibration target, independence and bridge theorems have nothing canonical to fix against.

scope and limits

used by (4)

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

declarations in this module (7)