costAlgPlusInitial
plain-language theorem explainer
The definition supplies the canonical object in the positive cost algebra category by fixing its cost parameter to exactly 1. Researchers working on initiality results in Recognition Science cite this object as the source for all order-preserving morphisms. The construction proceeds by direct record definition with positivity verified numerically.
Claim. The initial object in the category of positive-parameter cost families is the family with cost parameter equal to 1.
background
In the RecognitionCategory module, objects of the positive cost algebra category are positive-parameter cost families F_κ for κ > 0; this selects the order-preserving branch, excluding the negative branch that reverses order. Each such object carries a cost function induced by the multiplicative recognizer on positive ratios. The upstream canonical arithmetic object supplies the realization-independent Peano content realized here, while the cost of recognition events is identified with J-cost.
proof idea
The definition constructs the record by setting the parameter field to 1. The positivity constraint is discharged by a direct numeric normalization tactic.
why it matters
This object serves as the source for the initiality theorem establishing that the κ = 1 object is initial in the positive cost algebra category, described as the paper's crown-jewel result. It is also used to equate the attached cost with the canonical J-cost. In the Recognition Science framework this anchors the algebra to J-uniqueness and the Recognition Composition Law, supplying the base for subsequent phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.