costAlgKappaInitial_cost_eq_J
plain-language theorem explainer
The cost function attached to the canonical initial object of the CostAlg category coincides with the J-cost on positive reals. Researchers working on Recognition Science cost algebras cite this to confirm that the κ=1 calibration recovers the fundamental J function from the forcing chain. The proof is a one-line wrapper that applies the prior result equating the κ=1 cost family to J.
Claim. Let $C_1$ be the initial object in the CostAlg category with parameter $κ=1$. Then the associated cost function satisfies $C_1(x) = J(x)$ for every $x>0$, where $J$ is the canonical cost function obeying the Recognition Composition Law.
background
The CostAlg category is built from objects that are positive-parameter cost families $F_κ$ equipped with morphisms that intertwine costs via scaling exponents. The initial object is defined as the calibrated family with $κ=1$. This setting draws on the multiplicative recognizer construction, where cost is the derived comparator on positive ratios, and on the LedgerFactorization structure that calibrates J itself.
proof idea
One-line wrapper that applies the theorem establishing that the κ=1 cost family recovers J on positive reals, instantiated at the given positive argument.
why it matters
This equality anchors the initial object of the CostAlg category to the J-cost, which is the unique function satisfying J-uniqueness (T5) in the forcing chain. It directly enables the subsequent classification of morphisms out of the initial object into the positive and negative branches with exponents ±1/κ. The result therefore links the algebraic category construction to the Recognition Composition Law and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.