Pith. sign in
module module high

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationIndependence

show as:
view Lean formalization →

Defines the one-parameter cost gauge family $C_c(x)=\frac12(x^c+x^{-c})-1$ in multiplicative coordinates, with $C_1=J$. Records algebraic, continuity, and reciprocal-cost properties of the family, and proves that the cost laws alone do not force the calibration unit $c=1$. Cited by anyone tracking T5 uniqueness versus PRC calibration choice.

claimFor real $c$ and $x>0$, set $C_c(x)=\frac{1}{2}(x^{c}+x^{-c})-1$ (real powers). Then $C_1=J$, each $C_c$ meets the reciprocal-cost axioms, and the cost functional equations do not by themselves force the calibration unit $c=1$.

background

Recognition Science forces a unique cost $J$ on ratios via the T5 uniqueness theorem: $J(x)=\frac12(x+x^{-1})-1=\cosh(\log x)-1$, characterized by the Recognition Composition Law and regularity. The present module works one step upstream of that uniqueness, in the Primitive Recognition Calculus calibration layer.

It introduces the $\delta$-forced gauge family in multiplicative coordinates, $C_c(x)=\frac12(x^c+x^{-c})-1$ via real exponentiation. The $c=1$ member is exactly $J$. Sibling facts record the cosh form $C_c(x)=\cosh(c\log x)-1$, unit value at $x=1$, symmetry under $x\mapsto x^{-1}$, continuity on $(0,\infty)$, injectivity in the scale, and the reciprocal-cost package.

Upstream imports are the Cost API, the FunctionalEquation helpers used in the T5 proof, and the PRC calibration target module that states what a calibrated cost is supposed to hit.

proof idea

Definition-first module. The family is introduced as a plain definition; identities such as the cosh rewrite, unit value, symmetry, and the addition formula are short algebraic reductions from Real.rpow and hyperbolic trig. Membership in the cost-requirements and reciprocal-cost structures is checked by discharging each field of those structures. The headline independence claim is a negative existence/non-uniqueness argument: the same cost laws are satisfied for a continuum of $c$, so they do not pin the calibration unit to $1$.

why it matters in Recognition Science

Separates two layers that are easy to conflate in the forcing chain. T5 uniqueness fixes the functional form of $J$ once a calibration (the unit of the exponent) is chosen; this module shows that the bare cost laws and reciprocal structure still leave a one-parameter gauge free. That is exactly the content of the sibling calibration_unit_not_forced_by_cost_laws.

In the PRC stack, calibration must therefore come from an independent target (imported from PRCCalibrationTarget), not from the cost axioms alone. Downstream consumers of T5, the eight-tick octave, and dimension forcing can then treat $c=1$ as a calibrated choice rather than a pure cost-law consequence. No used-by edges are recorded yet; the module is a foundation leaf feeding the calibration narrative.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (16)