UnitGroupCertificate
plain-language theorem explainer
Bundles four properties that make the unit-residue surface a multiplicative monoid of residues coprime to the modulus. Factorization and character-theory certificates cite it as the unit-group ledger entry. The structure is pure interface: no proof body; a sibling theorem fills the fields from coprimality lemmas.
Claim. A unit-group certificate is a proposition packing: (i) a residue $a$ is a unit modulo $N$ if and only if $a$ and $N$ are coprime as ordinary naturals; (ii) the multiplicative identity is always a unit residue; (iii) unit residues are closed under multiplication; (iv) if $a$ is a unit residue modulo $N$, then every natural power $a^k$ remains coprime to $N$.
background
In the primitive recognition calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive type with zero and successor, mapped to ordinary Nat by a verifier toNat. Residues live in this orbit language rather than raw naturals.
A residue representative $a$ is declared a unit modulo $N$ when it is $\delta$-coprime to $N$ (unitResidue N a := coprime a N). The certificate asks that this internal notion match classical coprimality after toNat, and that the unit residues form a multiplicative monoid with the expected power behavior.
The module sits in the factorization lane of the foundation stack, importing the residue-orbit layer. The certificate is the unit-group surface that later character-theory and period-spectrum work consume.
proof idea
No proof body: this is a structure ... : Prop interface. The four fields are named hypotheses to be discharged elsewhere. The sibling theorem unit_group_certificate builds an inhabitant by wiring unit_display to unitResidue_iff_nat_coprime, one_is_unit to unitResidue_one, mul_closed to unitResidue_mul_closed, and the power clause to the corresponding Nat-coprimality fact. Treat the structure as a ledger row, not a derivation.
why it matters
Parent consumer is DeltaFactorizationCharacterTheoryCertificate, the current theorem ledger for the factorization character-theory lane; its unit_group field is exactly this certificate, alongside chart transition, residue orbit, period spectrum, and finite multiplicative characters. Without a filled unit-group row, the master factorization certificate cannot close.
In Recognition terms this is arithmetic infrastructure under the primitive recognition calculus: units modulo $N$ are the multiplicative group that characters and period spectra act on. It does not itself invoke the forcing chain (T5–T8), RCL, or $\varphi$-ladder physics; it supplies the monoid of invertible residues those later layers need when factorization is read off distinction orbits.
The concrete inhabitant unit_group_certificate shows the interface is already discharged in-module, so downstream ledgers can cite a proved unit-group surface rather than an open hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.