InformationCost
plain-language theorem explainer
InformationCost encodes the three axioms required of any recognition-derived cost function on positive reals: inversion symmetry, vanishing at the balanced point, and strict convexity. Workers deriving the J-cost from information principles cite this structure to frame the necessary conditions before invoking the calibrated reciprocal-affine uniqueness theorem. The declaration is a bare structure with no computational content or proof obligations.
Claim. A function $F:ℝ→ℝ$ is an information cost if $F(x)=F(x^{-1})$ for all $x>0$, $F(1)=0$, and $F$ is strictly convex on $(0,∞)$.
background
The module places this definition inside the information-theoretic side of J-cost uniqueness. Upstream results include the reciprocal automorphism on positive ratios from CostAlgebra and the canonical arithmetic objects from ArithmeticOf that ground ratio comparisons. The three fields match the doc-comment requirements exactly: bi-directional recognition symmetry, zero cost for the balanced state, and strict convexity to guarantee a unique equilibrium.
proof idea
The declaration is a structure definition that directly packages the three axioms with no further elaboration or lemmas applied.
why it matters
This structure supplies the hypothesis interface for jcost_is_unique and the verification theorem jcost_satisfies_information_cost. It closes the information-cost side of the J-uniqueness argument in Phase 7.5.1 and feeds H_UniquenessVerified. In the framework it supports the derivation of the phi-ladder constants from recognition symmetry and the T5 J-uniqueness step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.