CostSelectionPackage
plain-language theorem explainer
Packages the continuous uniqueness claim for the recognition cost: any reciprocal, normalized, RCL-satisfying, calibrated cost continuous on the positive reals equals J(x)=(x+x^{-1})/2-1, under the Aczél smoothness package. Cited by the public dual spine certificate and by cost-selection audits that refuse a deltaOnly tag. The structure is a Prop bundle; inhabitation is discharged elsewhere by the law-of-logic uniqueness theorem.
Claim. A cost-selection package asserts: for every $F:\mathbb{R}\to\mathbb{R}$ meeting the Aczél smoothness package, if $F$ is a reciprocal cost, $F(1)=0$, $F$ obeys the recognition composition law, $F$ is calibrated ($G''(0)=1$ for $G(t)=F(e^t)$), and $F$ is continuous on $(0,\infty)$, then $F(x)=J(x)$ for all $x>0$, where $J(x)=(x+x^{-1})/2-1$.
background
PublicSpine is the public dual of UnifiedForcingChain: a δ-stratified map of what is forced, keeping UFC names as certificate witnesses. Cost form is separated from unit calibration; uniqueness of the cost is a purchase under continuum and gauge hypotheses, not a free deltaOnly theorem.
The target cost is $J(x)=(x+x^{-1})/2-1$ (also $\cosh(\log x)-1$), the T5 landmark. Hypotheses are the standard RCL package: reciprocity under $x\mapsto x^{-1}$, normalization $F(1)=0$, the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ (here for general $F$), and calibration $\lim_{t\to 0} 2F(e^t)/t^2=1$. Continuity on $(0,\infty)$ plus AczélSmoothnessPackage (continuous d'Alembert solutions are $C^\infty$) close the analytic class.
The doc-comment tags the honest strength at least traceClosure (continuum carrier) plus the calibration gauge; never deltaOnly.
proof idea
No proof body: this is a structure-as-Prop bundling a single field j_unique. Inhabitation is supplied by cost_selection_holds, a one-line wrapper that fills the field with law_of_logic_forces_jcost applied to an arbitrary $F$ under the listed hypotheses. The structure itself only names the selection claim.
why it matters
Fills the cost-form-vs-selection slot on the public dual spine. Downstream, cost_selection_holds tags the package StrengthTag.traceClosure, and PublicSpineCert records it beside the δ-only tower, continuum purchase, φ-from-ι, and circle $H_1$. That matches the module contract: papers citing "what is forced" use this surface, not raw UFC names.
Framework landmark: T5 J-uniqueness under the Recognition Composition Law. The package makes explicit that continuous uniqueness needs reciprocity, normalization, RCL, calibration, continuity, and Aczél smoothness; calibration is a gauge, not free. Downstream PRC work uses the same selection language when refuting zero-orbit uniqueness without calibration (zero-flat countermodel).
Does not reopen FOP or the unique-cost paper; Lean-map honesty only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.