mul
plain-language theorem explainer
Defines the binary product of two unit residues modulo a fixed distinction modulus N: the product residue carries value equal to the product of the two values and inherits the unit (coprimality) witness. Anyone assembling the multiplicative monoid or group of residues coprime to N cites this constructor. The body is a structure instance that multiplies the underlying values and applies the already-proved closure lemma.
Claim. Let $N$ be a distinction modulus. If $u$ and $v$ are unit residues modulo $N$ (residues whose underlying values are coprime to $N$), then their product is the unit residue whose value is the product of the two underlying values.
background
In the factorization layer of the primitive recognition calculus, residues live in a distinction-nat type. A residue is a unit residue when it satisfies the unit-residue predicate, equivalently when its underlying natural is coprime to the modulus $N$. The structure UnitResidue N packages a value together with that unit witness and is the carrier for finite multiplicative character theory on residues.
Closure of the unit predicate under multiplication is already available: if $a$ and $b$ are unit residues modulo $N$, then so is $a\cdot b$. That fact is proved by rewriting to natural coprimality and invoking the standard fact that the product of two integers coprime to $N$ remains coprime to $N$. The present definition turns that closure into an internal binary operation on the structure.
proof idea
One-line structure constructor. The value field is set to the product of the two input values. The unit witness is obtained by applying the upstream closure theorem unitResidue_mul_closed to the two input witnesses. No further rewriting or case analysis is required.
why it matters
This is the multiplication half of the monoid (and later group) structure on unit residues. Downstream siblings such as the identity unit residue, value projections, and the unit-group certificate package sit on the same carrier; without an internal product there is no multiplicative character theory on the residue side of the factorization calculus. In the broader Recognition Science foundation this is scaffolding for discrete multiplicative structure that later interfaces with the eight-tick octave and phi-ladder bookkeeping, not a forcing-chain step itself. No parent theorem currently lists this definition as a direct dependency in the supplied graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.