H_UniquenessVerified
plain-language theorem explainer
The declaration encodes the hypothesis that any function F satisfying the InformationCost axioms equals the J-cost for positive arguments. Information theorists and Recognition Science modelers cite it when linking recognition axioms to thermodynamic and free-energy bounds. The statement is a direct one-line encoding of the T5 uniqueness result, presented as a scaffold after legacy axioms were removed.
Claim. Let $F : (0,∞) → ℝ$. If $F$ obeys the information-cost axioms (symmetry $F(x) = F(x^{-1})$, minimum $F(1) = 0$, and strict convexity on the positive reals), then $F(x) = J(x)$ for all $x > 0$, where $J$ is the J-cost function.
background
The Information module aggregates recognition-derived information theory and thermodynamics. Its key local definition is InformationCost F, the Prop requiring symmetry under inversion, zero at the balanced state, and strict convexity on positive reals. Upstream T5_uniqueness_complete supplies the calibrated uniqueness theorem under these plus continuity and derivative conditions at unity. J-cost itself arises as the derived cost of multiplicative recognizers and observer-forcing events.
proof idea
One-line definition that directly states the forall. The accompanying comment records removal of a legacy axiom and points to T5_uniqueness_complete for the actual proof. No tactics or reductions are performed inside this declaration.
why it matters
It supplies the uniqueness hypothesis required by the Information Bridge Aggregator, enabling downstream links to Landauer bounds and FEP/KL contacts. The statement realizes the T5 J-uniqueness step of the forcing chain inside the information layer. The module TODO flags the remaining unification task with the full aggregator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.