Audit historical follow-up supplier saving bindings

research/followup-supplier-binding-audit/EXPECTED.json

@@ -0,0 +1,21 @@
+{
+  "scope": "Historical standalone arithmetic acceptance lacks supplier saving equality; no CI bypass or producer-realizability claim.",
+  "original_fixed_receipt": "PASS",
+  "mutant_standalone_arithmetic": "PASS",
+  "mutant_fixed_receipt": "REJECT receipt mismatch",
+  "declared_complex_saving": "717/20000000",
+  "assembly_complex_saving": "717/10000000",
+  "declared_complex_moment_upper": "999993150031878243958187118629/1000000000000000000000000000000",
+  "independent_consumed_complex_moment_lower": "26765333515773650919263739596637204910737789925011211291357805254654977698386099774783307392176336271487032619290723599762754969869775548808376248427067782213/26765333504000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "consumed_moment_excess_lower": "11773650919263739596637204910737789925011211291357805254654977698386099774783307392176336271487032619290723599762754969869775548808376248427067782213/26765333504000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000",
+  "strict_excess_threshold": "1/2500000000",
+  "guard_controls": {
+    "original": "PASS",
+    "complex_mismatch": "REJECT",
+    "bit_mismatch": "REJECT",
+    "equivalent_rationals": "PASS",
+    "consistent_noncontracting": "PASS binding only"
+  },
+  "consistent_noncontracting_historical_arithmetic": "REJECT complex moment does not contract",
+  "bit_mismatch_historical_arithmetic": "PASS"
+}

research/followup-supplier-binding-audit/README.md

@@ -0,0 +1,162 @@
+# Historical follow-up supplier saving binding audit
+
+The historical PR49 arithmetic checker accepts a candidate whose complex
+supplier moment contracts at `717/20000000`, while its assembly still consumes
+`a_complex = 717/10000000`. For the same supplied child counts, an independent
+exact rational lower bound proves that the moment at the consumed saving is
+**greater than `1 + 4/10^10`**. The missing implication is equality between the
+checked supplier saving and the assembly parameter.
+
+This is a scoped audit of standalone arithmetic acceptance. The unmodified
+original certificate passes its original fixed receipt. The existing
+`--check docs/research/community-followup-arithmetic.json` check **already rejects
+the mutant** because the receipt binds the certificate bytes. This finding is
+not a CI bypass, a counterexample to the original witness, a validated finite
+construction, or a change to the selected result or multiplication theorem.
+
+## Concrete counterexample and controls
+
+`verify.py` reads the exact historical checker, arithmetic dependency,
+certificate and saved receipt from the Git commit recorded in `SOURCES.json`.
+It authenticates their Git blob IDs and SHA256 values before reconstructing
+those files in a disposable directory. All seven source rows are historical
+provenance; no evolving root helper is a live input. Full Git history containing
+the base commit is required. Future repairs of the root helper do not invalidate
+this historical reproduction.
+
+Starting with the pinned `research/climbed-48/certificate.json`, the complex
+counterexample changes exactly two JSON values:
+
+| Field | Original | Mutant |
+|---|---:|---:|
+| Last `complex.child_width_multiplicities` row | `[756, 516232080]` | `[756, 516232085]` |
+| `complex.saving` | `717/10000000` | `717/20000000` |
+
+The assembly parameter stays `717/10000000`. The complex denominator constants
+stay `m = 784`, `W = 537696432`. Counts are positive integers and all child ranks
+satisfy `0 < r < m`; this establishes the arithmetic domain only. The counts
+are supplied inputs, **not claimed to arise from the retained finite producer**.
+Other cached certificate fields are left unchanged and are not claimed to be
+producer-consistent.
+
+The historical CLI prints its ordinary PASS for the mutant. Its recomputed
+upper bound at the weaker saving is below one (approximately
+`0.9999931500318783`). The independent consumed-saving lower bound is above one
+(approximately `1.0000000004398843`). Approximate decimals are explanatory;
+`EXPECTED.json` contains the exact rational evidence and is checked on replay.
+
+The bounded replay executes these controls as real Python CLI processes:
+
+- Original historical checker with its fixed receipt passes and produces the
+  same parsed receipt; the optional guard also passes.
+- Mutant historical checker without `--check` passes, but the fixed receipt
+  check rejects it with `receipt mismatch`; the guard rejects `a_complex` mismatch.
+- An original certificate with only `assembly.parameters.a_bit = 1/100000`
+  still passes the historical arithmetic checker; the guard rejects the mismatch.
+- Equivalent rational spellings for both assembly savings pass the guard.
+- Restoring equality in the complex mutant makes the guard pass, while the
+  historical checker rejects `complex moment does not contract`. Equality is a
+  necessary binding check, not sufficient arithmetic validation.
+
+`guard.py` is an **opt-in** check of exactly the two rational equalities
+`bit.saving == assembly.parameters.a_bit` and
+`complex.saving == assembly.parameters.a_complex`. Its success marker is
+`PASS_SUPPLIER_SAVING_BINDING_ONLY`. It does not run the arithmetic checker or
+validate finite counts, all assembly parameters, or transfer hypotheses.
+Production entry points remain unchanged. A direct helper edit would invalidate
+live byte pins in `mixed-demotions-t37` and `mixed-fusions-x54-t37`; their frozen
+files are preserved.
+
+## Independent lower-bound argument
+
+For the supplied positive counts `c_r`, define
+
+\[
+M(a)=\sum_r\frac{c_r}{W}\left(\frac r m\right)^{1-a}
+=\sum_r\frac{r c_r}{mW}\exp\left(a\log\frac m r\right).
+\]
+
+The verifier checks positive integer `m,W,c_r`, `0 < r < m`, and `0 < a < 1`.
+For each `x=m/r`, divide by powers of two to obtain `x=2^k y` with
+`1 <= y <= 2`. For `t=(y-1)/(y+1)` we have `0 <= t <= 1/3`, and
+
+\[
+\log y=2\sum_{j=0}^{\infty}\frac{t^{2j+1}}{2j+1}
+\ \ge\ 2\sum_{j=0}^{23}\frac{t^{2j+1}}{2j+1}.
+\]
+
+Every omitted term is nonnegative and the series converges because `t < 1`.
+Use the same 24-term sum for `log 2`, multiply by `k`, and add. Rounding this
+rational lower bound **down** on the `10^30` grid preserves a nonnegative lower
+bound `L <= log(m/r)`. Hence `z=aL >= 0` and monotonicity plus the positive
+exponential series gives
+
+\[
+\exp(a\log(m/r))\ge\exp(z)\ge 1+z+z^2/2+z^3/6+z^4/24.
+\]
+
+All weights `r c_r/(mW)` are positive, so their weighted polynomial sum is a
+rigorous lower bound for `M(a)`. No floating point and no historical log/exp
+function is used in this independent computation. In particular, this is a
+positive-exponent expansion after the displayed identity, not a truncation of
+an alternating series at `(1-a)log(r/m)`. Exact `Fraction` comparison proves
+that the computed lower bound exceeds `1+4/10^10` for `a=717/10000000`.
+
+## Reproduction
+
+Python 3.12, Git, and the standard library are sufficient. From the repository
+root with the source history available:
+
+```sh
+python3.12 -B research/followup-supplier-binding-audit/verify.py
+python3.12 -O -B research/followup-supplier-binding-audit/verify.py
+python3.12 -B scripts/research_package.py --package research/followup-supplier-binding-audit --check-only
+python3.12 -B scripts/research_package.py --package research/followup-supplier-binding-audit
+```
+
+Both verifier modes require `PASS_FOLLOWUP_SUPPLIER_BINDING_AUDIT_ONLY` and compare
+all evidence to `EXPECTED.json`. Explicit checks remain active under `-O`; the
+historical child processes receive the same optimization level and private
+bytecode-cache namespace. Replay only uses temporary fixtures. No finite-count
+producer, historical all-package suite, Lean build, or selected cold replay is
+run. To apply only the opt-in binding guard to a separate candidate:
+
+```sh
+python3.12 -B research/followup-supplier-binding-audit/guard.py path/to/certificate.json
+```
+
+## Task, overlap and attribution
+
+Base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6.
+`TASK.json` retains the exact `portable-replay` card and declares **refined**
+scope: its proof-relevant field-comparison method is applied to supplier and
+assembly savings. This is a verifier side result, not an environment fix or a
+new construction.
+
+The pinned maintainer [PR49 review](../../docs/research/community-followup-review.md)
+credits **Rohan Arun** and candidate head
+`f95d2910e027495983b53cae1693cf535abf2569`, building on PR48. The historical
+independent arithmetic checker and its PR39 rational enclosure dependency retain
+**Douglas Colkitt's** attribution. The scope and original receipt are preserved.
+[PR1329](https://github.com/CrocSwap/integer-mult-bounds/pull/1329) concerns retained
+PR589 supplier identity and COPY deficit; it does not establish these PR49
+saving equalities. The current handoff/PR overlap scan found no equivalent
+PR49 arithmetic binding audit; absence of a match is not a universal novelty claim.
+
+Audit and opt-in guard by **roger-sato**, with substantial **OpenAI Codex** assistance
+in diagnosis, implementation, exact arithmetic, review and documentation.
+Apache-2.0, retaining predecessor attribution.
+
+## Open next questions
+
+Structured questions and blockers are in `TASK.json`.
+
+1. Integrate saving equality into a current arithmetic-checker entry point while
+   preserving frozen consumers. Start by choosing a non-frozen entry point or
+   source-preserving adapter, then replay the original-receipt and mismatch
+   controls. Maintainer selection of the integration surface and review of
+   dependent pins remain necessary; the optional guard is not production adoption.
+2. Audit one other consumed assembly parameter against its supplier evidence.
+   This matters because these two equalities do not prove complete binding.
+   Begin with one explicit dependency trace and check overlap before expanding
+   scope; finite-count production and the all-size transfer remain separate.

research/followup-supplier-binding-audit/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    },
+    {
+      "path": "docs/research/community-followup-arithmetic.json",
+      "usage": "provenance",
+      "git_blob": "55919f5cbef9549dd8bc656ede230a7af60d44d8",
+      "sha256": "88a00f3829705a0d70f9e73b1f5471a7e86e137e07a4c251e7d177763eec0743"
+    },
+    {
+      "path": "docs/research/community-followup-review.md",
+      "usage": "provenance",
+      "git_blob": "8048a13839e2d1481ac39ad91f1eff0e9f8730cb",
+      "sha256": "6be2b0f225ea1602824e7e21d3ad7397acb2d16fbfd0ed065fa3bb539753c3c7"
+    },
+    {
+      "path": "research/climbed-48/certificate.json",
+      "usage": "provenance",
+      "git_blob": "92dc457a500c3e3df1910012436bf2d0f0ba6dc3",
+      "sha256": "1118a869600f69898f6b078208dc0007af817e16de9e5696d6b8bda56574f19f"
+    },
+    {
+      "path": "scripts/audit_community_candidate.py",
+      "usage": "provenance",
+      "git_blob": "41176b012f4927b34d20fce65f085cecb72f64aa",
+      "sha256": "fe687e20639a26c852fcd336411636e5c4293c0d7ba1880cf570bcad2f9d6ac9"
+    },
+    {
+      "path": "scripts/audit_followup_candidate.py",
+      "usage": "provenance",
+      "git_blob": "a190d846e24adf332737687d7510576e1da93846",
+      "sha256": "dfb65258d08097acd6a4c29719f4d7459646801de56f33e78d9ae1cee55c2cfc"
+    }
+  ]
+}

research/followup-supplier-binding-audit/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "portable-replay",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "original_card": {
+    "id": "portable-replay",
+    "question": "Can one reproducible environment or artifact-comparison failure be repaired?",
+    "starting_points": [
+      "research/gzip-container-reproducibility/README.md",
+      "docs/ci-verification.md"
+    ],
+    "methods": [
+      "Reproduce one portability failure and add a minimal cross-environment fix.",
+      "Audit one canonical-payload comparison for omitted proof-relevant fields."
+    ],
+    "acceptance_gate": "Preserve immutable source hashes and proof-relevant content; a different compressed byte stream alone is not a mathematical mismatch.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the gzip-container reproducibility examples and distinguish frozen source bytes from regenerated payloads.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Reproduce one specific mismatch or audit one canonical comparison for omitted proof-relevant fields.",
+    "bottleneck_link": "Portable exact checks prevent environment failures from blocking valid contributions.",
+    "allowed_variations": [
+      "One interpreter/version mismatch or one payload field comparison."
+    ],
+    "scope_change_triggers": [
+      "Removing immutable-source pins because generated compressed bytes differ."
+    ],
+    "overlap_terms": [
+      "gzip container",
+      "reproducibility",
+      "canonical payload"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Audit the PR49 historical arithmetic checker for omitted supplier-to-assembly saving equality; reproduce a positive-domain arithmetic counterexample and supply an opt-in equality guard.",
+  "scope_change_reason": "Refine the portable-replay card's proof-relevant field-comparison method to a supplier/assembly parameter comparison. This is a scoped arithmetic audit, not an environment fix or a new construction.",
+  "bottleneck_link": "Proof-relevant parameter equality prevents a contracting supplier moment from being reused at an unchecked stronger assembly saving. This is a verifier side result; production integration remains open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after authenticated historical CLI reproduction, an independent exact consumed-moment lower bound, fixed-receipt controls, and a bounded equality guard. Do not rerun finite-count producers or change frozen helpers.",
+  "outcome": "completed",
+  "evidence": "EXPECTED.json records the actual historical CLI controls and an independent exact rational consumed-moment lower bound exceeding 1+4/10^10; verify.py replays every control normally and with -O.",
+  "author": "roger-sato",
+  "ai_assistance": "Substantial OpenAI Codex assistance with diagnosis, implementation, exact arithmetic, review, and documentation.",
+  "open_questions": [
+    {
+      "question": "How should production arithmetic-checker entry points enforce supplier saving equality without invalidating frozen consumers?",
+      "why_it_matters": "The package guard is opt-in; the historical helper remains unchanged because mixed-demotions-t37 and mixed-fusions-x54-t37 bind its live bytes.",
+      "first_step": "Design a current non-frozen entry point or a source-preserving adapter that runs the two rational equalities before arithmetic verification, with original-receipt and mismatched-saving controls.",
+      "blocked_by": "Maintainer choice of integration surface and review of dependent source pins. No frozen source identities should be rewritten."
+    },
+    {
+      "question": "Which additional supplier-to-assembly fields require independently checked semantic binding?",
+      "why_it_matters": "This audit covers only a_bit and a_complex; finite-count production, other parameters, and transfer hypotheses remain separate obligations.",
+      "first_step": "Trace one actual consumed parameter to its independently checked supplier evidence and propose a bounded control if equality is missing.",
+      "blocked_by": "Separate overlap and source-consumer review; no general completeness claim follows from this package."
+    }
+  ]
+}

research/followup-supplier-binding-audit/VERIFY.json

@@ -0,0 +1,28 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Authenticated historical CLI original and mutant controls, fixed-receipt rejection, exact independent consumed-moment lower bound, and opt-in equality guard controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same explicit checks and historical child CLI controls with assertions disabled."
+    }
+  ]
+}

research/followup-supplier-binding-audit/guard.py

@@ -0,0 +1,31 @@
+#!/usr/bin/env python3
+"""Opt-in supplier/assembly saving equality check, not a certificate verifier."""
+
+import argparse
+from fractions import Fraction
+import json
+from pathlib import Path
+
+
+def check_bindings(data):
+    for supplier in ("bit", "complex"):
+        saving = Fraction(data[supplier]["saving"])
+        parameter = "a_" + supplier
+        consumed = Fraction(data["assembly"]["parameters"][parameter])
+        if saving != consumed:
+            raise ValueError(f"{supplier}.saving does not match assembly.parameters.{parameter}")
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("certificate", type=Path)
+    args = parser.parse_args()
+    try:
+        check_bindings(json.loads(args.certificate.read_bytes()))
+    except (KeyError, TypeError, ValueError, ZeroDivisionError) as exc:
+        parser.exit(1, f"FAIL_SUPPLIER_SAVING_BINDING: {exc}\n")
+    print("PASS_SUPPLIER_SAVING_BINDING_ONLY")
+
+
+if __name__ == "__main__":
+    main()