costAlgPlusInitial_cost_eq_J
plain-language theorem explainer
The initial object with κ = 1 in CostAlg⁺ carries cost exactly equal to the canonical J-cost on positive reals. Algebraists formalizing Recognition Science cost structures cite this to anchor the initial object to the paper's J. The proof is a one-line wrapper applying the costFamily_one_eq_J lemma.
Claim. For every real $x$ with $0 < x$, the cost function of the canonical object with parameter κ = 1 satisfies cost(x) = J(x), where J is the canonical J-cost on positive reals.
background
The RecognitionCategory module builds CostAlg⁺ as the category whose objects are positive parameters κ > 0 equipped with cost functions from the cost family. The initial object is defined by setting κ := 1. The J-cost is the function recovered precisely at this parameter value, given by J(x) = (x + x^{-1})/2 - 1 for x > 0.
proof idea
The proof is a one-line wrapper that applies the lemma costFamily_one_eq_J to the positivity hypothesis hx.
why it matters
This equality anchors the cost on the initial object and is invoked to show that the initial morphism preserves J in CostAlgPlusHom.fromInitial_preserves_J. It supports the formalization of the initiality of the calibrated κ = 1 object in CostAlg⁺, aligning with the paper's crown-jewel theorem. The result connects to J-uniqueness at T5 in the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.