Factorial lanes / exact Python program
Ten step-factorial lanes, hypergeometric coordinates, factorial normalization, reciprocal inversion, five-adic checks and counterexamples. Python 3.10 or later, standard library only.
Read the complete hand derivation Download Python · Source and exact results ZIP · Source identities
Checked data: lane-products.csv · coefficients.csv · results.json
Run python -B factorial_lanes.py. Add --output factorial-results to write exact CSV and JSON tables.
1 #!/usr/bin/env python3
2 """Factorial lanes: independent, exact, standard-library worked example.
3
4 This computes a finite example; it does not certify unrelated research claims.
5 """
6 from __future__ import annotations
7
8 import argparse
9 import csv
10 from fractions import Fraction
11 import json
12 from math import comb, factorial, prod
13 from pathlib import Path
14
15 N, J, P = 10, 4, 5
16
17
18 def step_factorial(start: int, n: int, step: int = N) -> int:
19 """(start)_(n;step), including the empty product when n=0."""
20 if n < 0 or step <= 0:
21 raise ValueError('n must be nonnegative and the step positive')
22 return prod(start + step * k for k in range(n))
23
24
25 def lane_products(n: int) -> dict[int, int]:
26 return {r: step_factorial(r, n) for r in range(J + 1, J + N + 1)}
27
28
29 def pochhammer(value: Fraction, n: int) -> Fraction:
30 return prod((value + k for k in range(n)), start=Fraction(1))
31
32
33 def parameters() -> tuple[Fraction, ...]:
34 """The parameter 1 is handled by the built-in n! of 0F9."""
35 return tuple(Fraction(r, N) for r in range(J + 1, J + N + 1) if r != N)
36
37
38 def hypergeometric_coefficient(n: int) -> Fraction:
39 denominator = Fraction(factorial(J) * N ** (N * n) * factorial(n))
40 for alpha in parameters():
41 denominator *= pochhammer(alpha, n)
42 return 1 / denominator
43
44
45 def unit_tail(n: int) -> Fraction:
46 """Coefficient of t^(10n)/(10n)! after removing t^4/4!."""
47 return Fraction(1, comb(N * n + J, J))
48
49
50 def reciprocal_coefficients(last: int) -> list[Fraction]:
51 """Exact exponential-basis inverse of the normalized residue section."""
52 g = [unit_tail(n) for n in range(last + 1)]
53 c = [Fraction(1)]
54 for n in range(1, last + 1):
55 c.append(-sum((comb(N*n, N*k) * g[k] * c[n-k]
56 for k in range(1, n + 1)), Fraction(0)))
57 return c
58
59
60 def valuation(value: Fraction | int, prime: int = P) -> int | None:
61 """None represents infinity (the valuation of zero)."""
62 value = Fraction(value)
63 if not value:
64 return None
65 a, b, exponent = abs(value.numerator), value.denominator, 0
66 while a % prime == 0:
67 a //= prime
68 exponent += 1
69 while b % prime == 0:
70 b //= prime
71 exponent -= 1
72 return exponent
73
74
75 def finite_difference(n: int, steps: tuple[int, ...]) -> Fraction:
76 """Delta_q1 ... Delta_qs g(n), computed by exact inclusion-exclusion."""
77 total = Fraction(0)
78 for mask in range(1 << len(steps)):
79 degree = mask.bit_count()
80 offset = sum(step for i, step in enumerate(steps) if mask & (1 << i))
81 total += (-1) ** (len(steps) - degree) * unit_tail(n + offset)
82 return total
83
84
85 def check() -> dict[str, int]:
86 totals = {'lane_and_hypergeometric': 0, 'reciprocal': 0,
87 'prime_unit_and_displacement': 0, 'refinement': 0,
88 'boundary_witness': 0}
89 alphas = parameters()
90 assert len(alphas) == 9 and Fraction(1) not in alphas
91 for n in range(7):
92 assert factorial(J) * prod(lane_products(n).values()) == factorial(N*n + J)
93 assert hypergeometric_coefficient(n) == Fraction(1, factorial(N*n + J))
94 assert unit_tail(n) == Fraction(factorial(J) * factorial(N*n), factorial(N*n+J))
95 totals['lane_and_hypergeometric'] += 3
96 coeffs = reciprocal_coefficients(7)
97 for n, coefficient in enumerate(coeffs):
98 total = sum((comb(N*n, N*k)*unit_tail(k)*coeffs[n-k]
99 for k in range(n+1)), Fraction(0))
100 original = sum((comb(N*n+J, N*q)*coeffs[q]
101 for q in range(n+1)), Fraction(0))
102 assert total == original == (1 if n == 0 else 0)
103 assert valuation(coefficient) is None or valuation(coefficient) >= 0
104 totals['reciprocal'] += 2
105 assert coeffs[1] == -Fraction(1, 1001)
106 assert coeffs[2] == Fraction(178205, 966966)
107 assert [valuation(x) for x in coeffs[:5]] == [0, 0, 1, 0, 1]
108 for n in range(16):
109 g = unit_tail(n)
110 assert valuation(g) == 0
111 assert n == 0 or valuation(g - 1) >= 3
112 totals['prime_unit_and_displacement'] += 2
113 for q in (1, 2, 5, 10):
114 for n in range(6):
115 # Special four-factor cancellation supplies two extra powers of 5.
116 assert valuation(unit_tail(n+q)-unit_tail(n)) >= 3 + valuation(q)
117 totals['prime_unit_and_displacement'] += 1
118 for steps in ((2,), (2,2), (2,2,2), (2,2,2,2), (2,10), (5,10)):
119 for n in range(5):
120 value = finite_difference(n, steps)
121 lower = len(steps) + sum(valuation(q) for q in steps)
122 assert valuation(value) is None or valuation(value) >= lower
123 totals['prime_unit_and_displacement'] += 1
124 # Both the two-child and the literature's five-child refinements are exact.
125 for degree in range(100):
126 parent = int(degree % 10 == 4)
127 children_20 = int(degree % 20 == 4) + int(degree % 20 == 14)
128 children_50 = sum(int(degree % 50 == r) for r in (4, 14, 24, 34, 44))
129 assert parent == children_20 == children_50
130 totals['refinement'] += 1
131 # Outside 0 <= j < 5 the uniform unit conclusion can fail.
132 assert valuation(Fraction(1, comb(25, 5))) == -1
133 # Omitting the r=10 lane also fails to reconstruct the factorial.
134 assert factorial(4)*prod(v for r,v in lane_products(3).items() if r != 10) != factorial(34)
135 totals['boundary_witness'] += 2
136 return totals
137
138
139 def write_tables(folder: Path, counts: dict[str, int]) -> None:
140 folder.mkdir(parents=True, exist_ok=True)
141 cs = reciprocal_coefficients(7)
142 with (folder/'coefficients.csv').open('w', encoding='utf-8', newline='') as stream:
143 writer = csv.writer(stream)
144 writer.writerow(('n', 'degree', 'g_n', 'C_n', 'v5_g_n', 'v5_C_n'))
145 for n,c in enumerate(cs):
146 writer.writerow((n, 10*n+4, str(unit_tail(n)), str(c),
147 valuation(unit_tail(n)), valuation(c)))
148 with (folder/'lane-products.csv').open('w', encoding='utf-8', newline='') as stream:
149 writer = csv.writer(stream)
150 writer.writerow(('lane_start', 'factors_n3', 'product'))
151 for r, value in lane_products(3).items():
152 writer.writerow((r, ' * '.join(str(r+10*k) for k in range(3)), value))
153 (folder/'results.json').write_text(json.dumps({
154 'case': {'N': N, 'j': J, 'p': P},
155 'finite_assertions': counts, 'total': sum(counts.values()),
156 'interpretation': 'Finite exact checks, not a general formal proof.'
157 }, indent=2)+'\n', encoding='utf-8')
158
159
160 def main() -> None:
161 parser = argparse.ArgumentParser(description=__doc__)
162 parser.add_argument('--output', type=Path, help='Optional folder for exact CSV and JSON tables')
163 args = parser.parse_args()
164 counts = check()
165 print('FACTORIAL LANES | N=10, j=4, p=5')
166 print('34! = 4! * product of ten step-10 lanes (n=3)')
167 print('lane products: '+', '.join(f'{r}:{v}' for r, v in lane_products(3).items()))
168 cs = reciprocal_coefficients(3)
169 for n in range(4):
170 print(f'n={n} g_n={unit_tail(n)} C_n={cs[n]} v5(C_n)={valuation(cs[n])}')
171 print(f'PASS: {sum(counts.values())} exact finite assertions')
172 if args.output:
173 write_tables(args.output, counts)
174 print(f'Exact tables written to {args.output}')
175
176
177 if __name__ == '__main__':
178 main()