IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCCalibrationIndependence
Defines the one-parameter cost gauge family costLambda(c,x) = ½(x^c + x^{-c}) − 1 on the positive reals, with c = 1 recovering the canonical J-cost. Establishes that every member satisfies the Recognition cost axioms (symmetry, unit zero, continuity, reciprocity) and the cosh-addition identity, yet the unit scale c is not forced by those laws alone. Cited by anyone separating T5 uniqueness of the functional form from calibration of the multiplicative unit.
claimFor each real $c$ and $x > 0$, set $\Lambda_c(x) := \frac12\bigl(x^c + x^{-c}\bigr) - 1$ (real powers). Then $\Lambda_1 = J$, each $\Lambda_c$ obeys the cost axioms and the reciprocal-cost identity, and the cost laws alone do not force $c = 1$.
background
Recognition Science forces a unique cost functional $J$ on ratios via the Recognition Composition Law and regularity (T5). In multiplicative coordinates the natural family of gauges is $\Lambda_c(x) = \frac12(x^c + x^{-c}) - 1$, equivalently $\cosh(c\log x) - 1$. The member $c = 1$ is the standard $J$-cost used throughout the monolith.
The module sits inside Primitive Recognition Calculus and imports the Cost library together with the T5 functional-equation helpers. The companion target module supplies the calibration interface that this family is measured against. The point is to exhibit an explicit continuum of costs that all satisfy the same algebraic and analytic requirements, so that any later uniqueness claim must invoke an extra normalization (the unit of the multiplicative coordinate) rather than the cost laws alone.
proof idea
The module is largely definitional plus elementary real-analysis lemmas. costLambda is introduced via Real.rpow; costLambda_eq_cosh rewrites it as cosh(c log x) − 1. Symmetry, vanishing at 1, continuity on (0,∞), injectivity, and the reciprocal-cost predicate are discharged by direct calculation or Mathlib cosh identities. costLambda_one_eq_Jcost is the specialization c = 1. The key negative statement calibration_unit_not_forced_by_cost_laws exhibits distinct c yielding distinct gauges that still meet CostRequirements, showing the unit is free once the functional form is fixed.
why it matters in Recognition Science
T5 uniqueness fixes the shape of J up to the choice of multiplicative unit. This module makes that residual freedom concrete: the whole family Λ_c satisfies the cost axioms and the RCL-compatible addition identity, yet only an external calibration (the PRC calibration target) pins c = 1. Downstream forcing-chain and mass-ladder arguments that quote “the” J-cost therefore rest on that calibration step rather than on the functional equation alone. With no further used_by edges recorded yet, the module is the local witness that cost-law uniqueness and unit calibration are separate obligations inside the foundation layer.
scope and limits
- Does not prove T5 uniqueness of J; only exhibits the residual gauge family.
- Does not force c = 1 from cost axioms alone; that is the explicit negative claim.
- Does not address additive-coordinate gauges or discrete tick structure.
- Does not derive physical constants or the mass ladder from Λ_c.
- Does not claim every reciprocal cost arises as some Λ_c.
depends on (3)
declarations in this module (16)
-
def
costLambda -
theorem
costLambda_eq_cosh -
theorem
costLambda_unit0 -
theorem
costLambda_symm -
theorem
costLambda_isCostRequirements -
theorem
costLambda_continuousOn -
theorem
costLambda_one_eq_Jcost -
theorem
costLambda_inj -
theorem
calibration_unit_not_forced_by_cost_laws -
theorem
G_costLambda -
theorem
costLambda_coshAddIdentity -
theorem
costLambda_isReciprocalCost -
theorem
costLambda_isNormalized -
theorem
costLambda_satisfiesCompositionLaw -
theorem
costLambda_isCalibrated_iff -
theorem
calibration_is_the_only_hypothesis_pinning_J