cost_algebra_unique_aczel
plain-language theorem explainer
Any cost function packaged inside a CostAlgebraData structure, when calibrated so the second derivative of its exponential reparametrization at zero equals one and continuous on the positive reals, must coincide with the J-cost function on all positive reals. Researchers deriving unique physical cost functions from the recognition composition law cite this as the clean T5 uniqueness result. The proof extracts the reciprocal, normalization, composition-law, and calibration properties from the algebra data and invokes the Aczél-based uniqueness,
Claim. Let $C$ be a CostAlgebraData structure whose cost function satisfies the recognition composition law, vanishes at the multiplicative identity, is symmetric under reciprocals, and is non-negative. If the second derivative at zero of $tmapsto C.cost(e^t)$ equals one and the cost function is continuous on the positive reals, then $C.cost(x)=J(x)$ for all $x>0$, where $J(x)=frac12(x+x^{-1})-1$.
background
CostAlgebraData is the fundamental algebraic object of Recognition Science: a structure on the positive reals whose carrier is equipped with multiplication, a cost map obeying the Recognition Composition Law, normalization cost(1)=0, reciprocal symmetry, and non-negativity. The J-cost is the explicit function J(x)=½(x+x⁻¹)−1 that satisfies the same law. The module imports the Aczél functional-equation machinery; the upstream washburn_uniqueness_aczel lemma supplies the uniqueness statement under the extracted axioms plus continuity.
proof idea
The tactic proof first builds IsReciprocalCost, IsNormalized, SatisfiesCompositionLaw, and IsCalibrated by simpa on the corresponding fields of CostAlgebraData. It then applies washburn_uniqueness_aczel directly to these four properties together with the supplied continuity hypothesis, reducing the goal to the pointwise equality with J.
why it matters
This is the clean form of T5 (J-uniqueness) in the forcing chain T0–T8. It removes extra regularity parameters present in the sibling cost_algebra_unique and feeds directly into the self-similar fixed-point step T6 and the derivation of the eight-tick octave. The result underpins the RS-native constants G=phi^5/pi and the alpha band (137.030,137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.