CostRequirements
plain-language theorem explainer
The structure axiomatizing minimal properties for a cost function F in Recognition Science: invariance under inversion for positive arguments together with normalization to zero at unity. Derivations of J-cost symmetry, non-negativity, and quadratic bounds cite this interface before applying the Recognition Composition Law or phi-ladder mass formulas. It is introduced as a bare structure definition consisting of exactly two fields.
Claim. A function $F:ℝ→ℝ$ satisfies the cost requirements when $F(x)=F(x^{-1})$ for all $x>0$ and $F(1)=0$.
background
The JcostCore module supplies the foundational axioms for cost functions used in Recognition Science derivations. The symmetric field encodes inversion invariance, matching the J-uniqueness relation from the forcing chain where J(x)=(x+x^{-1})/2-1. The unit0 field normalizes the cost at the identity, consistent with the phi-ladder conventions and the eight-tick octave structure.
proof idea
This is the direct definition of the structure, introducing the symmetric field for inversion invariance and the unit0 field for normalization at one. No lemmas or tactics are invoked; the declaration functions as a type-level interface.
why it matters
The structure supplies the contract for all subsequent J-cost lemmas in the Cost module, including symmetry, non-negativity, and small-strain bounds that support mass formulas on the phi-ladder. It aligns with T5 J-uniqueness and prepares applications of the Recognition Composition Law. No open scaffolding remains at this level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.