PublicCostLayer
plain-language theorem explainer
Recognition Science packages its cost functional properties for the dimensional constraints rebuttal via the PublicCostLayer structure. The structure asserts that admissible functionals coincide with the canonical J on positives under primitive hypotheses and Aczel regularity, that the log form is cosh t minus one, plus normalization, reciprocity, nonnegativity, unique zero at unity, and defect divergence near zero. Paper authors cite it to access the public interface without confidential imports. The declaration is a structure definition that,
Claim. The public cost layer is the proposition bundle asserting: any admissible cost functional $F$ satisfying the primitive cost hypotheses and Aczel regularity kernel on the shifted $H$ equals the canonical $J$ for all $x>0$; the logarithmic cost satisfies $Jlog(t)=cosh(t)-1$; $J(1)=0$; $J(x)=J(x^{-1})$ for $x>0$; $J(x)geq 0$ for $x>0$; $J(x)=0$ iff $x=1$ for $x>0$; and for every bound $C$ there exists $epsilon>0$ such that the defect exceeds $C$ whenever $0<x<epsilon$.
background
This module packages the public cost-theoretic core for the dimensional constraints rebuttal, exposing only the statements needed in the paper while avoiding confidential imports. Key upstream definitions include the shifted cost $H(x)=J(x)+1=frac12(x+x^{-1})$, which converts the recognition composition law into the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. The logarithmic cost is $Jlog(t)=J(exp t)$. PrimitiveCostHypotheses bundles reciprocity, normalization, composition-law satisfaction, calibration, and continuity on the positive reals. AczelRegularityKernel supplies the smoothness and ODE hypotheses extracted from the Aczel classification.
proof idea
As a structure definition with empty proof body, the declaration simply enumerates the listed properties. It draws the uniqueness clause directly from the primitive hypotheses and Aczel kernel structures, the closed form from the Jlog definition, and the remaining algebraic properties from the Cost and CostAlgebra modules.
why it matters
This structure supplies the compact public cost interface required by the dimensional constraints rebuttal. It is instantiated by the downstream theorem public_cost_layer, which assembles the fields using lemmas such as Jlog_as_cosh and Jcost_unit0. The declaration fills the cost-layer slot in the rebuttal section and connects to the T5 J-uniqueness step of the forcing chain without exposing internal scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.