Finite shadows of Zorn's lemma, and a well-order of Q

"""Where choice is not needed: finite Zorn arguments and an explicit well-order.

Zorn's lemma is needed for infinite posets. In a finite poset, "keep climbing
until you cannot" always stops, and the program does exactly what the lesson's
Zorn arguments do, finitely: (1) it extends random linearly independent sets
of vectors in (Z/2)^4 to maximal ones and checks they are bases of size 4,
counting all 840 bases; (2) it finds the maximal ideals of Z/n by searching
the poset of ideals, and compares them with the primes dividing n; (3) it
well-orders the positive rationals with no choice at all, by the Calkin-Wilf
enumeration x -> 1/(2 floor(x) - x + 1), checking that every fraction p/q with
p, q <= 12 appears exactly once among the first 4095 terms. Evidence: exact
and exhaustive for the finite cases computed.
"""

import random
from fractions import Fraction
from itertools import combinations
from math import gcd

DIM = 4

def span(vectors):
    """All XOR-combinations of the given bit-vectors (a subspace of (Z/2)^n)."""
    space = {0}
    for v in vectors:
        space |= {s ^ v for s in space}
    return space

def independent(vectors):
    """Linear independence over Z/2: the span has 2^k elements."""
    return len(span(vectors)) == 2 ** len(vectors)

def extend_to_maximal(start, order):
    """Climb: add each vector (in the given order) outside the current span."""
    current = list(start)
    for v in order:
        if v not in span(current):
            current.append(v)
    return current

def count_bases(dim=DIM):
    """Number of unordered bases of (Z/2)^dim, by exhaustive search."""
    vectors = range(1, 2 ** dim)
    return sum(independent(c) for c in combinations(vectors, dim))

def ideal(a, n):
    """The ideal of Z/n generated by a."""
    return frozenset(a * r % n for r in range(n))

def maximal_ideal_generators(n):
    """Generators d | n of the maximal ideals of Z/n, found by poset search.

    Every ideal of Z/n is generated by one element (by its smallest non-zero
    element, or by n for the zero ideal), so searching principal ideals finds
    them all.
    """
    ideals = {ideal(a, n) for a in range(n)}
    proper = [i for i in ideals if 1 not in i]
    maximal = [i for i in proper if not any(i < j for j in proper)]
    return sorted(min([x for x in i if x] or [n]) for i in maximal)

def prime_divisors(n):
    """The primes dividing n."""
    out, p = [], 2
    while p * p <= n:
        if n % p == 0:
            out.append(p)
            while n % p == 0:
                n //= p
        p += 1
    return out + ([n] if n > 1 else [])

def calkin_wilf(count):
    """The first `count` terms 1, 1/2, 2, 1/3, 3/2, ... of the Calkin-Wilf order."""
    x, out = Fraction(1), []
    for _ in range(count):
        out.append(x)
        x = 1 / (2 * (x.numerator // x.denominator) - x + 1)
    return out

def main():
    rng = random.Random(1904)
    vectors = list(range(1, 2 ** DIM))
    sizes = set()
    for _ in range(200):
        k = rng.randint(0, DIM)
        start = rng.sample(vectors, k)
        if not independent(start):
            continue
        order = vectors[:]
        rng.shuffle(order)
        result = extend_to_maximal(start, order)
        assert independent(result) and len(span(result)) == 2 ** DIM
        sizes.add(len(result))
    print("1. Extending independent sets in (Z/2)^4 until no vector can be added:")
    print(f"   every maximal set found spans the space; sizes seen: {sorted(sizes)}")
    print(f"   bases of (Z/2)^4 by exhaustive count: {count_bases()}"
          "  (= 15*14*12*8/4!)")
    print("2. Maximal ideals of Z/n, by searching the poset of ideals:")
    for n in (12, 30, 97, 360):
        gens = maximal_ideal_generators(n)
        print(f"   n = {n:>3}: generated by {gens}  primes dividing n: "
              f"{prime_divisors(n)}")
    agree = all(maximal_ideal_generators(n) == prime_divisors(n)
                for n in range(2, 61))
    print(f"   agreement for every n = 2..60: {agree}")
    print("3. A well-order of the positive rationals, with no choice:")
    seq = calkin_wilf(4095)
    print("   " + ", ".join(str(x) for x in seq[:14]) + ", ...")
    targets = {Fraction(p, q) for p in range(1, 13) for q in range(1, 13)
               if gcd(p, q) == 1}
    once = all(seq.count(t) == 1 for t in targets)
    print(f"   all {len(targets)} fractions p/q with p, q <= 12 appear exactly once")
    print(f"   among the first 4095 terms: {once}")
    print()
    print("Epistemic status: exact, exhaustive checks of finite cases. Finite")
    print("posets always have maximal elements, so no choice is used here. For")
    print("infinite-dimensional spaces and arbitrary rings the existence of bases")
    print("and maximal ideals needs Zorn's lemma: if ZF is consistent, ZF alone")
    print("cannot prove either statement in general.")

if __name__ == "__main__":
    main()