canonicalRecognitionCostSystem_domain
plain-language theorem explainer
The canonical recognition cost system is defined over the positive real numbers as its state space. Researchers building cost algebras or applying the Recognition Composition Law reference this when fixing the domain for J-cost calculations. The proof is a one-line reflexivity that follows directly from the definition of PositiveDomain.
Claim. The ambient domain of recognition cost systems coincides with the positive reals: the set of all $r$ in the reals such that $r > 0$.
background
PositiveDomain is the ambient domain of recognition cost systems, consisting exactly of the positive real numbers. A recognition cost system packages a ratio cost, a conservation functional, and a finite window length. The module imports Cost, FunctionalEquation, and FunctionalEquationAczel, placing the result in the setting where costs are induced by multiplicative recognizers and observer forcing events.
proof idea
The proof is a one-line reflexivity that matches the definition of PositiveDomain directly to the open interval of positive reals.
why it matters
This equality fixes the state space for the cost algebra, enabling later use of the Recognition Composition Law and J-uniqueness from the forcing chain. It supplies the common domain for canonical objects in Gap45 and Navier-Stokes modules. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.