CostRequirements
plain-language theorem explainer
CostRequirements is a structure that any admissible cost function F from reals to reals must satisfy, namely symmetry under taking reciprocals for positive arguments together with normalization at one. Workers on the J-cost functional in Recognition Science cite this when checking candidate functions against the core axioms. The declaration consists of a bare structure definition with two fields and no further proof content.
Claim. A map $F : ℝ → ℝ$ meets the cost requirements when $F(x) = F(x^{-1})$ for every $x > 0$ and $F(1) = 0$.
background
In the Cost.JcostCore module the structure CostRequirements collects the two axioms imposed on the cost function F. The symmetric field encodes invariance under inversion while unit0 fixes the value at the identity. Upstream results supply concrete realizations of F such as the gap function log(1 + z/phi) from the Pipelines module and the anchor policy in Physics.AnchorPolicy.
proof idea
The declaration is a structure definition that directly introduces the two required fields without any computational reduction or lemma application.
why it matters
This structure is referenced by the CostRequirements declaration in the parent Cost module. It supplies the axiomatic foundation for subsequent Jcost lemmas such as Jcost_symm and Jcost_unit0 listed among the siblings. In the framework it supports the cost composition law derived from the Recognition Composition Law (RCL).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.