Certify six-bit stochastic precision for the selected P104 prefix (no κ)

research/p104-stochastic-prefix/PROOF.md

@@ -0,0 +1,176 @@
+# Stochastic precision on the first selected scalar block
+
+This proof and its source-bound certificate were produced by Nick Petalas.
+New work is Apache-2.0. The source word and its endpoint theorem are credited
+premises. This proof neither re-establishes that endpoint nor changes it.
+
+## The changed arithmetic contract
+
+Read `research/p104-helper-subspace-splits/WORD.json.gz` at the base pinned in
+SOURCES.json. Take the half-open program interval `[0,9589)`, stopping before
+its first MOVE. All 9,589 events are ADD or SCALE at frame 3, the empty frame.
+There are 9,358 ADDs and 231 SCALEs, on 748 public roles. The block touches
+501 roles. No native frame change, initialization or erasure occurs inside it.
+At a fixed stream sample, each real component is consequently a scalar linear
+straight-line program with fixed rational coefficients.
+
+Fix a grid spacing h > 0. All incoming scalar components, including every
+dirty helper component, belong to h Z. An ADD computes x_r + q x_s exactly
+before rounding once; a SCALE computes q x_r exactly before rounding once.
+This is a macro arithmetic contract, not a claim about the source's scalar
+bit implementation. There is no overflow or saturation. Integer-coefficient
+updates remain exactly on the grid and do not round. For a noninteger dyadic
+coefficient, write the exact updated scalar as h(a + theta), with integer a
+and 0 <= theta < 1. Return ha with probability 1-theta, or h(a+1) with
+probability theta, using a fresh draw conditional on the entire past. Exact
+grid values remain exact. Both negative numbers and arbitrary dirty values
+are included in this definition.
+
+The source coefficients have denominator 1, 2 or 4. Since the current values
+are on h Z, each noninteger update needs at most one or two fresh fair bits
+for exact sampling. There are 7,421 such updates, with total denominator
+logarithm 11,713. This bounds random bits per real sample for the literal
+fixed-draw sampler. It does not price integer operations, random-bit access,
+storage, routing or a full native implementation.
+
+## Exact output influences
+
+Let A_t be the exact update matrix for event t, and let d_t be its destination.
+Let R be the set of the 7,421 potentially rounded events. Number events from
+zero. Define the fixed output vector
+
+    b_t = A_(L-1) ... A_(t+1) e_(d_t),    L = 9589,
+
+where an empty product is the identity. For output j put
+
+    S_j = sum_(t in R) b_t[j]^2,
+    L_j = sum_(t in R) |b_t[j]|.
+
+These quantities concern propagation of newly injected errors, independently
+of the source's claimed endpoint map. The generated certificate computes
+all 748 pairs exactly. Two separate algorithms agree. The reverse engine
+starts from identity output columns, records each destination column before
+transposing that event, and uses integer vectors with binary denominators.
+The forward engine starts from zero formal errors, executes updates in their
+original order and injects a new independent formal variable after every
+event in R. It uses sparse Fraction dictionaries. Its final coefficients
+supply S_j and L_j directly.
+
+The resulting exact values are
+
+    max S_j = 733/8, attained only at role 217;
+    max L_j = 90, attained only at role 184;
+    sum S_j = 32269/4;
+    #{j : S_j > 0} = 282.
+
+The complete outputwise list is emitted by verify.py, with source/package
+hashes. There are 8,493 nonzero formal error coefficients at exit, with at
+most 98 in any output row. These are coefficient occurrences, not distinct
+program events. S_j is a sum over possible rounding sites, so it can be
+conservative when some sites happen to lie exactly on the grid. No equality
+claim for the worst actual stochastic variance is made.
+
+## Conditional variance and tails
+
+Let epsilon_t be the additive rounding error after event t. Conditional on
+the past, it has mean zero, variance at most h^2/4, and two possible values
+in an interval of length h. Set epsilon_t = 0 outside R. Because every
+update is linear, the exact difference from the unrounded block is
+
+    E_j = sum_(t in R) b_t[j] epsilon_t.
+
+The weights are deterministic. Cross terms have zero expectation by
+conditioning the later error on its past. Hence, for every allowed input,
+
+    E[E_j] = 0,
+    E[E_j^2] = sum_t b_t[j]^2 E[epsilon_t^2]
+             <= h^2 S_j/4,
+    E[sum_j E_j^2] <= 32269 h^2/16.
+
+Errors generally are not independent. Their distributions can depend on
+previous rounded states. Conditional zero mean is the property used here.
+
+For completeness, a centered random variable in an interval of length h
+satisfies E exp(lambda X) <= exp(lambda^2 h^2/8). Indeed, the second derivative
+of its log moment generating function is a variance under exponential tilt.
+Every tilted distribution has the same support interval. If a <= Y <= b,
+E[(Y-a)(b-Y)] >= 0 gives Var Y <= (b-a)^2/4 after completing the square.
+Integrating the derivative bound twice from zero proves the displayed
+inequality for positive and negative lambda. Apply it conditionally at each
+event, with lambda replaced by lambda b_t[j], then iterate conditional
+expectation. Chernoff's bound, optimized at lambda = 4u/(h^2 S_j), gives
+
+    Pr(|E_j| >= u) <= 2 exp(-2u^2/(h^2 S_j))    if S_j > 0.
+
+An output with S_j = 0 has zero error. A union bound, requiring no independence
+between outputs, therefore gives
+
+    Pr(max_j |E_j| >= u) <= 564 exp(-16u^2/(733 h^2)).
+
+This is an absolute-error statement. It has no input-magnitude factor,
+first-order truncation or asymptotic remainder.
+
+## A one-bit certificate improvement on this block
+
+For h = 2^-6 and u = 1/2, the preceding failure bound is
+
+    564 exp(-16384/733) < 2^-23.
+
+The strict inequality has an exact rational certificate. Put x = 16384/733.
+The verifier evaluates P = sum_(k=0)^64 x^k/k! and checks
+
+    P > 564 * 2^23.
+
+Since exp(x) > P, the claimed probability follows without a floating-point
+exponential or logarithm. For complex scalars at one stream sample, apply
+the same reasoning to both real and imaginary components. The simultaneous
+componentwise failure probability is below 2^-22. At M samples, a union
+bound multiplies these bounds by M; there is no all-stream assertion at
+fixed failure probability. Independence between samples is not needed for
+that union bound, provided each scalar update satisfies its own conditional
+rounding contract.
+
+For deterministic nearest rounding on the same block, the local error is
+at most h/2. The exact absolute-influence certificate gives
+
+    max_j |E_j| <= 45h.
+
+To certify a strict error below 1/2 with h = 2^-g, this bound needs g >= 7.
+At g = 6 it gives 45/64; at g = 7 it gives 45/128. Thus the stochastic
+certificate uses one fewer fractional bit for a stated failure probability.
+This is a comparison of sufficient certificates. It does not prove that
+nearest rounding at six bits fails, or that stochastic six-bit precision is
+optimal. The allowed initial 2^-6-grid inputs also belong to the 2^-7 grid.
+The exact prefix endpoint need not be integral, so this observation does not
+by itself imply integer recovery.
+
+## Essential boundaries and rejection controls
+
+Fresh conditional randomness is essential. For two updates y += x/2 with
+x = 1 and y = 0 on the unit grid, reusing the same fair bit makes the final
+error -1 or +1. Its variance is 1, while S_y/4 = 1/2. Each individual rounding
+has the right unconditional marginal, which is insufficient. Always rounding
+both ties down instead has bias -1. The verifier enumerates the fresh-draw
+versions and checks their genuine conditional probabilities.
+
+A later inverse word with fresh rounding need not restore the dirty inputs
+exactly, even if its exact linear endpoint is the identity. For example,
+y += x/2 followed by y -= x/2 can leave error -1 or +1 with positive
+probability. The finite fixtures include this word. We do not claim exact
+restoration from small expected error or a high-probability enclosure.
+
+No MOVE is rounded or executed here. Initial off-grid conversion, native
+frame operators, later scalar blocks, overflow headroom, correlated physical
+error, bit-level sampling/costs, exact cleanup, compiler/stock admission,
+analytic recovery and whole-multiplier error remain separate obligations.
+The full selected source theorem is reused only as provenance, not audited.
+The five selected framework assumptions are unchanged. Independent human
+and formal proof-kernel review are unclaimed.
+
+The rounding method and bounded-martingale argument are classical. See
+Connolly, Higham and Mary, *Stochastic Rounding and Its Probabilistic Backward
+Error Analysis*, SIAM J. Sci. Comput. 43 (2021), A566-A585,
+https://doi.org/10.1137/20M1334796, for mean-independent stochastic rounding.
+The fixed-grid proof above is self-contained. The contribution is the new
+exact selected-block influence certificate and its explicit precision/failure
+specialization, not a new general concentration theorem.

research/p104-stochastic-prefix/README.md

@@ -0,0 +1,141 @@
+# A stochastic precision certificate for the selected P104 prefix
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped proof with an exact finite influence certificate. On the selected
+#5599 word's first 9,589-event common-frame scalar block, fresh unbiased
+fixed-grid stochastic rounding has exact squared influence maximum **733/8**.
+For arbitrary incoming grid values, including dirty helpers, six fractional
+bits give simultaneous absolute error below 1/2 in every real output at one
+stream sample with failure probability below **2^-23**. For both components
+of complex outputs the probability is below **2^-22**.
+
+The deterministic nearest-rounding absolute-influence certificate on this
+same block gives error at most 45h and needs seven fractional bits to certify
+a strict error below 1/2. This is a one-bit improvement between sufficient
+certificates with different guarantees. Neither precision is proved optimal,
+and the exact intermediate endpoint need not be integral.
+
+The stochastic arithmetic contract is new here. Each noninteger dyadic scalar
+update is evaluated exactly and rounded once, with fresh conditional randomness.
+Integer-grid operations are exact. No predecessor verifier is imported or
+replayed, and no predecessor result is audited. [PROOF.md](PROOF.md) derives
+the variance and tail inequalities, explains their classical basis and states
+the complete boundary. No new kappa, physical supplier or multiplication
+theorem is claimed.
+
+## Evidence and reproduction
+
+The standalone verifier authenticates the frozen selected word and extracts
+its prefix before the first MOVE. A reverse integer-column engine and an
+independent chronological formal-error engine agree on all 748 output pairs.
+The generated stdout receipt includes every output's squared and absolute
+influence, the source/package hashes and the exact tail certificate.
+
+The block contains 7,421 potentially rounded updates. Its maximum absolute
+influence is 90; 282 outputs have nonzero formal noise influence. The forward
+engine retains 8,493 nonzero formal coefficients, at most 98 per output.
+An exact positive Taylor polynomial proves the exponential comparison.
+All 125 tiny-input fixtures are enumerated, with 423 terminal state occurrences.
+No random sampling is used.
+Controls distinguish chronological order, altered coefficients, fresh draws
+from a reused coin and unbiased rounding from biased ties. All checks remain
+active with Python optimization.
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/p104-stochastic-prefix/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -O -B research/p104-stochastic-prefix/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-stochastic-prefix
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-stochastic-prefix --check-source-history
+```
+
+Another CPython 3.12 path may replace the displayed interpreter. Expected
+markers are `PASS_P104_STOCHASTIC_PREFIX`, `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES`. Each registered command has a 120-second
+limit. The direct verifier writes no files. The publication preflight needs
+committed files and full source history. A Git-free replay needs this package
+and the single live word path declared in VERIFY.json.
+
+## Scope, cost and limitations
+
+The changed `uniform-transfer-audit` scope concerns the selected
+`precision_tape` assumption. Source-binding orientation passes, but no selected
+scientific replay is performed. Canonical base is
+`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228531)
+records the question. Live open PRs, account history, Discussions, local
+reservations, main README contents and distinctive merged-PR terms were
+searched. Sparse local cache coverage is incomplete, and these checks cannot
+exclude unpublished overlap or establish literature priority.
+
+The prefix uses one empty common frame and no MOVE. The proof is scalar and
+pointwise. All incoming values must already lie on the chosen grid; overflow
+and saturation are excluded. At M samples a union bound multiplies the stated
+failure probability by M. The literal dyadic sampler needs at most 11,713
+fresh fair bits per real sample, with integer arithmetic and random-bit
+movement still unpriced. Native approximation, input conversion, later blocks,
+stream-wide precision, physical random sampling, exact dirty restoration,
+compiler/stock obligations and analytic recovery remain unproved. All five
+selected framework assumptions remain. Independent human and formal
+proof-kernel review are unclaimed. Lean, Docker and full multiplier replays
+were not run.
+
+Fresh rounding does not make a rounded inverse restore dirty inputs exactly.
+A two-update identity word in the proof can leave a nonzero error. A reused
+coin can also violate the variance bound even when its one-step marginals
+look unbiased. These limitations prevent interpreting the certificate as an
+admitted randomized supplier.
+
+## Credit
+
+Ali Romman's #5599 supplies the selected independent-helper word and split
+construction. Pierre-Loic Doulcet / hexapode's #5565 supplies its commuting
+contacts. Retain Ali Romman's #5580/#5544/#5545, Joel Pulikkan / GamingPuzzled's
+#5569, DreamingOfClouds' #5561, thu-nmrc's #5551, Gareth Davidson / bitplane,
+David Arias, Cinna Davis, Jacob Alan Sussman, zxv, Cao Yifan and all geometry,
+BIT, native, precision, analytic and source predecessors in the unchanged
+[selected notice](../p104-helper-subspace-splits/NOTICE).
+SOURCES.json pins that notice and the source README as provenance.
+
+Stochastic rounding and mean-independent error analysis are classical; see
+[Connolly, Higham and Mary (2021)](https://doi.org/10.1137/20M1334796).
+The proof gives the fixed-grid concentration argument directly. The new
+contribution is the exact selected-prefix influence certificate, its explicit
+failure bound and the comparison of sufficient precision certificates.
+
+## Open next questions
+
+Can one complete native caller use this rounding model while restoring its
+dirty state exactly? Start with a round-and-restore ABI that retains and then
+erases its random bits, charging every action. A physical reversible sampler
+and its complete cost are the present blockers.
+
+Can a finite sample count and the next actual MOVE preserve a useful total
+failure budget? First propagate this block's errors through that native
+operator with its own approximation contract. Whole-stream precision and
+later blocks are outside this certificate. Structured questions are in
+TASK.json.
+
+## Code constraints
+
+The verifier is nonrecursive and uses no subprocess, network, dynamic code
+or write path. Fixed source bounds are 26,000 full-word events, 9,589 extracted
+events, 748 roles, coefficients with denominator at most four and absolute
+value at most 16. Reverse vectors have at most 128-bit numerators and exponent
+64; forward rational coefficients have matching bit caps, enforced during
+replay. Each formal row has at most 10,000 terms. Source
+reads are capped at 1 MiB compressed and 4 MiB unpacked, and six receipt reads
+at 1 MiB each. Tiny probability trees have at most eight steps, three roles
+and 256 states, enforced during enumeration. The Taylor sum has 65 terms.
+Functions fit below 60 physical lines. Warning-strict development-mode normal
+and optimized runs are the available diagnostics; no external static analyzer
+or whole-repository lint configuration is claimed.
+
+Power of Ten rule 3 has a managed-runtime deviation. Python, Fraction, JSON
+and gzip allocate dynamically. The verifier is a finite offline check with
+the enforced collection and input caps above, rather than a fixed-allocation
+arithmetic implementation. Its matrix and dictionary capacities are finite;
+this does not inspect allocator internals or establish a real-time guarantee.
+A deployed sampler would need its own storage and random-bit lifetime proof.

research/p104-stochastic-prefix/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/NOTICE",
+      "usage": "provenance",
+      "git_blob": "f34687ff7eab377d5433f7b0c18274a816d2b73c",
+      "sha256": "8bbda66537ac761d632603066bdbb568ab5b26545030ea7979e27a85fcbe040c"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/README.md",
+      "usage": "provenance",
+      "git_blob": "f6303a881379723e1f6512dfe153fafeecbf62dd",
+      "sha256": "a83c5c3ae7a31a5dfbc3c7c59669ee55cc15f966a0cb4405cb48cb8fa2a94f56"
+    },
+    {
+      "path": "research/p104-helper-subspace-splits/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "e325091e3051afe37a2d9c82f85afe9028510edb",
+      "sha256": "bbb072bced5824a8d9094c49be2fc51fbfdd05fb2b7dab8106e1275053075099"
+    }
+  ]
+}