Reduce complete mapped-contact replay time by 72.54% (no new κ)

research/rank-contact-replay/PROOF.md

@@ -0,0 +1,107 @@
+# Exact rank execution of mapped contacts
+
+This scoped implementation proof and the accompanying code were produced by
+Nick Petalas. David Ganz / Dugongue's PR4841 supplies the retained geometric
+formula, caller, graph and expected receipt. Rank-nullity and binary Gaussian
+elimination are classical. No new geometric lower bound is claimed.
+
+## Equality of the two actual-change computations
+
+Let U,V be n-dimensional subspaces of F2^(2n), with bases B_U,B_V. For any
+axis a, define T_a(x)=x+omega(x,a)a, where omega is the standard alternating
+binary symplectic form. Since omega(a,a)=0, T_a is linear and T_a^2=I.
+Consequently T_a(B_U) is a basis of T_a(U).
+
+The retained function computes
+
+    dim(U intersect V) - dim(T_a(U) intersect V).
+
+Rank-nullity gives dim(U intersect V)=2n-rank(B_U union B_V), and the
+corresponding identity holds for T_a(U). Subtraction therefore yields
+
+    rank(T_a(B_U) union B_V) - rank(B_U union B_V).
+
+This is exactly `ContactRank.__call__`. Its elimination works over F2 by
+XOR, so no floating-point or modular reconstruction premise enters. Isotropy
+of U and V is unnecessary. The code accepts 1<=n<=9, matching and bounding
+the source caller's domain. The same algebraic identity holds in every n.
+
+The difference lies in {-1,0,1}. Indeed T_a(B_U)-B_U has row space inside
+the line spanned by a, so the two concatenated matrices differ by a
+rank-at-most-one matrix. The runtime assertion checks this consequence.
+
+For an input set S of size 2^n, `checked_basis` validates ambient coordinates
+and span dimension n. Every point of S belongs to its computed span; the
+equal cardinalities imply that S is the entire subspace. This also rejects
+incomplete or nonclosed sets. Booleans are rejected as coordinates and axes.
+
+## One-contact cache and complete caller
+
+The cache stores one pair of immutable frozensets, their bases, width and
+original union rank. Object identity and width are tested on every call.
+Repeated equal sets with different identities are recomputed. A new cache
+entry is published only after both subspaces validate. Axis validation
+precedes access. Failed preparation leaves the preceding cache usable.
+The cache owns no state outside one replay and retains no historical contacts.
+
+The retained `small` and `actual_graph` functions execute without edits.
+Only the `actual_change` function reference in one freshly loaded module is
+replaced. The distinct retained `change_formula`, chosen edges, fixed seed,
+sampled axes, actual maps, rank checks and all receipt fields stay literal.
+The replacement never calls `change_formula`. The candidate still performs
+79,360 actual-change computations and 1,240 contact preparations. Complete
+receipt equality is checked against the authenticated retained JSON.
+
+For a contact queried q times, preparation uses at most 2^(n+1) input
+vectors once. Each subsequent query moves n basis vectors and eliminates
+2n rows, instead of moving and intersecting a set of 2^n vectors. Work is
+O(2^n n^2 + q n^3) elementary binary steps per contact, compared with
+O(q 2^n n) for a literal bit-cost implementation of the retained set route.
+These are algorithmic envelopes, not measured machine costs or a new supplier
+tariff. The physically relevant supplier program itself is unchanged.
+
+## Checks and scope
+
+`verify.py` compares the new engine directly with the retained literal
+intersection on all Lagrangian pairs through n=3, all axes including zero,
+and all 35 binary 2-planes, including nonisotropic ones. It adds 72 wider
+pairs through n=9, invalid inputs, cache-failure and sign/constant mutants.
+It then executes the complete retained caller with the replacement installed.
+The benchmark runs that whole caller with each engine in fresh processes,
+checks its receipt, and requires identical stdout hashes on every run.
+
+The written proof establishes replacement equivalence. The finite checks
+exercise its implementation; they are not a new proof of the predecessor's
+geometric claims. The full PR4841 five-command package, graph regeneration,
+native supplier, compiler, physical caller, precision and outer admission are
+outside this contribution. No selected assumption or kappa changes.
+
+## Code constraints
+
+Every new loop has a finite bound. Subspaces contain at most 512 points;
+ambient width is at most 18; basis unions contain at most 18 vectors. The
+conformance domains are explicit finite sets and the benchmark accepts five
+through nine pairs, with a 120-second subprocess limit. All functions are
+under 60 physical lines. Rejection checks remain active with optimization.
+
+Power of Ten rule 3 deviation: CPython allocates integer and collection
+objects during elimination. The public n<=9 check bounds live data to one
+contact's two at-most-512-point sets, two nine-vector bases and an 18-vector
+elimination buffer, plus caller-owned source data. No growing contact cache
+is used. A fixed-buffer implementation is a possible later port; it is not
+required for this Python research replay. The tests exercise the n=9 bound
+and invalid widths. Runtime/library allocator internals are not inspected.
+
+Power of Ten rules 8 and 9 deviation: the unchanged caller is loaded through
+one explicit authenticated file path, and one module function reference is
+replaced by one explicit callable object. This is necessary to run the real
+frozen caller without modifying its files. There is no input-selected module
+or callback registry. Exact hash checks precede loading, and complete caller
+and invalid-source controls cover the boundary. No source implementation is
+generated or evaluated from a string. A future upstream adoption could use
+an ordinary explicit engine parameter instead of this isolated adapter.
+
+Warning-strict normal and optimized execution, source compilation and AST
+function-length inspection pass locally. Ruff and mypy are not installed in
+the available environment; no static-type-checker pass is claimed. Their
+absence does not suppress a diagnostic or change shared repository checks.

research/rank-contact-replay/README.md

@@ -0,0 +1,92 @@
+# Faster complete mapped-contact replay
+
+The complete PR4841 mapped-contact distance caller takes 2.252 s rather than
+8.199 s at the median of five alternating fresh-process pairs on the recorded
+local machine, a **72.54% time reduction**. All ten runs succeed with identical
+output hashes. This is a scoped implementation-equivalence proof with finite
+conformance and local performance evidence. No new kappa is claimed.
+
+The implementation, proof and experiments were produced by Nick Petalas.
+David Ganz / Dugongue retains PR4841's compiler, geometric predicates, complete
+small-domain checks, frozen graph and expected receipt. Cao Yifan's PR4610 and
+Cinna Davis's PR4690/4672 retain the actual-word and contact-model lineage.
+The full unchanged predecessor notice is an authenticated input.
+Rank-nullity and binary elimination are classical. New work is Apache-2.0.
+
+## Change and evidence
+
+The original actual-change engine moves all 512 elements of each nine-dimensional
+subspace for every axis. The replacement moves nine basis vectors and computes
+an exact binary rank. A one-contact cache retains the original union rank and
+the two immutable bases. [PROOF.md](PROOF.md) derives equality with literal
+intersection without using the separate transvection-distance formula.
+
+The complete caller retains every small check, 4,429 frames, 145 maps, all
+1,240 chosen mapped edges, the same seed and every one of 79,360 sampled axes.
+Its output is checked against the original authenticated JSON. The new engine
+prepares exactly 1,240 contacts and executes every actual-change query.
+No frozen predecessor file is edited.
+
+The replacement conformance check covers 1,170,036 Lagrangian pair/axis cases
+through width three, including the zero axis; 19,600 cases on all binary
+two-planes; one equal-value cache replacement; and 4,608 wider cases through
+width nine. Eleven invalid inputs, four changed-source controls and two
+incorrect-output controls reject. Normal and optimized Python run the same
+checks. This is verification of the replacement implementation, not a new
+audit claim for the predecessor's construction.
+
+The untimed profile attributes 16.799 of 18.866 profiled seconds to the
+retained actual-change engine. Its generator performs 40,711,680 iterations.
+The timing experiment includes interpreter startup, source authentication,
+both complete caller phases, expected-output validation and JSON output.
+Literal samples range from 8.028 to 8.284 s; rank samples range from 2.196 to
+2.302 s. The medians are 8.198592292 and 2.251555958 s. Every side runs the
+same source, flags and checks. The host has 18 logical CPUs, with observed
+load averages 3.66/2.51/1.80 before measurement. Other work may run on this
+shared machine, so the local percentage is not a hardware-independent promise.
+The profile is excluded from the timing samples. It explains why removing
+the enumeration can affect the complete path by this amount.
+
+## Reproduce
+
+From the repository root, using the Python 3.12 environment:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank-contact-replay/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rank-contact-replay/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank-contact-replay
+```
+
+The direct commands print `PASS_RANK_CONTACT_REPLAY` in generated JSON. The
+launcher must also print `PASS_REGISTERED_RESEARCH_PACKAGE`. Source pins are
+in [SOURCES.json](SOURCES.json); all four live inputs are declared in
+[VERIFY.json](VERIFY.json). Python's standard library suffices.
+
+Run `replay.py` for the complete faster caller or add `--engine literal` for
+the retained engine. To remeasure, choose an existing scratch directory and run:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank-contact-replay/benchmark.py --output "$TMPDIR/contact-benchmark.json"
+```
+
+The benchmark emits actual timings, exit status, complete work counts, output
+hashes, environment and package-file hashes. It refuses to write inside the
+package. Generated logs and receipts belong outside the checkout. Set TMPDIR
+to the chosen scratch directory to place verification's temporary corruption
+fixtures there too. CI runs conformance, not a speed threshold.
+
+## Limits
+
+The measured path is the entire retained `decoder/testformula.py --graph ...`
+caller. It is one command of PR4841's larger package, not its whole five-command
+compiler suite. Graph regeneration, new chart search, native implementation,
+physical hosting, supplier admission, precision and outer funding were not run.
+The five framework assumptions and selected frontier remain unchanged. No
+independent human or formal proof-kernel acceptance is claimed.
+
+## Open next questions
+
+Can a basis-only contact ABI remove complete-subspace materialization too?
+That could remove preparation work, but changes the caller interface. Start
+with a bounded validated basis contract and measure the whole source caller.
+It remains outside this first-improvement package.

research/rank-contact-replay/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/native-clifford-gauge-compiler/NOTICE.md",
+      "usage": "input",
+      "git_blob": "5519958ecf6200f04b63a4783f805394c717b915",
+      "sha256": "ea459c3cae30546924cc4d3521eca3d982db19d34ae37cb04d0651909df1081e"
+    },
+    {
+      "path": "research/native-clifford-gauge-compiler/decoder/TRANSVECTION-EXPECTED.json",
+      "usage": "input",
+      "git_blob": "6e929cc239937ccd9374d02856e0379fe23109a1",
+      "sha256": "18a092c2cd4cd9174488646782c86f1bcc3ef044bbb5d7feceb6c513f6fc7988"
+    },
+    {
+      "path": "research/native-clifford-gauge-compiler/decoder/testformula.py",
+      "usage": "input",
+      "git_blob": "0533809634361ff9954df601a77184461c1abbb0",
+      "sha256": "a9f32161eb0222ae9279a96f74504b0af8863ac6251973d9fde32f205dd3ed8c"
+    },
+    {
+      "path": "research/native-clifford-gauge-compiler/inputs/round3-contact-graph.txt",
+      "usage": "input",
+      "git_blob": "31e1bfc6c5ca64d1056bce4f35861d840412cd2a",
+      "sha256": "f802be993525ec7b944a2622c4fd47db76101d7a558ea449ece7254780f6efef"
+    }
+  ]
+}

research/rank-contact-replay/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "replay-runtime",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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": "refined",
+  "actual_scope": "Exact basis-rank execution of the complete PR4841 mapped-contact caller, retaining all checks and receipts.",
+  "scope_change_reason": "The runtime card is refined to the complete retained PR4841 contact-distance caller and its measured literal intersection bottleneck.",
+  "bottleneck_link": "This verifier-engineering side result removes measured exponential subspace enumeration from a complete native-contact replay; it does not improve the paid supplier invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified complete-caller improvement; do not optimize other caller phases.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; verify.py; benchmark.py emits timed complete-caller receipts and SHA256 bindings outside the checkout.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a basis-only contact ABI eliminate materialization of complete subspaces at the caller boundary?",
+      "why_it_matters": "The current adapter still pays for span construction and validates full input sets.",
+      "first_step": "Define a separate bounded basis contract and compare the complete graph caller, including basis validation.",
+      "blocked_by": "This changes the source interface and is outside the first-improvement scope."
+    }
+  ],
+  "question_source": {
+    "pr": 4841,
+    "author": "Dugongue",
+    "role": "Retained implementation and geometric predicates; the performance question is newly posed."
+  }
+}

research/rank-contact-replay/VERIFY.json

@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/native-clifford-gauge-compiler/NOTICE.md",
+    "research/native-clifford-gauge-compiler/decoder/TRANSVECTION-EXPECTED.json",
+    "research/native-clifford-gauge-compiler/decoder/testformula.py",
+    "research/native-clifford-gauge-compiler/inputs/round3-contact-graph.txt"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Replacement versus literal intersections, invalid inputs, one-contact cache and complete retained caller"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "The same complete conformance and caller checks with optimization enabled"
+    }
+  ]
+}