PositiveDomain
plain-language theorem explainer
PositiveDomain sets the state space for recognition cost systems to the positive reals. Researchers on cost composition or canonical systems cite it when verifying domain consistency for J-cost derivations. The declaration is a direct one-line abbreviation to the open interval (0, ∞).
Claim. The ambient domain of recognition cost systems is the open interval of positive real numbers: $PositiveDomain := (0, ∞)$.
background
Recognition cost systems package a ratio cost, conservation functional, and finite window length, all operating on positive ratios. Upstream results define cost via Jcost on recognition events and derivedCost on multiplicative recognizer comparators, with the J function satisfying the Recognition Composition Law on positive reals. The module imports establish this domain as the setting for algebraic identities in CostAlgebra.
proof idea
The definition is a one-line abbreviation that directly equates PositiveDomain to Set.Ioi 0.
why it matters
PositiveDomain feeds the canonicalRecognitionCostSystem_domain theorem, which confirms the domain for the canonical system and inherits balance. It supplies the required state space in the algebra layer, consistent with J-uniqueness and the Recognition Composition Law from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.