Releases: Chi-sora/tau-sync-sieve
v0.1.2 - miner update
Arithmetization corrections and additions (draft for review)
Status
established:
definition, direct consequence of definitions, or proof under stated
preconditions
finite validation:
checked in a stated finite range by the reviewer's harness
correction:
the existing text is arithmetically inaccurate or weaker than provable
addition:
new arithmetized statement proposed for the documentation set
This document reviews docs/01..11 for statements that can be arithmetized
and for arithmetic inaccuracies. Each item names the file and section it
corrects or extends. Nothing here claims an infinite theorem.
Part A — Corrections
A1. classify5 misroutes prime x <= P_def [correction, established]
Target: docs/07 section 4 (classify5 flow), docs/05 section 5 (Shadow).
As written, classify5 tests the killed route before the prime route:
2. If x has a small prime factor p with 5 <= p <= P_def:
y = x / p
if y is prime: return S_K
else: return A_K
3. If x is prime: return P
For a prime x with 5 <= x <= P_def, step 2 fires with p = x and y = 1.
Since 1 is not prime, classify5 returns A_K.
counterexample:
classify5(7) = A_K (as written)
correct: P
Fix (either is sufficient):
step 2 condition:
exists prime p with 5 <= p <= P_def, p | x, and p < x
equivalently:
y = x / p with y >= 2
With the fix:
classify5(7) = P (step 2 skipped, step 3 fires)
classify5(25) = S_K (p=5 < 25, y=5 prime) unchanged
classify5(125) = A_K (p=5, y=25 composite) unchanged
The same edge appears in the Shadow equivalence in docs/05 section 5:
as written:
Shadow(x) ... equivalently, x has a small factor p with 5 <= p <= P_def
corrected:
Shadow(x):
x is composite
and exists prime p with 5 <= p <= P_def and p | x
For composite x every prime factor satisfies p < x, so the composite gate
makes the clause exact. Note this edge is invisible in the intended domain
(x >> P_def); it matters only for the formal statement and for any future
use of classify5 on small inputs. The included packed-index builder
(tau_c0c2cm_index/main.c) does not have this defect: its sieve marks only
multiples m >= p*p, so a prime x is never marked.
A2. S(x) >= 1 already implies composite [correction, established]
Target: docs/11 section 6 (Lemma 6.4, Theorem 6.5), docs/07
(S(x)+Exc(x) summary).
The current text hedges:
S(x) = 1 and not Exc(x):
Prime or Semi
Semi under the composite precondition
The hedge is unnecessary. If S(x) >= 1, some prime p satisfies p | x and
p*p <= x, hence 1 < p <= sqrt(x) < x, so p is a proper divisor and x is
composite. Therefore:
Lemma A2.1 [established]:
S(x) >= 1 -> x is composite
Theorem 6.5, strengthened branch [established]:
Unit6(x) and S(x) = 1 and not Exc(x) -> Semi(x)
No composite precondition is needed on this branch. The precondition
remains meaningful only in the implementation narrative (where S_total
arrives via a certified-composite path), not in the arithmetic statement.
Proof polish for Lemma 6.4: the case m = 1 in "m is 1 or prime" is
impossible under S(x)=1, because x = p would give S(x) = 0 (p*p <= p
fails for p >= 2). Also state explicitly that gcd(m,6)=1 follows from
Unit6(x), so the second counted prime q >= 5.
A3. tau totality convention [correction, established]
Target: docs/01 (Lapse), docs/05 section 7, docs/11 section 16.1.
tau_Cs(N) := min { j : C_s(N,j) holds }
is partial: if no j satisfies C, the minimum does not exist and the
relation tau_Cs(N) > J iff lapse_Cs(N,J) is ill-typed on the left.
Adopt the explicit convention:
tau_Cs(N) := min { j >= 1 : C_s(N,j) } if the set is nonempty
tau_Cs(N) := infinity otherwise
lapse_Cs(N,0) := true (empty prefix)
With this convention both stated relations hold for all J >= 0,
including the no-hit case, and LapseLen(N) = tau_g(N) - 1 is read as
infinity when tau_g(N) = infinity. This matters for arithmetization
and for any Lean/Coq formalization, where min over a possibly empty
set must be total or explicitly partial.
A4. tau_qs does not depend on N [correction, established]
Target: docs/05 section 3.
tau_qs(N) := min { j : Q_s(j) }
Q_s(j) contains no occurrence of N, so tau_qs is a constant function of
N. Either drop the argument (write tau_qs) or add a note that the value
is N-independent. Leaving the argument suggests a dependence that does
not exist.
A5. Lapse trichotomy: domain gates and wording [correction, established]
Target: docs/01 (Lapse decomposition), docs/02 (Lapse as arithmetic
no-hit prefix).
Three precision points.
-
docs/01 writes "x has a factor p with 5 <= p <= P_def" where docs/05
and docs/07 write "prime p". Inside the scan domain the two are
equivalent (x odd and 3 not dividing x force the smallest prime
factor of any such divisor to be >= 5), but for consistency write
"prime p" in docs/01 as well. -
The trichotomy
q_fail or x_killed_lapse or x_prough_lapse
is exhaustive and exclusive over the lapse prefix only under the
following arithmetic gates, which should be stated where the
decomposition is introduced:
parity gate [established]:
N even and q_s(j) odd -> x_s(N,j) odd
C3 gate [established, configuration-dependent]:
N != q_s(j) mod 3 at scanned indices -> 3 does not divide x_s(N,j)
positivity gate:
the scan is restricted to j with x_s(N,j) >= 5
(equivalently q_s(j) <= N - 5)
Without the positivity gate, x = 1 satisfies the literal
x_prough_lapse condition (no factor in [5,P_def]) while being
neither prime nor composite, and x <= 0 is outside the domain.
- Within the lapse prefix and with q_s(j) prime, x_s(N,j) is
automatically composite (x prime would give a Goldbach hit at
j < tau_g, contradicting minimality). State this one-line lemma:
Lemma A5.1 [established]:
j < tau_gs(N) and Q_s(j) and x_s(N,j) >= 5
-> x_s(N,j) is composite
This is the arithmetic reason x_prough_lapse splits into exactly
S_PR_lapse and A_PR_lapse with no prime residue case.
A6. g-sync: define j_forced, derive delta_x = 0 [correction, established]
Target: docs/01 (Sync), docs/02 (g-sync transfer), docs/05 section 8.
The g-sync event is currently listed as four independent conditions, but
two of them are derivable once j_forced is defined explicitly. Write
the lane signs as q_a(t) = 6t + e_a and q_b(j) = 6j + e_b with
e_a, e_b in {+1, -1}, and B = N_b - N_a.
Definition A6.1 (forced index):
j_forced(t) := t + (B + e_a - e_b) / 6
defined iff 6 divides (B + e_a - e_b)
Lemma A6.2 (lane compatibility) [established]:
j_forced is integral iff B = e_b - e_a (mod 6)
Lemma A6.3 (alignment) [established]:
if j_forced is defined, then
q_b(j_forced) = q_a(t) + B
and
delta_x(j_forced, t) = 0
Proof of A6.3: q_b(j_forced) = 6t + B + e_a - e_b + e_b = q_a(t) + B;
then x_b(N_b, j_forced) = N_a + B - q_a(t) - B = x_a(N_a, t).
Theorem A6.4 (g-sync, minimal premises) [established]:
G_a(N_a, t)
and 6 | (B + e_a - e_b)
and j_forced(t) >= 1
and Prime(q_a(t) + B)
-> G_b(N_b, j_forced(t))
and tau_gb(N_b) <= j_forced(t)
delta_x = 0 and valid_t need not be listed as separate premises:
delta_x = 0 is Lemma A6.3, and valid_t(a,b,B,t) is exactly
Prime(q_a(t)) and Prime(q_a(t)+B), the first conjunct of which is
already inside G_a. The existing event list is not wrong, but it is
redundant; the minimal form above is the arithmetized version.
Consistency check against the validated stream pairs
[finite validation]:
55 -> 15 and 51 -> 11: e_a = -1, e_b = +1, e_b - e_a = 2 (mod 6)
listed B in {68, 74}: 68 = 74 = 2 (mod 6) consistent
11 -> 51 and 15 -> 55: e_a = +1, e_b = -1, e_b - e_a = 4 (mod 6)
listed B in {70, 76}: 70 = 76 = 4 (mod 6) consistent
The orig-rule values (B = 68 or 74) both lie in the admissible residue
class, so the orig rule selects within the lane-compatible set, as
expected.
A7. PrimePair count zero: exact statement [correction, established]
Target: docs/11 section 3, Corollary 3.2.
The current caution ("x is prime, almost-prime class, or outside the
composite case") can be replaced by an exact equivalence once x = 1 is
excluded:
For x > 1:
|PrimePair(x)| = 0 <=> Prime(x) or Almost(x)
Reason: x > 1 is prime or composite; composite x has |PrimePair| = 1
iff Semi(x) (Corollary 3.2), hence 0 iff Almost(x).
A8. tau_g vs tau_gs naming [correction, definition]
Target: docs/11 section 8.1 versus docs/01 and docs/05.
docs/11 defines the stream-joined first hit
tau_g(N) := min { j : exists s, GoldbachHit(N,j,s) }
while docs/01 and docs/05 define per-stream tau_gs(N). Both are useful;
state the relation once:
tau_g(N) = min over s of tau_gs(N)
with the infinity convention of A3.
Part B — Additions (new arithmetized statements)
B1. x-side parity and C3 lemmas [addition, established]
Currently implicit; state once in docs/01 or docs/11 section 8:
Lemma B1.1:
N even -> for all j, s: x_s(N,j) is odd
Lemma B1.2 (already present as the C3 separation rule):
3 | x_s(N,j) <=> N = q_s(j) (mod 3)
Together these justify restricting endpoint composite certificates to
prime divisors p >= 5 inside the scan, which is the precondition for
the C0/C2/CM mark and for the killed/P-rough split.