right_distrib
plain-language theorem explainer
Right distributivity of multiplication over addition on PRC integers: (a+b)·c = a·c + b·c. Cited by the PRC rational-field certificate, GoldenInt component lemmas, and Φ-ring constructions that need ℤ-like arithmetic on signed-orbit classes. Proof is a short injectivity transfer: push both sides through the verifier map toInt and invoke ordinary Int.add_mul.
Claim. For all PRC integers $a,b,c$ (signed-orbit quotient classes), multiplication is right-distributive over addition: $(a+b)\cdot c = a\cdot c + b\cdot c$.
background
PRCInt is the Recognition-native integer type: the quotient of signed δ-orbits by the internal balanced-length relation (K4.8). Addition and multiplication are defined on representatives and descend to the quotient; the verifier display toInt : PRCInt → ℤ is the bridge that recovers ordinary integer arithmetic.
The surrounding module builds integer and rational structure from primitive recognition calculus (orbits and orbit arithmetic), not from Mathlib's ℤ as a primitive. Distributivity is one of the ring axioms that must be re-proved on this quotient before rationals and Φ-ladder coefficients can be certified.
Upstream, multiplication and addition on the underlying orbit/LogicNat layers already match Nat/Int under their display maps (e.g. recovery theorems such as toNat_mul). Right distributivity here is the corresponding statement after signing and quotienting.
proof idea
One short tactic proof. Apply injectivity of the verifier map toInt so it suffices to check equality after display into ℤ. Then simp with Mathlib's Int.add_mul, which is ordinary right distributivity on ℤ. The simp set unfolds toInt on add and mul so both sides become the same Int expression.
why it matters
This is a structural ring axiom for PRCInt. Downstream it is re-exported as right_distrib' on PRCRat and packed into RationalFieldCertificate / rational_field_certificate, which certify that the PRC rational quotient carries field arithmetic. It is also consumed by GoldenInt multiplication component lemmas (mul_b) and by PhiInt (elements a + bφ with a,b ∈ ℤ), i.e. the integer coefficient ring for the φ-ladder.
In the forcing chain this sits under foundation arithmetic that later supports T6 (φ as self-similar fixed point) and mass/yardstick constructions on the φ-ladder. Without right distributivity, the rational and golden-integer layers cannot honestly claim ring structure from recognition orbits alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.