left_distrib
plain-language theorem explainer
Left distributivity of multiplication over addition on PRC integers: signed-orbit quotient classes that display into ℤ. Anyone assembling the ring laws on PRCInt, or lifting them to PRC rationals and the rational-field certificate, cites this. The proof is a two-line reduction through the injective toInt display onto Mathlib's Int.mul_add.
Claim. For all PRC integers $a,b,c$ (quotient classes of signed orbits under the balanced-length relation), $a\cdot(b+c)=a\cdot b+a\cdot c$.
background
PRC integers are the K4.8 construction: quotient of signed orbits by the internal balanced-length setoid. Each class has a verifier display toInt into ordinary ℤ; injectivity of that display is the standard way to discharge equalities on the quotient without choosing representatives.
Addition and multiplication on signed-orbit representatives are defined componentwise from the underlying distinction naturals, and both commute with the integer display: (add a b).toInt = a.toInt + b.toInt and (mul a b).toInt = a.toInt * b.toInt. Those transport lemmas sit on top of the ArithmeticFromLogic layer, where LogicNat already satisfies mul_add and recovers ordinary Nat multiplication under toNat.
The local module builds the integer and rational layers of the Primitive Recognition Calculus from orbit arithmetic, staying choice-free wherever possible (the cross-equality hub for rationals routes through ℤ rather than Mathlib ℚ).
proof idea
Term-mode, two steps. Apply injectivity of the integer display on PRCInt, so it suffices to check equality after toInt. Then simp with Mathlib's Int.mul_add, using the already-proved transport lemmas add_toInt and mul_toInt (and the corresponding quotient constructors) so that both sides become the same integer expression toInt(a) * (toInt(b) + toInt(c)). No induction on the quotient itself is needed.
why it matters
This is one of the ring axioms required before PRC integers can support the downstream rational field and the φ-ladder algebra. It is re-exported almost verbatim as left_distrib' on PRCRat and is listed among the fields of RationalFieldCertificate / rational_field_certificate, which package the field laws for the Primitive Recognition Calculus kernel.
Upstream of the φ-ring, the same distributivity is consumed when building PhiInt (pairs $(a,b)$ for $a+b\varphi$) and the GoldenInt component lemmas such as mul_b. Those structures sit on the path toward the mass ladder and the forcing chain's self-similar fixed point φ (T6). The kernel first-pass certificate also depends on this layer being inhabited, so the lemma is part of closing the arithmetic substrate rather than a physics claim in its own right.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.