IndisputableMonolith.Information.JCostNecessity
This module axiomatizes the Recognition Information Cost as a function F on positive reals obeying symmetry, zero minimum at unity, and strict convexity. Information theorists and Recognition Science modelers cite it to ground thermodynamic cost in recognition symmetry before deriving J-cost uniqueness. The module is purely definitional, importing convexity from Cost.Convexity with no internal proofs.
claimA Recognition Information Cost is a function $F:\mathbb{R}_+\to\mathbb{R}$ satisfying $F(x)=F(1/x)$, $F(1)=0$, and strict convexity on $\mathbb{R}_+$.
background
The module resides in the Information domain and imports Cost together with Cost.Convexity. The latter establishes that $J\log(t)=\cosh t-1$ is strictly convex on $\mathbb{R}$ and that $J\cost(x)=\frac12(x+x^{-1})-1$ is strictly convex on $\mathbb{R}_+$, results described as foundational for uniqueness theorem T5.
The supplied doc-comment states the three required properties verbatim: symmetry (bi-directional recognition), minimum zero at balance, and strict convexity (unique stable equilibrium). These axioms prepare the ground for the parent Information module that aggregates MDL and oriented exp-log constructions.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The definition supplies the axiomatic base that the downstream Information module aggregates into its information-theoretic and thermodynamic foundation, explicitly feeding CompressionPrior and EMLFromRecognition. It directly supports the J-uniqueness step T5 in the forcing chain by codifying the minimal conditions any admissible cost must obey.
scope and limits
- Does not prove existence of a function meeting the three axioms.
- Does not derive the explicit J-cost formula (handled by siblings).
- Does not extend the axioms to vector or multi-variable costs.
- Does not link the axioms to numerical constants such as alpha or G.