costAlgKappaInitial
plain-language theorem explainer
The definition costAlgKappaInitial supplies the initial object of the CostAlg category by fixing the parameter at κ = 1. Algebraists working on Recognition Science cost structures cite it as the calibrated base case from which power-map morphisms and J-cost equalities are derived. The construction is a direct record instantiation whose sole positivity obligation is discharged by norm_num.
Claim. The initial object in the CostAlg category is the positive-parameter family with κ = 1, where each object F_κ carries the cost function costFamily(κ) and morphisms are power maps x ↦ x^α satisfying α κ₂ = ± κ₁.
background
Objects of the CostAlg category are structures CostAlgObjKappa consisting of a real parameter κ > 0. Each object is equipped with the cost function costFamily C.κ, which descends from upstream definitions including MultiplicativeRecognizerL4.cost (derived cost of a comparator on positive ratios) and ObserverForcing.cost (cost of a recognition event equals its J-cost). The module RecognitionCategory assembles the full paper-facing category whose morphisms CostAlgHomKappa are power maps obeying the intertwining condition α κ₂ = ± κ₁. This construction sits above the canonical arithmetic object supplied by ArithmeticOf.canonical, which furnishes realization-independent initial content.
proof idea
The definition directly constructs the CostAlgObjKappa record by setting κ := 1 and discharging the field κ_pos via the norm_num tactic. No further lemmas or reductions are invoked.
why it matters
This definition supplies the initial object that feeds CostAlgHomKappa morphisms and the downstream theorem costAlgKappaInitial_cost_eq_J establishing equality with the canonical J-cost. It realizes the calibrated κ = 1 family as the base case in the Recognition cost algebra, anchoring the J-uniqueness step of the forcing chain and the subsequent eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.