Uniform Least-Residue Unit-Coset Lift

Abstract

Reduction of a unit coset through a coprime prime extension of the modulus has an exact rational least-residue first moment. Two finite bijections identify retained units and removed prime multiples on native unit groups.

For every modulus n, the unit group is the actual group of invertible elements of Z/nZ, and r denotes the natural-valued ZMod.val. At positive moduli this is the least nonnegative representative. At n greater than one every unit has representative between one and n minus one. Cardinalities are finite carrier cardinalities. All moment and deviation arithmetic below is rational; the integer representative is coerced before subtraction.

Definition 1.1 (Actual finite left cosets).

$$\forall (n:\mathbb{N}),[\mathrm{NeZero}(n)]\forall (K:\mathrm{Subgroup}((\mathbb{Z}/n\mathbb{Z}{)}^{\times })),\forall (c:(\mathbb{Z}/n\mathbb{Z}{)}^{\times }),\mathrm{cosetFinset}(n,K,c)=\{u\in (\mathbb{Z}/n\mathbb{Z}{)}^{\times }\mid c^{-1}u\in K\}$$

Formalization. D5/S3/ArithUnits/MercaCosetFiberLift.cosetFinset (✓ std3).

Source. Repository-derived.

Commentary.

The membership condition is c inverse times u in K, so this is the left coset cK.

Definition 1.2 (Reduction on the actual unit groups).

$$\forall (N:\mathbb{N}),\forall (\ell :\mathbb{N}),\mathrm{reduceUnits}(N,\ell )=\mathrm{unitsMap}(N\mid N\ell )$$

Formalization. D5/S3/ArithUnits/MercaCosetFiberLift.reduceUnits (✓ std3).

Source. Repository-derived.

Commentary.

This multiplicative map is induced by reduction modulo N, using N dividing N ell. Its source is the unit group modulo N ell and its target the unit group modulo N.

Definition 1.3 (The actual reduction preimage).

$$\forall (N:\mathbb{N}),\forall (\ell :\mathbb{N}),[\mathrm{NeZero}(N\ell )]\forall (B:\mathrm{Finset}((\mathbb{Z}/N\mathbb{Z}{)}^{\times })),\mathrm{liftedFinset}(N,\ell ,B)=\{v\in (\mathbb{Z}/N\ell \mathbb{Z}{)}^{\times }\mid \mathrm{reduceUnits}(N,\ell )(v)\in B\}$$

Formalization. D5/S3/ArithUnits/MercaCosetFiberLift.liftedFinset (✓ std3).

Source. Repository-derived.

Commentary.

The lifted finite set contains exactly the units whose reduction belongs to the given set.

Definition 1.4 (The rational least-residue moment).

$$\forall (n:\mathbb{N}),\forall (B:\mathrm{Finset}((\mathbb{Z}/n\mathbb{Z}{)}^{\times })),M_n(B)=\sum _{u\in B}{r}_n(u)\in \mathbb{Q}$$

Formalization. D5/S3/ArithUnits/MercaCosetFiberLift.moment (✓ std3).

Source. Repository-derived.

Commentary.

Each integer representative is coerced into the rationals before summing.

Definition 1.5 (The subgroup-sized rational center).

$$\forall (n:\mathbb{N}),\forall (K:\mathrm{Subgroup}((\mathbb{Z}/n\mathbb{Z}{)}^{\times })),\forall (B:\mathrm{Finset}((\mathbb{Z}/n\mathbb{Z}{)}^{\times })),F_n(K,B)=M_n(B)-\frac{n|K|}{2}$$

Formalization. D5/S3/ArithUnits/MercaCosetFiberLift.deviation (✓ std3).

Source. Repository-derived.

Commentary.

The center uses the cardinality of the subgroup, while the finite set is an explicit argument.

Theorem 1.6 (The rational triangular sum).

$$\forall (ell:\mathbb{N}),(0<ell)\Rightarrow (\sum _{t:\mathrm{Fin}\left(ell\right)}(Fin.val\left(t\right):\mathbb{Q})=\frac{((ell:\mathbb{Q}))\cdot ((ell:\mathbb{Q})-1)}{2})$$

Proof. Machine-checked in Lean as D5/S3/ArithUnits/MercaCosetFiberLift.sum_fin_rat (✓ std3). ∎

Source. Repository-derived.

Commentary.

The rational sum of the representatives of Fin ell is ell times ell minus one divided by two.

Theorem 1.7 (The complete uniform lift theorem).

$$\begin{gathered} \forall (N:\mathbb{N}),\forall (\ell :\mathbb{N}),\forall (K:\mathrm{Subgroup}((\mathbb{Z}/N\mathbb{Z}{)}^{\times })),\forall (c:(\mathbb{Z}/N\mathbb{Z}{)}^{\times }),1<N\wedge \mathrm{Prime}(\ell )\wedge \mathrm{Coprime}(\ell ,N)\Rightarrow \\ \mathrm{let}{\pi }_{N,\ell }=\mathrm{reduceUnits}(N,\ell )\mathrm{in}\mathrm{let}H={\pi }_{N,\ell }^{-1}(K)\mathrm{in}\mathrm{let}e=\mathrm{unitOfCoprime}(\ell )\mathrm{in}\mathrm{let}C=\mathrm{cosetFinset}(N,K,c)\mathrm{in}\mathrm{let}{C}^{\prime }=\mathrm{cosetFinset}(N,K,e^{-1}c)\mathrm{in}\mathrm{let}L=\mathrm{liftedFinset}(N,\ell ,C)\mathrm{in}|H|=|K|(\ell -1)\wedge \\ |L|=|K|(\ell -1)\wedge \\ (\exists d\in (\mathbb{Z}/N\ell \mathbb{Z}{)}^{\times },{\pi }_{N,\ell }(d)=c\wedge L=\mathrm{cosetFinset}(N\ell ,H,d))\wedge \\ {M}_{N\ell }(L)=\ell M_N(C)+\frac{N|K|\ell (\ell -1)}{2}-\ell M_N(C^{\prime })\wedge \\ {F}_{N\ell }(H,L)=\ell (F_N(K,C)-F_N(K,C^{\prime }))\wedge \\ {F}_{N\ell }(H,L)=\ell (M_N(C)-M_N(C^{\prime })) \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ArithUnits/MercaCosetFiberLift.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

Index all representative blocks by (u,t) in C times {0,…,ell minus one}, with q equal to r_N(u) plus Nt. The representative bound gives q below N ell, and reduction of q modulo N is u. Consequently q is coprime to N. Euclidean quotient and remainder recover the pair, proving uniqueness. For blocks not divisible by ell, q is coprime to both factors and defines a unit modulo N ell reducing to u. Conversely a lifted unit v gives (pi(v),r_(N ell)(v)/N). Its reduction representative is the remainder modulo N, so the division equation recovers q exactly. Unit coprimality excludes divisibility by ell. The two maps are mutually inverse on native unit carriers and preserve the representative weight. For removed blocks, a unit y in C prime gives z equal to ell times r_N(y). The unit ey belongs to C, its representative is z modulo N, and the block (ey,z/N) has value z. In the inverse direction, divisibility gives a equal to q/ell with ell a equal to q and a below N. Coprimality of q with N implies coprimality of a with N, so a defines a native unit y. Reducing ell a equal to q proves ey equal to u; hence y belongs to the inverse-translated coset C prime. Division and block uniqueness prove both inverse identities. The removed weight is exactly ell times r_N(y). Summing all blocks gives ell M_N(C) plus N times the size of C times ell(ell minus one)/2, with the triangular sum calculated in the rationals. The removed sum is ell M_N(C prime), while the retained sum is M_(N ell)(L). Their disjoint partition proves the first-moment formula. Multiplication identifies each coset with K, so there are |K|ell blocks and |K| removed blocks. Thus L has |K|(ell minus one) elements. Setting c equal to one identifies its lift with H. Surjectivity of reduction on units provides d reducing to c, and pi(v) in cK is equivalent to d inverse times v in H, proving L equal to dH. Finally subtract the proven lifted center from the first-moment formula. The small-modulus centers are equal and cancel. No step uses primality of N, oddness of ell, a proper subgroup, an identity coset or cyclicity. Literature priority remains unassessed; no novelty claim is made.

References

• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.cosetFinset
• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.deviation
• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.liftedFinset
• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.moment
• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.reduceUnits
• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.result
• Truth anchor: D5/S3/ArithUnits/MercaCosetFiberLift.sum_fin_rat