diff --git a/exact_quantum_factoring_v2.txt b/exact_quantum_factoring_v2.txt
index 70b57ff..fd1da38 100644
--- a/exact_quantum_factoring_v2.txt
+++ b/exact_quantum_factoring_v2.txt
@@ -2,35 +2,38 @@ EXACT QUANTUM FACTORING OVER A FIXED FINITE GATE SET
 ====================================================
 
 A note to young readers
------------------------
+=======================
+
+This is a complete proof of one theorem: there is a quantum algorithm
+that factors every integer N >= 2 into its prime factorization with
+probability exactly one, using a fixed finite gate set, in polynomial
+time and space. Every lemma and proposition in this paper exists only
+to build that.
 
-This is a complete proof of a theorem about quantum computers and
-factoring. The reader is assumed to know modular arithmetic (a^n mod m,
-gcd, Euler's totient phi), complex numbers, and matrix multiplication.
-No prior knowledge of quantum computing is assumed; each unfamiliar
-object is defined when it first appears.
+Prerequisites. Integer arithmetic (division, gcd, powers mod m),
+Euler's totient, complex numbers, 2x2 matrices. No prior quantum
+computing; each unfamiliar object is defined first. A qubit is a unit
+vector in C^2; a gate is a unitary matrix of fixed size. Nothing is
+hidden.
 
-If this is your first pass, read Section 1 (the big picture), Section 2
-(the setup), then the STATEMENT of every lemma, proposition, and theorem,
-skipping the proofs. Read the proofs on a second pass. Each formal
-statement is a finished claim on its own; each proof uses only material
-from earlier in the paper plus the reference it cites.
+How to read. First pass: Sections 1-2 for the map, then every lemma
+and theorem STATEMENT, skipping proofs. Second pass: the proofs. Each
+uses only earlier material plus the cited reference. Every proof is
+complete; nothing is waved away.
 
-Every lemma, proposition, and theorem is proven in full. There is no
-"we omit the proof" and no "standard argument gives". If you get stuck
-on a line, the surrounding paragraphs contain the missing steps.
+Why "probability one" matters. No "with high probability" or "large
+enough constant" arguments. Every probability is exact; every
+polynomial is explicit. The theorem is exact, and the proof is exact.
 
 Abstract
 --------
 
-We prove: there is a polynomial-time uniform family of polynomial-size
-quantum circuits that, on input any integer N >= 2, outputs the complete
-prime factorization of N with probability exactly one. Every circuit in
-the family uses the same fixed finite gate set, and both the number of
-gates and the number of qubits are bounded by a fixed polynomial in the
-bit length of N. Neither arbitrary-angle rotations nor a growing gate
-library are needed. The proof is constructive and covers every step from
-the arithmetic to the final measurement.
+We prove: a polynomial-time uniform family of polynomial-size quantum
+circuits outputs the complete prime factorization of every integer
+N >= 2 with probability exactly one. Every circuit uses the same fixed
+finite gate set, and both gate count and qubit count are polynomial in
+the bit length of N. Neither arbitrary-angle rotations nor a growing
+gate library are needed. The proof is constructive.
 
 Contents
 --------
@@ -106,41 +109,29 @@ chosen explicitly.
 1.2 Prior work
 --------------
 
-Shor [Shor] gave polynomial-time quantum factoring and discrete log
-with bounded error. Miller [Miller] introduced the order-to-gcd
-reduction.
-
-Exact transforms and algorithms appear in several quantum models.
-Mosca and Zalka [MZ] construct exact Fourier transforms using "computed
-rotations": gate parameters obtained during the computation. In that
-model they obtain exact discrete-log for known group orders, and they
-report Mosca's exact factoring algorithm in a generalized model
-([MZ] Section 5.2, see also [Imran] Section 1). Imran [Imran]
-constructs an exact order-finding algorithm that takes a supplied
-multiple of the unknown order. A suitable multiple of polynomial bit
-length is additional information that factoring does not provide
-initially. Both are material model and input distinctions. Nishimura
-and Ozawa [NO] study exact computation by finitely generated uniform
-circuit families and show why approximate universality cannot replace
-explicit gate analysis.
-
-Recent resource-oriented algorithms include Regev [Regev] and
-Pilatte [Pilatte]. Regev's construction initially required a
-number-theoretic hypothesis; Pilatte proves unconditional correctness
-for modified versions. Their success guarantees remain probabilistic.
-This paper addresses a different axis: certainty and worst-case
-polynomial bounds in a specified exact gate model, with no claim to
-practical resource improvement.
-
-Amplitude amplification (Grover [Grover], Brassard-Hoyer-Mosca-Tapp
-[BHMT]) is the tool of the final step. Exact probability engineering at
-success 1/4 already appears in Brassard-Hoyer's exact algorithm for
-Simon's problem [BH], and Mosca-Zalka use success 1/4 plus one ordinary
-amplification step ([MZ] Section 2.1). General schemes for exact
-amplification with phases depending on the success probability are
-[Hoyer,BHMT]. Here the factoring preparation makes the success
-probability exactly 1/4 with fixed gates and dyadic arithmetic; then
-the standard one-step reflection suffices.
+Shor [Shor] gave polynomial-time quantum factoring with bounded
+error, via the order-to-gcd reduction of Miller [Miller]. Exact
+quantum algorithms exist in stronger models: Mosca-Zalka [MZ] use
+"computed rotations" (gate parameters set during the computation) to
+obtain exact transforms, and report Mosca's exact factoring algorithm
+([MZ] Sec 5.2); Imran [Imran] gives exact order finding that requires
+a supplied multiple of the unknown order, which factoring does not
+provide; Nishimura-Ozawa [NO] show why approximate universality
+cannot replace an exact gate analysis. This construction uses only
+the fixed gate set of Section 2, receives only N, and accepts no
+advice.
+
+Recent resource-oriented algorithms [Regev, Pilatte] also factor in
+polynomial time; some required number-theoretic hypotheses, later
+removed; their guarantees remain probabilistic. This paper is about a
+different axis: certainty and worst-case bounds in an exact model.
+
+Amplitude amplification [Grover, BHMT] is the final step. Brassard-
+Hoyer's exact Simon algorithm [BH] already achieves success 1/4, and
+Mosca-Zalka [MZ] Sec 2.1 use success 1/4 plus one ordinary
+amplification step. Here the factoring preparation makes success
+probability exactly 1/4 using fixed gates and dyadic arithmetic; the
+standard one-step reflection then makes it 1.
 
 1.3 Strategy and the ancestry of its ingredients
 ------------------------------------------------
@@ -204,6 +195,14 @@ verification of the auxiliary data and the all-good generation
 property. A second dyadic correction makes the full preparation's
 success probability exactly 1/4.
 
+For a concrete taste of the arithmetic, take N = 15 and a = 2, a unit
+mod 15. The powers of 2 mod 15 are 2, 4, 8, 1, 2, ... so ord_15(2) = 4.
+Since r = 4 is even, gcd(2^{r/2} - 1, 15) = gcd(3, 15) = 3, splitting
+15 = 3 x 5. Every factoring run reduces to this. The bulk of the paper
+is the exact-probability engineering that makes r (a multiple of the
+true order) appear with a prescribed dyadic mass, using only a fixed
+finite gate set.
+
 1.4 Road map
 ------------
 
@@ -377,12 +376,10 @@ independent of anything else in the paper.
 SECTION 3. AN ORDER TRIAL WITH A PRESCRIBED SUCCESS PROBABILITY
 ---------------------------------------------------------------
 
-This is the technical heart. For a unit a modulo m, we construct a
-quantum trial whose probability of returning the true order is an
-explicit dyadic function of that order. No knowledge of the order
-itself, or of its factorization, is required to run the trial. This
-additional control of the success probability is what allows the
-final factoring algorithm to be exact.
+This is the technical heart. We construct a quantum trial whose
+probability of returning the true order is an explicit dyadic
+function of that order, with no knowledge of the order or its
+factorization. That control is what makes the final algorithm exact.
 
 3.1 Definitions and the target proposition
 ------------------------------------------
@@ -409,10 +406,9 @@ satisfying 1 <= d < B and r | d. Moreover,
 The trial uses only the fixed finite gate set G and does not require r
 or any factorization of r.
 
-Two comments. (1) "No candidate" is an allowed outcome; if the trial
-returns some d then d is a positive multiple of r. (2) The mass at r
-is exactly phi(r) lambda(r), not merely bounded below. This is the
-crucial feature.
+(1) "No candidate" is allowed; a returned d is a positive multiple of
+r. (2) The mass at r is exactly phi(r) lambda(r), not just bounded
+below. This is the crucial feature.
 
 The construction has two parts. First we replace the Fourier phases in
 order sampling by a piecewise-linear phase function g that admits exact
@@ -754,11 +750,9 @@ it applies equally to complex-valued functions.) Therefore
 
     |I(u)| >= (1/d)(2/pi - pi^2/32) > 1/(8d).
 
-For the numerical check: pi < 2 sqrt(3), obtained from
-tan(pi/6) > pi/6, so 2/pi > 1/sqrt(3). And pi^2 < 12, so
-pi^2/32 < 12/32 = 3/8. Hence 2/pi - pi^2/32 > 1/sqrt(3) - 3/8, which
-is about 0.202 and certainly > 1/8. The upper bound |I| <= 1/d follows
-from |g| <= 1.
+(Numerical check: pi < 2 sqrt(3) gives 2/pi > 1/sqrt(3), and pi^2 < 12
+gives pi^2/32 < 3/8; so 2/pi - pi^2/32 > 1/sqrt(3) - 3/8 > 1/8. The
+upper bound |I| <= 1/d follows from |g| <= 1.)
 
 Step 3: piecewise-polynomial representation of J. Let G be the
 continuous primitive of g satisfying G(0) = 0. Because g is piecewise
@@ -824,35 +818,21 @@ and
 using d < B and Q = B^16 (so 65 B / (2 Q) = 65/(2 B^15) < 1/2). This
 proves (b) for the STATED U.
 
-Step 5: computing S(d,j) without enumerating residues. What remains is
-computing (1/2) sum_{u=0}^{d-1} U(d,j,u) in polynomial time. Since U is
-a sum of a bounded number of piecewise polynomials, sum over each
-piece's integer range.
-
-Intersect the bounded collection of rational piece intervals with the
-integers 0, ..., d-1, using floors and ceilings and assigning each
-boundary integer only once. There are at most 17 pieces (the quarter
-intervals of [-1/2, 3/2], each crossed with the argument u/d, plus the
-eta = 0 special case). Sum each piece-polynomial by the integer power
-sums through degree four. These sums are computed, for example,
+Step 5: computing S(d,j) without enumerating residues. U is a sum of a
+bounded number of piecewise polynomials over integer ranges. Intersect
+the pieces with integers 0, ..., d-1 using floors and ceilings,
+assigning each boundary integer once. There are at most 17 pieces
+(quarter intervals of [-1/2, 3/2] crossed with u/d, plus eta = 0).
+Sum each piece by the power sums through degree four, computed
 recursively from
 
     M^{q+1} = sum_{l=0}^{q} binom(q+1, l) sum_{u=0}^{M-1} u^l
                 (0 <= q <= 4),
 
-which follows from M^{q+1} = sum_{u=0}^{M-1} ((u+1)^{q+1} - u^{q+1}). The
-zeroth power sum is the count M, with u^0 = 1 also at zero. These sums
-have O(n) bits for M <= B, and there are only a bounded number of
-pieces. This computes S(d,j) in polynomial time without enumerating the
-residues.
-
-Since D = Q B^8 is a power of two, both U and S are dyadic with O(n)-bit
-representations. All operations used to compute them are rational
-arithmetic, integer division, and rounding. The proof is complete. []
-
-The next subsection uses this majorant to add the discrepancy between
-P and U by uniform random choices. A further, smaller correction makes
-the mass per reduced numerator exactly lambda(d).
+which follows from M^{q+1} = sum_{u=0}^{M-1}((u+1)^{q+1} - u^{q+1}).
+The zeroth sum is M, with u^0 = 1 also at zero. Sums have O(n) bits
+for M <= B. Since D = Q B^8 is a power of two, both U and S are
+dyadic with O(n)-bit representations. The proof is complete. []
 
 3.7 Three modes with a prescribed mass
 --------------------------------------
@@ -985,22 +965,17 @@ predicate valid(d, j), whose conjunction includes a^d = 1 mod m. Since
 r is the least positive integer with this property, r | d. A return
 with no candidate is also allowed by the statement.
 
-Polynomial cost. All arithmetic is exact: the P, U, S, c, rho are
-dyadic with polynomial bit length (Lemma 3.3, Definition 3.2), and the
-integer arithmetic performed on them uses only polynomial-bit integers.
-The quantum part is Lemma 3.1 (cost polynomial in b = 16n), applied a
-bounded number of times. The classical checks (valid(d,j), the
-retention comparisons, and the sum over phi(r) numerators) are
-polynomial bit operations. There is no dependence on r or on the
-factorization of r. This proves all claims of Proposition 3.1. []
-
-Remark. The error term in (a) is not zero, and at false labels no
-identity between the artificial P(d, j, t) and a quantum probability
-was used. The correctness at the true label r uses only equation (***),
-which is a genuine probability. False labels are simply not attempted;
-validation rejects them. This is why the trial makes no claim about
-false-label mass, and this is also why the mass at r is known exactly
-despite the trial not knowing r.
+Polynomial cost. All arithmetic is exact: P, U, S, c, rho are dyadic
+with polynomial bit length, and integer arithmetic on them is
+polynomial. The quantum part is Lemma 3.1, applied a bounded number
+of times. The classical checks (validation, retention comparisons,
+summation over phi(r) numerators) are polynomial bit operations. There
+is no dependence on r or on its factorization. []
+
+Remark. The error term in (a) is not zero, but at false labels d != r
+the trial makes no claim about P(d, j, t): validation rejects those
+labels before any probability is used. At the true label r, (**) is a
+genuine quantum probability, and the trial's mass at r is exact.
 
 SECTION 4. FACTORING WITH VERIFIABLE AUXILIARY DATA
 ---------------------------------------------------
@@ -1183,21 +1158,16 @@ We now compute the good probability of the list transition without
 enumerating residues. The key fact is that a uniform unit modulo m has
 all 2-adic levels equal with probability at most 1/2.
 
-Cyclic structure of a prime field. Let p be an odd prime with p^e || m.
-The nonzero elements of the residue field F_p form a cyclic group under
-multiplication.
+Cyclic structure of F_p. Let p be an odd prime with p^e || m. The
+nonzero elements of F_p form a cyclic group.
 
 Proof. Let T be the exponent of F_p^*: the least T with x^T = 1 for all
-nonzero x. Lagrange gives ord(x) | p - 1 for every x, so T | p - 1.
-
-The exponent of a finite abelian group is attained. For each prime
-power q^k || T, take x_k with q^k | ord(x_k). Then
-x_k^{ord(x_k)/q^k} has order exactly q^k. The product over the distinct
-q's has order T.
-
-The polynomial X^T - 1 has at most T roots in any field, but every
-nonzero element of F_p is a root, so p - 1 <= T. Combining with
-T | p - 1 gives T = p - 1. An element of order p - 1 generates F_p^*.
+x != 0. Lagrange gives T | p - 1. The exponent of a finite abelian
+group is attained: for each prime power q^k || T, an element whose
+order contains q^k yields, after taking a power, an element of order
+exactly q^k; the product of these has order T. But X^T - 1 has at most
+T roots in F_p, and every nonzero element is a root, so p - 1 <= T.
+Thus T = p - 1 and F_p^* is cyclic.
 
 Two-adic levels in F_p. Write p - 1 = h 2^l with h odd. In a cyclic
 group of order p - 1, the count of elements with v_2(order) = t is
@@ -1262,7 +1232,7 @@ Hence with K = n^5,
       >= 1 - exp(-n^4/8)
       >= 1 - 2^{-2n}    (for n >= 128).
 
-The denominator of s is at most 2^{b_m * K} <= 2^{nK}, polynomial in n.
+The denominator of s divides 2^{nK}, so s has at most nK <= n^6 bits.
 
 4.6 The order good probability
 ------------------------------
@@ -1298,7 +1268,7 @@ Then with K = n^5,
 Denominator. Since r < B = 2^n, phi(r) < 2^n. And
 lambda(r) = 2^{-ceil(log_2 r) - 10} with ceil(log_2 r) <= n. So
 phi(r) lambda(r) has denominator dividing 2^{n+10}. Then s has
-denominator dividing 2^{(n+10)K}, polynomial in n.
+denominator dividing 2^{(n+10)K}, so s has at most (n+10)K = O(n^6) bits.
 
 4.7 Why good transitions split
 ------------------------------
@@ -1650,8 +1620,8 @@ So the output is correct.
 Polynomial bounds. Each of the L conditional pass probabilities is a
 dyadic with denominators dividing 2^E where E = W + 2n + 2 =
 O(n^6), or from the transition's own s with denominators dividing
-2^{(n+10)K} = 2^{n^6 + 10 n^5}. Both are polynomial. Evaluating the
-deferred tests over L slots, using the retained histories, costs
+2^{(n+10)K} = 2^{n^6 + 10 n^5}. Both denominators have polynomial
+bit length. Evaluating the deferred tests over L slots, using the retained histories, costs
 polynomial time and workspace. The output string is polynomially
 long. This completes the proof. []
 
@@ -1659,8 +1629,8 @@ Final bound. p_* = (1 - 2^{-n})^{n^{10}}. Bernoulli gives
 (1 - 2^{-n})^{n^{10}} >= 1 - n^{10} 2^{-n}. At n = 128 the subtracted
 term is 2^{-58}, and the function x^{10} 2^{-x} is decreasing for real
 x >= 128 because its logarithmic derivative 10/x - ln 2 is negative
-there. So p_* > 1 - 2^{-58} > 1/2. Its denominator 2^{n^{11}} is
-polynomial in n. []
+there. So p_* > 1 - 2^{-58} > 1/2. Its denominator is 2^{n^{11}}, whose
+bit length n^{11} is polynomial in n. []
 
 5.4 A known quarter of success
 ------------------------------