The Multiplier-Two Obstruction Modulo 157

Abstract

Doubling orbits obstruct a thirteen-element affine multiplier relation modulo 157.

Theorem 1.1 (Affine fixed-point translation gives multiplier invariance).

$$\forall R\in Type,D\in Finset\left(R\right),m\in R,shift\in R,center\in R,\left(CommRing\left(R\right)\wedge \left(m\cdot center=center+shift\wedge imageMul\left(D,m\right)=imageAdd\left(D,shift\right)\right)\right)\Rightarrow imageMul\left(imageSub\left(D,center\right),m\right)=imageSub\left(D,center\right)$$

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

Source. Repository-derived.

Commentary.

Let D be a finite subset of a commutative ring. If multiplication by m takes D to its translate by shift and center is a fixed point of the associated affine map, translating D by negative center converts the relation into invariance under multiplication by m.

Theorem 1.2 (Nonzero multiplier orbits divide the invariant-set cardinality).

$$\forall p\in \mathbb{N},u\in Units\left(ZMod\left(p\right)\right),S\in Finset\left(ZMod\left(p\right)\right),\left(Prime\left(p\right)\wedge imageMul\left(S,coe\left(u\right)\right)=S\right)\Rightarrow orderOf\left(u\right)\mid card\left(eraseZero\left(S\right)\right)$$

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

Source. Repository-derived.

Commentary.

For a prime modulus, the cyclic subgroup generated by a unit acts freely on the nonzero part of every invariant finite set. The orbit quotient times the cyclic subgroup is therefore equivalent to that nonzero part, so the unit order divides its cardinality.

Theorem 1.3 (Two has multiplicative order 52 modulo 157).

$$orderOf\left(2:ZMod\left(157\right)\right)=52$$

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

Source. Repository-derived.

Commentary.

Kernel-checked modular powers establish exponent 52 and exclude the proper prime-divisor exponents required by the finite-order criterion.

Theorem 1.4 (Doubling-invariant cardinalities have residue zero or one).

$$\forall S\in Finset\left(ZMod\left(157\right)\right),imageMul\left(S,2\right)=S\Rightarrow card\left(S\right)\mathrm{mod}52\in \left\{0,1\right\}$$

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

Source. Repository-derived.

Commentary.

The nonzero part has cardinality divisible by 52. Splitting on whether zero is present leaves exactly the residues zero and one for the full set.

Theorem 1.5 (No thirteen-element affine multiplier relation exists modulo 157).

$$\forall D\in Finset\left(ZMod\left(157\right)\right),g\in ZMod\left(157\right),card\left(D\right)=13\Rightarrow imageMul\left(D,2\right)\ne imageAdd\left(D,g\right)$$

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

Source. Repository-derived.

Commentary.

Translation by negative g conjugates a supposed affine relation to pure doubling invariance without changing cardinality. The resulting set would have cardinality 13, contradicting the zero-or-one residue theorem modulo 52.

Theorem 1.6 (The explicit thirteen-residue set has a nontrivial doubling inequality).

$$card\left(thirteenResidues\right)=13\wedge imageMul\left(thirteenResidues,2\right)\ne imageAdd\left(thirteenResidues,0\right)$$

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

Source. Repository-derived.

Commentary.

The explicit residues from zero through twelve form a thirteen-element finite set modulo 157, and a kernel computation shows that its doubling image is not its zero translate. Both clauses are retained in one theorem.

Theorem 1.7 (A three-element doubling orbit exists modulo seven).

$$orderOf\left(2:ZMod\left(7\right)\right)=3\wedge \left(card\left(doublingOrbitSeven\right)=3\wedge imageMul\left(doublingOrbitSeven,2\right)=doublingOrbitSeven\right)$$

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

Source. Repository-derived.

Commentary.

Modulo seven, two has order three and the explicit set containing one, two, and four has cardinality three and is invariant under doubling. All three clauses are retained in one theorem.

This module proves only the multiplier-two orbit obstruction for a hypothetical cyclic (157,13,1) difference set. It does not formalize the First Multiplier Theorem bridge, the Singer correspondence, or nonexistence of an arbitrary projective plane of order twelve.

References

• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.affine_multiplier_conjugacy
• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.card_of_invariant_under_mul_two
• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.doublingOrbitSeven_witness
• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.multiplier_two_obstruction
• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.orderOf_dvd_card_erase_zero_of_image_mul_eq
• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.orderOf_two_zmod157
• Truth anchor: D5/S3/ArithUnits/CyclicPlaneTwelveMultiplierObstruction.thirteenResidues_witness