Independently check #4623's monotone extension, decoder rank and idle-free controller; sharpen ceiling to C≥.005687/.006512 (no new κ)

research/pr4623-monotone-decoder-check/README.md

@@ -0,0 +1,107 @@
+# Independent check of #4623: monotone extension, copied-input decoder, idle-free controller (no new κ)
+
+**No new κ and no supplier admission.** This is a scoped independent check of
+three parts of dillona's [PR #4623](https://github.com/CrocSwap/integer-mult-bounds/pull/4623)
+(head `fd5d3be12b9d6ee92c8fa089d95bd529c3236563`; canonical discussion
+[#4611](https://github.com/CrocSwap/integer-mult-bounds/discussions/4611)) that
+pinterbanget's [#4625](https://github.com/CrocSwap/integer-mult-bounds/pull/4625)
+did not replay. Nothing is imported from #4623 or #4625. Card: `independent-moment`.
+
+## Scope
+
+1. **(A) Monotone extension** (BUDGET.md): a negative bound at C=.006 (complex) and C=.007 (BIT)
+   implies negativity for every larger saving C ≤ 1, for every positive integer p.
+2. **(B) Copied-input X decoder** (DECODER.md): the exact correction identity, the forced
+   matrices and rank p−1, and the all-concave-moment cumulative certificate.
+3. **(T) Sanity**: deleting every whole IDLE call from the source chronology and thinning
+   stages 2,4,…,2p−2 gives exactly the stated triangular `Q^-1 U` / `Q V` controller, with
+   a degree-(p−1) diagonal border.
+
+## Result: agreement on all three, plus a sharpened ceiling
+
+**(A) holds.** Write h(t)=Σ_r s_r r^t (s = local helpers − local paid) and
+J_p(t) = (p+2)h(t) − v(p−1) + 2vp(1+b+2b/p)^t (the Jensen envelope of the 2vp main outputs
+whose determinant-forced total rank is 2v[p+b(p+2)]; valid as x^t is concave for t∈[0,1]).
+*Lemma.* If σ>0 and every summand c·r^t of J_p satisfies c·(r−σ) ≥ 0, then
+d/dt[c(r/σ)^t] = c·ln(r/σ)(r/σ)^t ≥ 0, so J_p(t)/σ^t is nondecreasing on [0,1];
+hence J_p(t₀)<0 implies J_p(t)<0 for all t≤t₀, i.e. every C ≥ 1−t₀.
+The hypothesis is p-independent: the signed local profile is
+complex {1:−2237, 2:−388, 3:−494, 4:−119, 5:−36, 7:+7, 8:+39, 9:+326} and
+BIT {1:−1323, 2:−1342, 3:−79, 4:−44, 5:−102, 6:−11, 7:−19, 8:+439}; coefficients (p+2)s_r keep
+their sign; the thin queries are a negative rank-1 term; the main base 1+b+2b/p > 1+b.
+So any σ in (5,7] (complex) or (7,8] (BIT) works; #4623's σ=6 and 15/2 are valid.
+Combined with J_p(t₀) ≤ pA(t₀)+B_J(t₀) (tangent at 1+b), and A, B_J < 0 at the cutoffs,
+the exclusion holds for all p ≥ 1 and all C ∈ [cutoff, 1]. My certified intervals
+(exp/log series with explicit remainder bounds, outward rounding to 2⁻¹²⁰) reproduce
+A = −2.6366097978, B_J = −132.6282065738 (complex, .006) and A = −3.5731057049,
+B_J = −133.1717283853 (BIT, .007), widths < 2·10⁻²⁹.
+
+**Sharpening (new, scoped).** The cutoffs are not tight for this model. Certified:
+A<0 and B_J<0 already at **C = .005687 (complex)** and **C = .006512 (BIT)**, so the same
+argument excludes C ≥ .005687 / C ≥ .006512 for every p. Conversely A>0 at C=.005685 /
+.006510; since J_p(t)/p → A(t) as p→∞, the optimistic J_p is positive for large p there,
+so this relaxation cannot exclude smaller savings. The model's sharp all-p threshold is in
+(.005685, .005687) complex and (.006510, .006512) BIT. This is a ceiling, not a supplier.
+
+**(B) holds in the stated model.** Using the emitted idle-free X block,
+z = (I+J)X' − Q⁻¹Jx equals Q⁻¹Dx exactly (p=2..7). Solving M(I−S)=I, N=−MS exactly gives
+M=I+J, N=−J, rank p−1 (p=2..7). The cumulative rank sums A_r(p) of (paid − target), with
+p−1 fresh rank-one correction queries per port, are affine in p and reproduce DECODER.md's
+base/slope table for every listed threshold (e.g. complex r=1: 9172+2461(p−2); r=17: 32+64(p−2);
+BIT r=15: 30+63(p−2)); all bases and slopes are positive, so Abel summation with
+f(r)=r^(t−1) gives paid > target at every t∈(0,1] and p≥2. Direct certified moment
+evaluation agrees at p∈{2,16}, t∈{.01,.5,1}.
+
+**(T) holds.** My hand replay of the source chronology (F_s = D_s S_y(Q⁻¹), B_s = D_s S_x(−Q),
+bridges, reverse bridges, signed swap; IDLEs deleted; thin stages without D_s) equals both
+the closed form U, V of DISCOVERY.md and the literal pinned source emitter
+(`complex_controller_factor.controller(p, 0)` with thin exponents zeroed), coefficient by
+coefficient, for p=1..7. Weights w(X_j)=j, w(Y_j)=p−1−j give border degree set exactly
+{0,…,p−1}, all diagonal entries are unit monomials (so the limit is the full-rank diagonal
+monomial map), det = Π_{thick s} D_s² (p+2 thick stages), and A(1)=I.
+
+## Controls (all rejected as required)
+
+Tampered input bytes; flipped backward-shear sign; no thinning; reversed weights (negative
+degrees); a net-negative rank-9 paid term (breaks the separator lemma); non-certification at
+complex C=.005 and BIT C=.006 (checker is not vacuous); decoder without fresh queries (some
+cumulative sum negative); decoder without the raw-input term (identity fails).
+
+## Reproduce
+
+```sh
+python3.12 scripts/research_package.py --package research/pr4623-monotone-decoder-check --check-only
+python3.12 scripts/research_package.py --package research/pr4623-monotone-decoder-check
+python3.12 -B research/pr4623-monotone-decoder-check/verify.py
+```
+
+Standard library only; about 2 s.
+
+## NOT covered
+
+- The precision/approximation lemma (EXACTIFICATION.md) and the H₀(f) budget.
+- The repeated whole-controller (K≥2) argument; the determinant/Laurent rank-mass invariant
+  itself (taken as stated; #4625 checked the p16 masses).
+- Whether the frozen #4470/BIT inventories and the "thin stage = unscaled shear" modelling
+  are the right physical contract; any BIT scalar-extension or native implementation.
+- Decoder lower bound beyond the stated model (shared/reused internal queries, cross-port or
+  operator-valued adapters). Controller sanity was checked only for p=1..7, not symbolically.
+- #4625 already performed a sign check of the separator premise; this package adds the
+  derivation, a different certified enclosure, the maximal separator ranges and the sharpening.
+
+## Open next questions
+
+- **Does the sharpened ceiling (C* ≈ .005686 complex / .006511 BIT) bind the actual diagonal
+  family as p→∞?** It matters because it is the true limit of this idle-free interface under the
+  frozen inventories. First step: certify the explicit-diagonal roots pA+B for p up to 2¹⁰ and show
+  they increase to C*. Blocked by: nothing.
+- **Can the p−1 paid thin queries be reused as the decoder's Q⁻¹x_(i+1) values?** It is the only
+  route #4623 leaves open for exact X correction. First step: a chronological ownership/restoration
+  check at p=2. Blocked by: an explicit retained-query contract in the source interface.
+
+## Credit
+
+dillona (Dillon) for #4623 and its proofs; pinterbanget for #4625; Matarener for #4602's idle-bill
+diagnosis; Cinna Davis (1337isnot1337) for #4440/#4470; zxv and the native/BIT controller lineage
+for the source emitter and inventories. Prepared by lm1909 with Claude Code (Claude Opus 5.5)
+assistance. No independent human review. Apache-2.0.

research/pr4623-monotone-decoder-check/SOURCES.json

@@ -0,0 +1,57 @@
+{
+  "schema_version": 1,
+  "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/joint-helper-lattice/RESULT.json",
+      "usage": "input",
+      "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596",
+      "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/complex_controller_factor.py",
+      "usage": "input",
+      "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947",
+      "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497"
+    },
+    {
+      "path": "research/query-thinned-controllers/BIT-CONTROLLER.json",
+      "usage": "input",
+      "git_blob": "89c400d5970024b3debe870c36ce43889beed001",
+      "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d"
+    },
+    {
+      "path": "research/controller-border-interface/BUDGET.md",
+      "usage": "provenance",
+      "git_blob": "e58271a6145d84478326db867b487ee959a3d6ec",
+      "sha256": "10c878e928d390c0101900a60b8ab5ec51d62d514c9ad214cd74ca4733389dbd",
+      "pin": "head:fd5d3be12b9d6ee92c8fa089d95bd529c3236563:research/controller-border-interface/BUDGET.md"
+    },
+    {
+      "path": "research/controller-border-interface/DECODER.md",
+      "usage": "provenance",
+      "git_blob": "1d656c2279a8e31d65e86f602bcb5401c07dc20b",
+      "sha256": "d921f6795602867e29e351972eb1239e6f940e406656c2ebab9cc15c95d38471",
+      "pin": "head:fd5d3be12b9d6ee92c8fa089d95bd529c3236563:research/controller-border-interface/DECODER.md"
+    },
+    {
+      "path": "research/controller-border-interface/DISCOVERY.md",
+      "usage": "provenance",
+      "git_blob": "745cf3dfa6c3091aa899b476a5e80284337c6a23",
+      "sha256": "b19edaa4764cb69f94488ad1cba979e1e6fa79ab621b1437ea7037d2beef23eb",
+      "pin": "head:fd5d3be12b9d6ee92c8fa089d95bd529c3236563:research/controller-border-interface/DISCOVERY.md"
+    }
+  ]
+}

research/pr4623-monotone-decoder-check/TASK.json

@@ -0,0 +1,106 @@
+{
+ "schema_version": 1,
+ "task_id": "independent-moment",
+ "priority_revision": 7,
+ "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d",
+ "original_card": {
+  "id": "independent-moment",
+  "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+  "starting_points": [
+   "docs/research/research-family-status.md",
+   "certificates/selected-result.json",
+   "research/staged544-mixed-fourth-entry/README.md",
+   "research/staged-fourth-mixture-ceiling/README.md",
+   "research/r437-two-window-carrier/README.md"
+  ],
+  "methods": [
+   "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.",
+   "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls."
+  ],
+  "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+  "first_step": {
+   "command": [
+    "python3",
+    "-B",
+    "scripts/research_baseline.py"
+   ],
+   "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+   "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.",
+   "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+  },
+  "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.",
+  "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+  "allowed_variations": [
+   "Reconstruct either a source ledger or a numeric enclosure with a different method."
+  ],
+  "scope_change_triggers": [
+   "Importing the primary function and calling its output independent verification.",
+   "Calling an aggregate histogram or source archive an independently accepted physical supplier."
+  ],
+  "overlap_terms": [
+   "independent moment",
+   "rank histogram",
+   "exact enclosure",
+   "2979",
+   "rank7 joint endframes",
+   "paired extraction",
+   "joint lowering",
+   "4088",
+   "4091",
+   "4067",
+   "staged544-mixed-fourth-entry",
+   "staged-fourth-mixture-ceiling",
+   "r437-two-window-carrier"
+  ],
+  "existing_checks": [
+   {
+    "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.",
+    "evidence": "research/staged544-mixed-fourth-entry/README.md",
+    "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.",
+    "status": "author-checked",
+    "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0",
+    "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+   },
+   {
+    "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.",
+    "evidence": "research/staged-fourth-mixture-ceiling/README.md",
+    "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.",
+    "status": "author-checked",
+    "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4",
+    "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+   },
+   {
+    "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.",
+    "evidence": "research/r437-two-window-carrier/README.md",
+    "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.",
+    "status": "author-checked",
+    "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e",
+    "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+   }
+  ]
+ },
+ "scope_status": "unchanged",
+ "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?",
+ "scope_change_reason": null,
+ "bottleneck_link": "Independent coverage of #4623's controller-level idle-deletion ceiling (monotone extension), decoder barrier and controller algebra; prevents an unsupported interface campaign.",
+ "budget_minutes": 60,
+ "stop_rule": "Stop after (A) monotone extension, (B) decoder rank/all-moment certificate and (T) small-p controller sanity; precision lemma left uncovered.",
+ "outcome": "completed",
+ "evidence": "Separator lemma holds for sigma in (5,7] complex / (7,8] BIT; certified A,B_J<0 at .006/.007 reproduce #4623; sharpened exclusion at C>=.005687 complex / .006512 BIT with A>0 at .005685/.006510. Decoder: M=I+J, N=-J, rank p-1, cumulative table reproduced, all positive. Idle-free emitter = closed form = literal source for p=1..7, border degree p-1, det prod D_s^2.",
+ "author": "lm1909",
+ "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.",
+ "open_questions": [
+  {
+   "question": "Does the sharpened ceiling C* (~.005686 complex, ~.006511 BIT) bind the explicit-diagonal family as p grows?",
+   "why_it_matters": "It is the exact limit of the idle-free interface under the frozen inventories.",
+   "first_step": "Certify pA+B roots for p up to 2^10 and show monotone convergence to C*.",
+   "blocked_by": "Nothing."
+  },
+  {
+   "question": "Can the p-1 paid thin queries be reused as the decoder's Q^-1 x_(i+1) values?",
+   "why_it_matters": "It is the remaining route to exact X correction without p-1 fresh queries per port.",
+   "first_step": "Chronological ownership/restoration check at p=2.",
+   "blocked_by": "An explicit retained-query contract in the source interface."
+  }
+ ]
+}

research/pr4623-monotone-decoder-check/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/joint-helper-lattice/RESULT.json",
+    "research/kappa-rebuild/bit/complex_controller_factor.py",
+    "research/query-thinned-controllers/BIT-CONTROLLER.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Input sha256 pins; separator lemma and certified A,B_J<0 at cutoffs and sharpened cutoffs; decoder identity/forced rank/cumulative certificate; idle-free controller = closed form = literal source p=1..7; 9 rejection controls."
+    }
+  ]
+}