one_mul
plain-language theorem explainer
Left multiplication by the multiplicative unit is the identity on PRC integers (signed-orbit quotient classes). Anyone assembling a monoid or ring structure on the primitive recognition calculus integers cites this unit law. The proof injects both sides into ℤ via the display map and discharges the equality by simplification against the integer unit law.
Claim. For every PRC integer $a$ (a balanced-length quotient class of signed orbits), left multiplication by the unit satisfies $1 \cdot a = a$.
background
PRC integers are the K4.8 construction: quotient classes of signed orbits under the internal balanced-length relation. The display map into ordinary integers is a downstream theorem, not part of the definition; equality of classes is therefore often proved by showing the displays agree and invoking injectivity of that map.
Multiplication on signed orbits is defined componentwise so that the display intertwines it with ordinary integer multiplication (mul_toInt). The unit is the class whose numerator display is $1$ and whose denominator display is $1$ in the natural numbers recovered from logic arithmetic. Upstream, ArithmeticFromLogic.one_mul already gives the unit law on LogicNat (succ zero * n = n), and the recovery theorem toNat_mul ensures that display agrees with Nat multiplication.
The local module builds integer and rational layers of the primitive recognition calculus without classical choice on the integer hub: cross-multiplication characterizations stay in ℤ and depend only on propext and Quot.sound.
proof idea
One short tactic proof. Apply injectivity of the integer display (toInt_injective) to reduce mul one a = a to an equality in ℤ. A single simp then rewrites the left-hand display via mul_toInt together with the unit numerator/denominator display lemmas (one_num_toInt, one_den_toNat) and the upstream logic-arithmetic unit law, yielding reflexivity on the right-hand display.
why it matters
This is the left unit law for the monoid structure on PRC integers. Downstream it is consumed heavily: CostAlgebra uses it inside level-set classification of the J-cost (J_eq_iff_eq_or_inv) and in the shifted-composition carrier; PhiRing builds ℤ[φ] pairs on top of integer arithmetic; cosmology modules invoke it for B−L fixed-point identities under sphaleron reprocessing (output_BminusL_eq_input), for flow-product conservation after paired events (flowProduct_addEvent), and in eta_B prefactor comparisons. In the Recognition forcing chain it sits under the arithmetic substrate that later supports T5 J-uniqueness and the RCL identities, rather than stating those landmarks itself. No open scaffold remains: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.