one_mul'
plain-language theorem explainer
The theorem establishes that the multiplicative identity acts as a left unit on every element of the quotient field LogicRat built from LogicInt. Researchers verifying field axioms in logic-derived number systems would cite it during construction of the rational layer. The proof reduces the claim to the corresponding identity in Mathlib's Rat by applying the transfer map and the preservation theorems for multiplication and the unit, then normalizes with the ring tactic.
Claim. For every $a$ in the field of fractions LogicRat of LogicInt, the identity element satisfies $1 · a = a$.
background
LogicRat is the quotient of PreRat by the equivalence relation setoid, forming the field of fractions of LogicInt. The module RationalsFromLogic constructs these rationals after IntegersFromLogic supplies LogicInt, with the overall goal of building reals from logical primitives. The transfer theorem eq_iff_toRat_eq states that equality of LogicRat elements is equivalent to equality of their images under toRat in Mathlib's Rat. The maps toRat_mul and toRat_one record that multiplication and the unit are preserved under this transport.
proof idea
The proof is a short tactic sequence. It rewrites the goal with eq_iff_toRat_eq, substitutes the images under toRat_mul and toRat_one to reach the identity 1 * toRat a = toRat a in Rat, and finishes with the ring tactic.
why it matters
This lemma supplies the left-unit property required by the integer and real analogues that cite it. It forms part of the algebraic scaffolding that supports the Recognition Science forcing chain (T0-T8) and the Recognition Composition Law by ensuring the rational field behaves as expected before constants such as phi and the eight-tick octave are introduced. The parallel statements in IntegersFromLogic and RealsFromLogic follow the same transport pattern.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.