CostRequirements
plain-language theorem explainer
The cost requirements structure specifies the minimal axioms for an admissible cost function F on the positive reals: invariance under inversion and vanishing at the unit point. Researchers deriving J-cost expressions within Recognition Science cite this when validating candidate functions such as the logarithmic gap map. The declaration consists of a direct structure definition carrying no proof obligations.
Claim. A map $F:ℝ→ℝ$ meets the cost requirements when $F(x)=F(x^{-1})$ for every $x>0$ and $F(1)=0$.
background
The Cost module packages the symmetry and normalization conditions demanded of any cost function F. These axioms originate in the J-cost core and are satisfied by the generating functional $F(z)=log(1+z/φ)$ from the Pipelines module. The symmetry property mirrors the J-uniqueness relation in the forcing chain while the unit condition fixes the zero point for phi-ladder mass formulas.
proof idea
The declaration is a structure definition that directly encodes the two field requirements; it carries no proof body and serves as a type for later theorems to assume.
why it matters
This structure supplies the interface referenced by the J-cost core to define admissible cost maps. It underpins derivations of further properties such as non-negativity and averaging agreement, feeding into the Recognition Science mass formula on the phi-ladder. It aligns with the recognition composition law and the T5 J-uniqueness step in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.