unit_group_certificate
plain-language theorem explainer
Packages the unit-residue surface into a single certificate: residues coprime to the modulus form a multiplicative monoid closed under powers, with 1 as unit. Factorization and character-theory arguments cite it when they need the unit group of residues. The proof is a four-field structure instance wiring existing coprimality lemmas.
Claim. There is a unit-group certificate asserting: for distinction naturals $N,a$, the unit-residue predicate on $(N,a)$ holds if and only if $a$ and $N$ are coprime as ordinary naturals; the multiplicative unit is always a unit residue; unit residues are closed under multiplication; and if $a$ is a unit residue mod $N$ then $a^k$ remains coprime to $N$ for every $k\in\mathbb{N}$.
background
In the Primitive Recognition Calculus factorization layer, residues of distinction naturals are tracked relative to a modulus $N$. A residue is called a unit residue when it is invertible in the residue monoid, which here is identified with ordinary coprimality: unitResidue N a means $\mathrm{gcd}(a,N)=1$ after forgetting to Nat.
The structure UnitGroupCertificate is the Prop-level bundle of that identification plus the monoid axioms needed downstream: the unit is a unit residue, products of unit residues are unit residues, and powers of unit residues stay coprime to the modulus. Upstream lemmas already prove each clause separately via Nat.Coprime facts (coprime_one_left, Coprime.mul_left, Coprime.pow_left) after unfolding the residue predicate.
This sits under the factorization module that feeds the master delta-factorization character-theory certificate.
proof idea
Tactic-mode structure instance. Each field is discharged by naming the corresponding lemma:
unit_displayis exactlyunitResidue_iff_nat_coprime(unfold pluscoprime_iff_nat_coprime).one_is_unitisunitResidue_one(reduce toNat.coprime_one_left).mul_closedintros $N,a,b$ and hypotheses, then appliesunitResidue_mul_closed.pow_closed_displayintros and appliesunitResidue_pow_closed. No new arithmetic is proved here; it is pure packaging.
why it matters
The master certificate delta_factorization_character_theory_certificate requires a unit_group field and fills it with this theorem, alongside chart-transition, residue-orbit, and period-spectrum certificates. Without a certified unit-residue monoid, character sums and orbit period arguments on the factorization surface lack their multiplicative domain.
In the broader Recognition foundation this is scaffolding for the discrete residue geometry that later supports forcing-chain bookkeeping (octave ticks, ladder rungs), not a physics claim by itself. It closes the unit-group slot of the factorization master certificate so character-theoretic delta identities can be stated against a proved monoid of units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.