equivRat
plain-language theorem explainer
This definition supplies an explicit equivalence between the field of fractions built from logic integers and the standard rationals. Researchers formalizing the Recognition Science base layer would cite it to move statements about rational arithmetic between the native construction and conventional libraries. The construction is a direct definition of the equivalence structure that names the forward map, its inverse, and the two round-trip lemmas already established in the module.
Claim. The field of fractions of the logic integers is equivalent to the standard rationals via the map that sends each quotient class to its recovered rational value, with the inverse embedding a standard rational by taking its numerator and denominator as logic integers.
background
LogicRat is the quotient of PreRat pairs under the equivalence ratRel, yielding the field of fractions over LogicInt. The module RationalsFromLogic constructs these rationals directly from the integers obtained in the preceding IntegersFromLogic layer. Upstream, fromRat embeds a standard rational into the quotient while fromRat_toRat proves that the round trip recovers every original class, serving as the key injectivity result for the transport.
proof idea
The definition assembles the equivalence structure by setting the forward function to the existing toRat map, the inverse function to fromRat, and the left and right inverse proofs to the already-proved round-trip theorems fromRat_toRat and toRat_fromRat.
why it matters
The equivalence closes the transport API between the logic-derived rationals and Mathlib's standard rationals, allowing theorems proved inside the Recognition Science foundation to be used in conventional arithmetic. It supports downstream structures that rely on rational arithmetic, such as those appearing in NucleosynthesisTiers and PhiForcingDerived. No open scaffolding questions are resolved here; the declaration simply records the bijection once the round-trip lemmas exist.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.