Cursor/pr6030 precision envelope mass 7270

research/pr6030-precision-envelope-mass/PROOF.md

@@ -0,0 +1,68 @@
+# Complete-envelope exponent of the selected PR6030 review
+
+Assumption ID: `precision_tape`. This is a scoped identity for the published
+envelope. It is not a proof of that assumption.
+
+## Data
+
+Let `H` be `complete_cost.paid` in
+`research/p104-helper470-twin-rung-removal/RESULT.json`, and let `T` be
+`complete_cost.targets`. Write `R(H) = Σ r n_r` and `N(H) = Σ n_r`.
+
+Direct evaluation gives
+
+- `R(H) = 240152` and `N(H) = 66834`;
+- `R(T) = 240912` and `N(T) = 13444`;
+- `R(T) - R(H) = 760`, equal to `rank_mass_surplus`.
+
+The same file records `nonrecursive.raw_budget = 10^9`,
+`nonrecursive.raw_scalar_upper = 184647552`, and
+`nonrecursive.local_paid_rank_mass = 5952`. The local mass is the
+nonrecursive note's growth coefficient. It is not `R(H)`.
+
+The application review
+`docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md` states the
+paid rank mass `240,152`, the productive rank mass `240,912` with surplus
+`760`, the caller bound `126,626,680`, the allowance `184,647,552 < 10^9`,
+and the envelope `2^(10^9+240152f)`.
+
+## Lemma
+
+Let a product contain elementary factors whose coordinate row-l1 majorants
+are at least 1. Suppose at most `B` of them are non-Gaussian and each has
+majorant at most 2, and suppose the Gaussian factors have ranks `r_i` with
+`Σ r_i = R` and majorant at most `2^(r_i f)` for an integer `f ≥ 0`.
+
+Then every subproduct has row-l1 majorant at most `2^(B + R f)`.
+
+Proof. Pass to base-2 logarithms of the majorants. Each logarithm is a
+nonnegative integer, the non-Gaussian logarithms sum to at most `B`, and the
+Gaussian logarithms sum to at most `R f`. The logarithm of a subproduct is
+at most the sum of the logarithms of its factors, hence at most the sum of
+every logarithm. Nonnegativity is necessary: majorants `2` and `1/2` have
+logarithms `1` and `-1`, the full sum is `0`, and the first factor alone
+has logarithm `1`.
+
+## Application to the published sentence
+
+Take `B = 10^9` and `R = R(H) = 240152`. The lemma's conclusion is exactly
+the published envelope `2^(10^9+240152f)`.
+
+The review also states a caller bound `C = 126626680` and an allowance
+`A = 184647552`, with `C < A < 10^9`. The differences are
+
+- `10^9 - C = 873373320`;
+- `10^9 - A = 815352448`.
+
+Under the same majorant hypotheses with `B = C` instead of `B = 10^9`, the
+lemma would give `2^(126626680+240152f)`, smaller than the published
+envelope by exactly `2^873373320`, for every `f`. The review states `C` and
+still writes the budget exponent. This note does not replace `10^9` by `C`.
+
+## Not established
+
+The lemma's majorant hypotheses are not proved for the selected caller.
+`RESULT.json` does not count non-Gaussian factors. The review's next
+sentences keep COPY residuals and the owned-erasure premise outside this
+exponent. Nothing here discharges `precision_tape`, `native_all_columns`,
+`owned_erasure`, `compiler`, or `analytic_recovery`, and κ is unchanged.

research/pr6030-precision-envelope-mass/README.md

@@ -0,0 +1,82 @@
+# PR6030 precision envelope uses the complete paid rank mass
+
+**Scoped identity; no new κ.** Assumption ID `precision_tape`, card
+`uniform-transfer-audit`. On the selected PR6030 invoice, the application
+review's coordinate envelope `2^(10^9+240152f)` is `2^(B + R f)` where
+`R = 240152` is the complete paid rank mass and `B = 10^9` is the recorded
+raw budget. The recounted caller bound is not the exponent that sentence uses.
+
+This does not prove the majorants, so it does not discharge `precision_tape`.
+
+## Scope and evidence
+
+Original card: `uniform-transfer-audit`. Scope status: **refined**. The card
+asks for one assumption and one caller-bound implication. The implication
+checked here is the published envelope's exponent, not a universal precision
+theorem. [#5625](https://github.com/CrocSwap/integer-mult-bounds/pull/5625)
+row reentry and [#5707](https://github.com/CrocSwap/integer-mult-bounds/pull/5707)
+root-prefix lowering stay partial interfaces; neither is treated as a
+discharge of the five selected assumptions.
+
+The proof is in [PROOF.md](PROOF.md). Pins are in [SOURCES.json](SOURCES.json).
+
+The complete histogram `complete_cost.paid` in
+`research/p104-helper470-twin-rung-removal/RESULT.json` has rank mass
+`240152` and `66834` calls. `complete_cost.targets` has rank mass `240912`
+and `13444` fields. The surplus is `760`. Those are the figures named in
+`docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md`.
+
+`nonrecursive.local_paid_rank_mass` is `5952`. The nonrecursive growth note
+tells a reader to use that local mass for the whole word. That coefficient
+does not reproduce the published envelope. The envelope matches the expanded
+histogram.
+
+`nonrecursive.raw_budget` is `10^9`. The review's caller bound
+`126,626,680` and allowance `184,647,552` are strictly smaller. Spending the
+budget instead of the caller bound leaves an exponent slack of `873373320`,
+so the published envelope is larger by `2^873373320` than the same lemma
+with the caller bound in the exponent. The review states the caller bound
+and still writes `10^9`.
+
+## Reproduce
+
+Python 3.12, standard library, from the repository root:
+
+```sh
+python3 -I -B research/pr6030-precision-envelope-mass/verify.py
+python3 -I -O -B research/pr6030-precision-envelope-mass/verify.py
+python3 -B scripts/research_package.py --package research/pr6030-precision-envelope-mass
+```
+
+The verifier prints `PASS_PR6030_PRECISION_ENVELOPE_MASS` with
+`paid_rank_mass=240152`, `caller_slack=873373320`,
+`precision_tape_discharged=false`, and `no_new_kappa=true`. Checks raise
+exceptions, so `-O` does not disable them.
+
+`python3 -B scripts/research_selected_baseline.py` is orientation only. It
+is not a supplier replay. No Lean, Docker, or `make frontier6030-verify`
+run was part of this package.
+
+## Open next questions
+
+1. Do the selected caller's scalar and dyadic factors have row-l1 majorant
+   at most 2, and its rank-`r` Gaussians majorant at most `2^(r f)`, with
+   every majorant at least 1? The exponent identity applies to the caller
+   only under those bounds. First step: one scalar ADD and one rank-`r`
+   Gaussian, including a COPY into a nonzero residual. Blocked by the
+   inherited `precision_tape` and `owned_erasure` premises.
+2. Can `10^9` in this sentence be replaced by `126626680`? That would shrink
+   the envelope by `2^873373320` for every `f`. First step: count
+   non-Gaussian elementary factors in the admitted caller. Blocked because
+   the pinned invoice does not contain that count.
+
+## Credit
+
+The invoice is DreamingOfClouds' PR6030 package
+`research/p104-helper470-twin-rung-removal`. The envelope sentence is the
+PR6030 application review by Douglas Colkitt with OpenAI Codex assistance.
+Ali Romman, Mason Hale, Pierre-Loic Doulcet, Matarener, Chris R /
+Clear1nsight, and the retained native, compiler, and analytic lineage keep
+the credit recorded in that review.
+
+Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0.

research/pr6030-precision-envelope-mass/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md",
+      "usage": "input",
+      "git_blob": "26f2f6324bce57e69e861d2aae5a27c9de325a8e",
+      "sha256": "8bd158b8ef68202000f167b9b78db0b31531b5b067b5cbd91b5bf35f3ddd1ab6"
+    },
+    {
+      "path": "research/p104-helper470-twin-rung-removal/RESULT.json",
+      "usage": "input",
+      "git_blob": "e4a03118d585fb80c9ac932281b528ac394ccc5f",
+      "sha256": "84fcbe2a0b64307b5703c363408042bdd91555b0419509aa50daa43b3b1924ad"
+    }
+  ]
+}

research/pr6030-precision-envelope-mass/TASK.json

@@ -0,0 +1,89 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "On the selected PR6030 invoice, the published precision_tape envelope 2^(10^9+240152f) is the complete paid rank mass times f, plus the raw budget 10^9. This identifies that constant. It does not prove the majorants or discharge precision_tape.",
+  "scope_change_reason": "The card asks for one assumption ID and one quantified implication at the actual caller. This fixes precision_tape's published complete-envelope exponent on the PR6030 complete paid histogram. It does not treat #5625 or #5707 as a discharge of any of the five assumptions, and it does not prove native_all_columns, owned_erasure, compiler, or analytic_recovery.",
+  "bottleneck_link": "The selected conditional supplier is admitted only under precision_tape. The published coordinate envelope is the precision statement the application review actually uses. Binding its exponent to the complete paid rank mass shows which invoice quantity it spends, and that the recounted caller bound is not the exponent it claims.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the envelope identity and the nonnegative-majorant subproduct lemma. Do not prove the scalar or Gaussian majorants, and do not start a second assumption.",
+  "outcome": "completed",
+  "evidence": "research/pr6030-precision-envelope-mass/verify.py prints PASS_PR6030_PRECISION_ENVELOPE_MASS with paid rank mass 240152, raw budget 1000000000, and caller-bound slack 873373320.",
+  "author": "unpaidmoon",
+  "ai_assistance": "Cursor Grok assisted with the audit, verifier, and write-up.",
+  "open_questions": [
+    {
+      "question": "Does every non-Gaussian elementary factor of the selected PR6030 caller have coordinate row-l1 majorant at most 2, and every rank-r Gaussian majorant at most 2^(r f), with every majorant at least 1?",
+      "why_it_matters": "Those four bounds are the hypotheses that turn the paid rank mass and the raw budget into the published envelope. Without them the exponent identity does not apply to the caller.",
+      "first_step": "Bind one scalar ADD and one rank-r Gaussian in the admitted caller event list to those majorants, including a COPY implemented as ADD into a nonzero residual.",
+      "blocked_by": "The inherited precision_tape and owned_erasure premises. The review states both and does not prove them."
+    },
+    {
+      "question": "Can the same majorant argument replace 10^9 by the recounted caller bound 126626680?",
+      "why_it_matters": "That replacement would shrink the published envelope by exactly 2^873373320, independent of f. The review states the caller bound and still spends the raw budget.",
+      "first_step": "Count the non-Gaussian elementary factors in the admitted caller and compare that count with 126626680 and with 184647552.",
+      "blocked_by": "No source-bound factor count is in the pinned invoice. The caller bound in the review is not by itself that count."
+    }
+  ]
+}

research/pr6030-precision-envelope-mass/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md",
+    "research/p104-helper470-twin-rung-removal/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "SHA256 pins; complete paid histogram rank mass 240152 and 66834 calls; productive mass 240912, 13444 fields, surplus 760; envelope sentence uses 10^9 plus that mass; raw budget 10^9 strictly above allowance 184647552 and caller bound 126626680; nonnegative subproduct lemma on a scalar, a monomial, and one rank-3 Gaussian; negative-exponent prefix counterexample; one-call histogram mutant misses 240152."
+    }
+  ]
+}