rational_contains_jcost_domain
plain-language theorem explainer
The declaration confirms that the rational numbers contain the positive domain required for the J-cost function by showing 1 is positive in ℚ. Number theorists or Recognition Science modelers would reference this when embedding the J-cost into the rational system. Its proof reduces immediately to a numerical check via norm_num.
Claim. The inequality $1 > 0$ holds in the field of rational numbers.
background
In the Recognition Science framework the five number systems correspond to recognition depths: ℕ for discrete counts, ℤ for signed differences, ℚ for rational recognition ratios where the J-cost is defined, ℝ for continuous fields, and ℂ for amplitudes and phases. The J-cost function is defined on ℝ⁺, a subset that must sit inside the rationals for the model to proceed. This theorem supplies the required positivity fact for that containment.
proof idea
The proof is a one-line wrapper that applies norm_num to verify the positivity of 1 in ℚ.
why it matters
This result populates the rational_pos field inside the NumberSystemCert definition, which certifies that all five number systems are present as required by configDim D = 5. It anchors the J-cost domain inside the rational recognition ratios, matching the module description of ℚ as the system where J is defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.