Construct exact mirror windows with one rank-pair classification

research/mirror-window-sweep/PROOF.md

@@ -0,0 +1,93 @@
+# One classification per rank pair constructs the same mirror windows
+
+This scoped algorithmic proof and implementation are produced by Nick
+Petalas. Apache-2.0. Window semantics and the compiler context are zxv's
+PR4483, retaining Ryanson Jonathan's corrected PR4459 mirror identity and
+Jacob Alan Sussman's integer compiler. Endpoint sweeps are classical.
+
+## Contract
+
+Let `T[k]` and `P[r]` be finite nonempty positive integer rank histograms.
+Form the sorted cuts `0`, `1/k` and `1/r`. The direct constructor visits each
+elementary cell `(left,right]` and every ordered target/paid pair. At any
+interior point `x`, that pair contributes `T[k]*P[r]` at product rank `kr`:
+
+- to the exit histogram when `r>k` and `1/r < x <= 1/k`;
+- to the source histogram when `k>r` and `1/k < x <= 1/r`.
+
+Equal ranks contribute neither. Cells with no exits are omitted. A cell
+with exits and no source histogram raises the funding error. The return
+value is the ordered list of retained `(left,right,exits,sources)` tuples.
+
+`windows.mirror_windows` preserves that complete return value and funding
+error on its declared input domain: each histogram has at most 64 ranks,
+and ranks and counts are positive integers at most `10^12`. Booleans are
+rejected. The original compiler's stronger native-profile hypotheses are
+unnecessary for this window-construction lemma.
+
+## Sweep invariant
+
+Each unequal pair has exactly one active interval
+`(a,b]=(1/max(k,r),1/min(k,r)]` on exactly one side. Place a positive event
+of weight `T[k]*P[r]` at `a` and its negative at `b`, using product rank `kr`
+as the histogram key. Product collisions add, rather than deduplicate.
+
+Immediately before emitting cell `(c_i,c_(i+1)]`, apply all events at its
+left endpoint `c_i`. The resulting active histogram contains exactly the
+pairs satisfying `a <= c_i < b`, equivalently `a < x <= b` for every
+interior point `x` in that cell. Thus it equals the direct histogram.
+Grouping all events before checking positivity preserves coincident starts
+and stops, including collisions at the same product rank.
+
+This proves the invariant by induction over the sorted cuts. The emission
+and funding rules then give identical return values or the same funding
+error at the same first offending cell. Applying the final closing events
+leaves both active histograms empty, an executable postcondition.
+
+The API copies each emitted histogram. Earlier cells cannot change when
+the sweep advances or when a caller edits another cell. Inputs and separate
+invocations share no mutable state.
+
+## Work removed and work retained
+
+Write `K=|supp(T)|`, `R=|supp(P)|`, `S` for the number of elementary cells,
+and `U` for the number of unequal ordered rank pairs. The direct constructor
+classifies `S*K*R` pairs. The sweep classifies `K*R` pairs and records exactly
+`2U` endpoint updates. These are enumerated logical operation counts, not
+elapsed-time or whole-caller complexity claims.
+
+Sorting cuts, updating active counters and copying output histograms remain
+payable. In particular, materializing all returned histograms can dominate
+the cost. No claim that total work is merely `O(KR)` follows from the pair
+classification reduction. Shared compiler code is not changed.
+
+On the exact retained inventories, the checker enumerates:
+
+| Inventory | Elementary / emitted cells | Direct classifications | Sweep classifications | Endpoint updates |
+| --- | --- | --- | --- | --- |
+| p7 | 16 / 9 | 1,296 | 81 | 158 |
+| p16 | 25 / 19 | 4,550 | 182 | 360 |
+
+The inventory files are cited inputs; no native supplier, root, invoice,
+compiler theorem or predecessor scientific certificate is being audited.
+
+## Evidence and limits
+
+The checker compares complete lists and every histogram multiplicity on all
+6,400 pairs of nonempty histograms on ranks 1–4 with counts 0–2. Exactly
+3,688 return matching lists and 2,712 reject for missing source funding.
+The written invariant, rather than extrapolation from that finite family,
+supplies the general equivalence proof.
+
+A literal boundary fixture gives one cell `(1/3,1/2]` with exit histogram
+`{6:33}` and source histogram `{4:35}`. Other controls exercise equal ranks,
+unfunded exits, colliding product ranks, malformed inputs, input preservation,
+independent cell snapshots and isolation across calls. Both modes use explicit
+exceptions and generate source/package-hash-bound receipts on stdout.
+
+There is no runtime speedup claim, default adoption, new compiler admission,
+native/caller implementation, κ improvement, selected-frontier change,
+independent human review or formal proof-kernel acceptance. The source's
+physical, chronological, ownership, precision, tape, stock and analytic
+obligations remain separate. Full caller timing and an incremental consumer
+are open questions.

research/mirror-window-sweep/README.md

@@ -0,0 +1,104 @@
+# Construct mirror windows with one classification per rank pair
+
+This scoped algorithmic proof and implementation are produced by Nick
+Petalas. The opt-in endpoint sweep returns exactly the same ordered mirror
+cells, complete integer histograms and funding errors as zxv's PR4483 direct
+constructor, while classifying each target/paid rank pair once.
+
+On the retained p16 input, pair classifications fall from 4,550 to 182;
+on p7 they fall from 1,296 to 81. The checker enumerates these counts and
+compares every output. They are operation counts, not a runtime speedup.
+Output copying, counter updates, exact moment evaluation and the rest of a
+compiler replay remain payable.
+
+[PROOF.md](PROOF.md) gives the interval invariant, input contract and limits.
+[windows.py](windows.py) is a standalone standard-library implementation.
+Shared/default code and frozen sources are unchanged. The contribution
+adds no compiler theorem, supplier, new κ or selected-frontier update.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Reproduction
+
+From the repository root with CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/mirror-window-sweep/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mirror-window-sweep
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mirror-window-sweep --check-source-history
+```
+
+An equivalent Python 3.12 path may replace the absolute path. Both registered
+commands run the complete new certificate in normal and optimized modes.
+Expected markers are `PASS_MIRROR_WINDOW_SWEEP`,
+`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`.
+Generated receipts bind every package and input file by SHA256 and go to
+stdout; no receipt is handwritten or consumed as a proof premise.
+
+The check covers all 6,400 nonempty histogram pairs on ranks 1–4 with counts
+0–2, including all 2,712 funding rejections, and complete retained p7/p16
+histograms. Twenty boundary, collision, input, capacity and ownership checks
+exercise half-open intervals, equal ranks, missing funding, invalid histograms,
+independent snapshots and separate invocations. The old direct definition is
+used only for implementation conformance. No predecessor scientific suite,
+native word, root or multiplication theorem is replayed as the deliverable.
+
+## API and scope
+
+`mirror_windows(targets, paid, stats=None)` accepts positive integer-keyed
+histograms. Each has at most 64 entries, with ranks and counts at most
+`10**12`. It returns `(left, right, exits, sources)` cells; endpoints are exact
+Fractions, and each Counter is independently owned. The optional stats map
+records pair classifications, endpoint updates and cell counts.
+
+The new sweep follows the exact original interval semantics. A pair has one
+active interval and therefore two boundary events. The proof includes all
+product collisions and source-funding errors. Histogram materialization is
+still proportional to the returned data. No complete-caller runtime claim
+or shared adoption is supplied.
+
+Scientific base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030. The replay-runtime card changes scope to this originally posed
+implementation question. [TASK.json](TASK.json) records the
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19380512),
+source/overlap coverage and exact scope. Live PRs, the full seven-day account
+list, claims, main README searches and merged/general-form searches were
+checked. Arbitrary diffs and unpublished work remain outside that coverage.
+
+## Open next questions
+
+- Does adopting the sweep reduce an actual complete compiler replay time?
+  First install it in one isolated current caller and benchmark end to end,
+  preserving every output and rejection. Exact powers or output copying may
+  dominate; this package supplies no such timing result.
+- Can an incremental exact moment consumer avoid copying each histogram?
+  First specify its endpoint and interval contract and compare complete
+  enclosures. Changing the consumer requires a separate proof.
+
+Structured relevance, first steps and blockers are in TASK.json.
+
+## Credit and code constraints
+
+The new implementation and proof are produced by Nick Petalas. Credit zxv
+PR4483 for the direct constructor and adaptive compiler, Ryanson Jonathan
+PR4459 for the corrected mirror semantics, Jacob Alan Sussman for the
+integer compiler, Cinna Davis for the retained p7/p16 inventories and
+Dugongue for the compact p16 consumer. Existing source notices remain
+unchanged. Endpoint sweeps and difference events are classical. New work
+is Apache-2.0.
+
+Build the Lever shaped the standalone opt-in function and rerunnable
+certificate. Prove It Works and Test Behavior, Not Implementation shaped
+the complete returned-value/error comparison, literal boundary fixture and
+ownership checks. The call graph is acyclic, functions fit within 60 lines,
+and explicit exceptions survive optimized execution. Both registered modes
+make warnings errors; no separate linter is installed.
+
+Power-of-ten rule 3 has a managed-runtime deviation: Python Counters,
+Fractions and output lists allocate while running. The API bounds each
+support by 64, hence at most 4,096 pair classifications, 8,192 endpoint
+updates and 128 elementary cells. The verifier has 6,400 fixed pairs and
+two fixed retained profiles, under 120-second per-command limits. Memory
+also includes copied output histograms. A long-lived or unbounded-input
+implementation needs its own allocation contract. No new dispatch,
+recursion, subprocess, network access or file-writing API is introduced.

research/mirror-window-sweep/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/compact-joint-compiler/arithmetic/RESULT.json",
+      "usage": "input",
+      "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff",
+      "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091"
+    },
+    {
+      "path": "research/higher-moment-strictification/RESULT.json",
+      "usage": "input",
+      "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a",
+      "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156"
+    },
+    {
+      "path": "research/rank-convergence/PROOF.md",
+      "usage": "input",
+      "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e",
+      "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376"
+    },
+    {
+      "path": "research/rank-convergence/compiler.py",
+      "usage": "input",
+      "git_blob": "2a3bfcb3b3700a3e7b4f339084ba5a5a1a1996da",
+      "sha256": "71e8fc45ee3a22f8197fdb023c538f1f55730e389c982b8cab3586ddc8217b5f"
+    }
+  ]
+}

research/mirror-window-sweep/TASK.json

@@ -0,0 +1,71 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "replay-runtime",
+    "question": "Can one measured replay bottleneck be sped up without dropping coverage?",
+    "starting_points": [
+      "scripts/run_isolated_tests.py",
+      "scripts/verify_replay_coverage.py",
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Profile one isolated replay and optimize the measured bottleneck.",
+      "Design source-bound reuse with explicit dependency invalidation and negative controls."
+    ],
+    "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.",
+    "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.",
+    "allowed_variations": [
+      "Profile one stage or design one source-bound cache boundary."
+    ],
+    "scope_change_triggers": [
+      "Skipping coverage or comparing different fixtures to claim speedup."
+    ],
+    "overlap_terms": [
+      "replay runtime",
+      "cache invalidation",
+      "isolated tests"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "An opt-in endpoint-event sweep constructs exactly the same elementary mirror windows as PR4483 while classifying each target/paid rank pair once. Exact full-output conformance and enumerated classification counts are certified.",
+  "scope_change_reason": "The card asks for a measured replay speedup. This scoped contribution instead proves an exact reduction in repeated pair classifications and supplies complete interface conformance. It does not claim a wall-time speedup or identify the complete caller bottleneck; those remain explicit next questions.",
+  "bottleneck_link": "Exact mirror histograms are reused in compiler admission inequalities. The sweep removes repeated pair classification while preserving every cell, product-rank multiplicity and source-funding rejection. It does not change native work or supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact reduction in repeated classifications. Do not tune additional kernels or infer a runtime speedup from operation counts.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, windows.py and verify.py: complete output equality on 6400 histogram pairs and retained p7/p16 inputs, exact endpoint/ownership/collision controls, and classification counts 1296 to 81 and 4550 to 182.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does explicit adoption of the sweep reduce an actual complete compiler replay time?",
+      "why_it_matters": "Fewer pair classifications do not measure total runtime; output copying and exact powers may dominate.",
+      "first_step": "Install the opt-in function in one isolated current compiler caller and perform a fair end-to-end benchmark with every output and rejection preserved.",
+      "blocked_by": "No shared/default adoption or full-caller timing is supplied."
+    },
+    {
+      "question": "Can consumers reuse endpoint events without materializing every full histogram?",
+      "why_it_matters": "The current implementation pays to copy each emitted source/exit histogram, so its total work includes output size.",
+      "first_step": "Specify an incremental exact moment consumer and compare its complete interval output with the materialized interface.",
+      "blocked_by": "A changed consumer contract needs separate proof and source binding."
+    }
+  ],
+  "coordination": {
+    "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19380512",
+    "source": "original implementation question; primary code predecessor zxv/PR4483"
+  }
+}

research/mirror-window-sweep/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/compact-joint-compiler/arithmetic/RESULT.json",
+    "research/higher-moment-strictification/RESULT.json",
+    "research/rank-convergence/PROOF.md",
+    "research/rank-convergence/compiler.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "All 6400 bounded histogram pairs, complete p7/p16 window conformance, classification counts and twenty endpoint/input/ownership controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same complete certificate under optimized Python; all checks use explicit exceptions."
+    }
+  ]
+}