Prove exact Gaussian phase-window boundary counts (no κ)

research/gaussian-phase-boundary-count/PROOF.md

@@ -0,0 +1,147 @@
+# Exact counts for the physical Gaussian carve
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and source
+
+Let s,k,w be positive integers, k<s, t=s+k, and assume
+
+    floor(s/(2k)) > 4w.                                      (1)
+
+For each integer x, let j be its residue in [0,s), p=floor(x/s), and
+
+    q_j=floor(tj/s+1/2),     h_j=q_j-j=floor(kj/s+1/2).
+
+A physical cell is a maximal interval on which the pair (p,h_j) is
+constant. The source cuts at physical period seams even if the unwrapped
+phase does not change there. For a nonempty window [a,a+m), intersect it
+with these cells. A piece of length L contributes
+
+    f(L) = L  if L<=4w,
+           2w if L>4w,                                      (2)
+
+boundary rows. A piece is called long exactly when L>4w.
+
+This is the carve in Jose Manuel / jmbarrancoml's PR3851,
+`gaussian_axis.py:prepare_weights` and
+`gaussian_window.py:prepare_positions,emit_cell`, retained at
+`7ab67b4a84d28cd562b9711aa315ca5b47822b37`. Its numerical and physical
+correctness are cited premises, not rechecked results. The construction
+and credit of its Gaussian, RaD, PR481/486/489 and physical-word predecessors
+remain with their sources. Dugongue's PR5566 already uses complete Beatty
+runs for another inverse algorithm; the floor identity and general run
+viewpoint are credited, rather than claimed as new mathematics.
+
+The new result is the exact count for this physical-period carve, its
+long-piece count and a smaller allowance for the unchanged caller.
+
+## Every complete cell is long
+
+In one physical period the phases are 0,...,k. Define their cuts
+
+    A_0=0,  A_(k+1)=s,
+    A_c=ceil(s(2c-1)/(2k)) for 1<=c<=k.
+
+The phase-c cell is exactly [A_c,A_(c+1)). This follows by solving
+c<=kj/s+1/2<c+1 for the integer j, including the half-open right
+endpoint. The first cell has length ceil(s/(2k)), the last has length
+floor(s/(2k)), and each other length is floor(s/k) or ceil(s/k).
+Consequently every complete physical cell has length at least
+floor(s/(2k)), and is long by (1). There are k+1 complete physical cells
+per period. The two half-runs at the ends must not be merged.
+
+The source production hypotheses include integer d with
+
+    k/s < 1/(2d-1),       d-2 > 4w.
+
+They imply s/(2k)>d-1/2, hence floor(s/(2k))>=d-1>4w.
+Thus (1) follows in that domain. Other production, locality and numerical
+hypotheses are not needed for this counting lemma and are not discharged.
+
+## Exact constant-size formula
+
+The cell containing x has ordinal
+
+    g(x)=floor(x/s)+floor(kx/s+1/2).                         (3)
+
+Indeed, writing x=ps+j gives g(x)=p(k+1)+h_j. Consecutive physical cells
+increase this ordinal by one, including negative periods and physical
+seams. If c=h_j, its left and right endpoints are
+
+    ell(x)=ps+A_c,          r(x)=ps+A_(c+1).                (4)
+
+Set b=a+m and C=g(b-1)-g(a)+1. This is exactly the number of nonempty
+pieces meeting the window. If C=1, then
+
+    n_B=f(m),             c_long=[m>4w].                   (5)
+
+Otherwise let L=r(a)-a and R=b-ell(b-1). Then
+
+    n_B = 2w(C-2)+f(L)+f(R),
+    c_long = C-2+[L>4w]+[R>4w].                            (6)
+
+Only the first and last pieces can be clipped. Each of the other C-2
+pieces is a complete long cell, proving both equations. The interior-row
+count is exactly m-n_B. The formulas hold for any positive window length,
+including multiple periods and arbitrary signed starts.
+
+The formula uses a fixed number of exact integer operations, independent
+of the number of rows or cells. This is an arithmetic-operation statement,
+not a constant bit-time claim or an encoded tape implementation. Integer
+division and descriptor access still need their physical charges.
+
+## A smaller source-domain allowance
+
+For 1<=m<=s, each floor difference in (3) is bounded above by the ceiling
+of its argument increment. The period difference is at most one. Hence
+
+    C <= 2+ceil(k(m-1)/s).
+
+For C>=2, f(L),f(R)<=4w, so (6) gives n_B<=2w(C+2). For C=1,
+f(m)<=4w also obeys the following bound. Since n_B<=m in every case,
+
+    n_B <= min(m, 2w ceil(k(m-1)/s)+8w).                  (7)
+
+The source's actual window satisfies s-m>w and therefore m<s, so it is
+covered. With theta=k/s and the source inequality theta<1/(2d-1),
+
+    2w ceil(theta(m-1))+8w
+        < 2theta mw+10w
+        < 2mw/(2d-1)+10w
+        < 4mw/d+12w.                                    (8)
+
+The last inequality uses d>=1 and w,m>0. Thus the new untrivialized
+allowance is strictly smaller than the published allowance; capping both
+allowances by m can make them equal on short windows. No new carve,
+word, numerical output or recursive paid profile is asserted.
+
+## Exact strict example and complete invoice substitution
+
+Take s=480,t=485,k=5,w=3,d=48 and [a,b)=[0,384). The phase-piece
+lengths are
+
+    48, 96, 96, 96, 48.
+
+They are all long. Equations (5)-(6) give n_B=30, c_long=5 and n_I=354.
+The published allowance is 4*384*3/48+12*3=132. Equation (7) is
+6*ceil(5*383/480)+24=48. This is a strict improvement of an upper bound
+for the same carve, not a changed execution. The ratio/spacing hypotheses
+hold; this small fixture is not an asymptotic production payload.
+
+The source's word-API count is
+
+    20 n_I + 16w^2 c_long + 2 n_B(4w+1)
+        + 2m + 2n_target + 2n_core + 32 c_long.
+
+Substitute n_I=m-n_B to obtain
+
+    22m+(8w-18)n_B+(16w^2+32)c_long+2n_target+2n_core.       (9)
+
+At fixed c_long=5, the old n_B allowance gives 10120 plus the last two
+terms, (7) gives 9616, and the exact count gives 9508. These totals are
+derived solely from the displayed source tariff. They do not claim fewer
+calls in the unchanged program. For w>=3 the n_B coefficient is positive,
+so an upper bound can be substituted in (9); for w=1,2 it is negative
+and that substitution would be invalid. Exact equations (5)-(6) remain
+valid for every w. The full tensor/setup/native invoice and all inherited
+numerical premises remain separate.

research/gaussian-phase-boundary-count/README.md

@@ -0,0 +1,121 @@
+# Exact boundary counts for Gaussian phase windows
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped counting proof with exact finite corroboration. For the unchanged
+physical-period/phase-cell carve in Jose Manuel / jmbarrancoml's
+[PR3851](https://github.com/CrocSwap/integer-mult-bounds/pull/3851), the
+boundary-row and long-piece counts have a formula requiring only the two
+endpoint cells and a fixed number of integer operations. It handles clipped
+pieces, negative lifted starts and windows crossing any number of periods.
+
+For one-period windows in the source production domain, the published
+allowance improves from
+
+    n_B <= 4mw/d+12w
+
+to
+
+    n_B <= min(m, 2w ceil((t-s)(m-1)/s)+8w).
+
+In the explicit s=480,t=485,w=3,d=48,m=384 window, the old allowance is
+132, the new allowance is 48, and the exact count is 30. The execution and
+actual number of rows are unchanged. This is a tighter accounting bound,
+with no new kappa or selected-frontier change.
+
+[PROOF.md](PROOF.md) gives the all-size formula and its source-domain
+implication. It also substitutes the exact row and long-piece counts in
+the complete source word-API tariff. This avoids silently charging saved
+boundary rows while forgetting their interior charge. The coefficient of
+n_B in that tariff is positive only for w>=3.
+
+## Evidence and reproduction
+
+From the repository root, using the CPython 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gaussian-phase-boundary-count/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gaussian-phase-boundary-count/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gaussian-phase-boundary-count
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gaussian-phase-boundary-count --check-source-history
+```
+
+Another CPython 3.12 path may replace the local path. The scientific marker
+is `PASS_GAUSSIAN_PHASE_BOUNDARY_COUNT`. Registered replay runs both modes.
+All acceptance checks use explicit exceptions and remain active under -O.
+Default replay writes nothing. Optional `--receipt PATH` exclusively creates
+a generated source-hash receipt outside the checkout; no receipt is handwritten.
+
+The independent literal checker computes nearest indices from t*j/s and
+groups the actual (physical period, nearest-j) keys. It appends one row at
+a time and updates the source's threshold rule without calling the closed
+form. It checks every s=10..64, w=1..3 and k satisfying the long-cell
+hypothesis, every starting residue and every length 1..2s+1. Alternating
+residues are shifted into negative periods. All 1,459,710 windows across 319 configurations agree exactly, including
+722,570 one-period upper-bound checks. Six semantic and eleven domain controls
+pass. Additional fixtures cover
+larger periods, translated starts, 4w/4w+1 thresholds and the strict example.
+The universal claim comes from the written proof, not these finite cases.
+
+The verifier authenticates the three source inputs before counting. It
+imports and executes no predecessor implementation or scientific suite.
+Source-byte hashes bind the scope; they do not certify the numerical or
+physical correctness inherited from the source.
+
+## Scope, credit and overlap
+
+Source head: `7ab67b4a84d28cd562b9711aa315ca5b47822b37` from PR3851.
+Publication base: canonical main `2485805a6d47f36ea83ddde6327d453ac82d44dc`,
+priority revision 8. [SOURCES.json](SOURCES.json) pins the retained source
+bytes, original card and selected record. [TASK.json](TASK.json) explicitly
+changes `uniform-transfer-audit` to this accounting side result for the
+analytic/physical caller. No selected assumption is discharged.
+
+Credit Jose Manuel for the complete physical producer/consumer and its
+carve, threshold and word-API tariff. Credit Dugongue's
+[PR5566](https://github.com/CrocSwap/integer-mult-bounds/pull/5566) for the
+related complete Beatty-run inverse and classical floor/run viewpoint;
+Vlado Vojdanovski and the phase-cell contributors, RaD/hipotures,
+Chafik Boukhalfa's PR481/486/489, the physical word implementation and the
+retained Harvey-van der Hoeven/source lineage. Those results are premises
+and context, not audit deliverables. Frozen sources and their credit remain
+unchanged. Elementary floor arithmetic is classical; no literature-priority
+claim is made for it.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19292015)
+preceded the experiment. Live PRs, recent account work, active Discussions,
+local reservations, merged searches and main-tree README formula/object
+searches were checked. The card helper had no usable remote cache and
+searched only 105 of 8722 local notes; separate live queries and Git-tree
+searches supplemented it. Sparse notes, arbitrary diffs and unpublished
+work remain outside coverage. These checks are not proof of novelty.
+
+No changed physical planner, numerical Gaussian replay, native supplier,
+retained-backing reduction, full tensor/setup bill, improved multiplication
+exponent or complete multiplication theorem is supplied. The fixture does
+not satisfy every production locality requirement. The full numerical,
+compiler, ownership, precision/tape and analytic assumptions remain.
+Independent human and formal proof-kernel review are unclaimed. Lean,
+Docker and the selected supplier cold replay were not run.
+
+## Open next questions
+
+Can the encoded preparation planner use the exact counts before allocating
+boundary banks? Start with one actual Window preparation, charge its encoded
+divisions and descriptor access, and compare retained backing and the whole
+setup/online bill. A changed physical allocation implementation is missing.
+The arithmetic formula alone establishes no storage or runtime reduction.
+
+## Implementation bounds
+
+The verifier is nonrecursive. Functions remain below 60 physical lines.
+The exhaustive domain fixes s<=64,w<=3 and at most 129 literal rows per
+scan; extra literal scans are capped at 1024. Formula inputs are capped at
+4096 bits, including a maximum-capacity fixture. The mathematical theorem
+has no such bit cap. Source/package reads are capped at 256 KiB per file.
+State is local, there is no dynamic code or scientific subprocess, and
+failures propagate. Python's integer, dictionary and temporary allocation
+are a managed-runtime deviation from fixed steady-state storage; finite
+loop, bit and file bounds constrain this command. Warning-strict normal
+and optimized execution are registered. An external static analyzer and
+fixed-allocation native implementation are not claimed.

research/gaussian-phase-boundary-count/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/physical-gaussian-core/PROOF.md",
+      "usage": "input",
+      "git_blob": "883c8d4a6f0eead888fb3532b60db41596940889",
+      "sha256": "e909026dd3f455c35ff28210a0c4ffa232ad8d7633174e481094fd09e2469d7a"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_window.py",
+      "usage": "input",
+      "git_blob": "335e0e2d2ee67302a67d1c5ba7c63baecc9b02d8",
+      "sha256": "d10eb4ac559a5dc3ef4a6178ab4cac7dfdcdb5e84ef8acf372bd22c81ab64996"
+    },
+    {
+      "path": "research/beatty-run-gaussian-inverse/analysis.md",
+      "usage": "provenance",
+      "git_blob": "e5cc397cd0baacd686cb8a075d636b9e595bdfae",
+      "sha256": "5c015de52b1867b07296c666bbe917c89ce508f6ca45dec909aceea0518b111a"
+    }
+  ]
+}