Prove sharp minimum block length 112 for fixed tail gates (no κ)

research/p104-minimum-tail-block/ORIGINS.json

@@ -0,0 +1,29 @@
+{
+  "repository": "CrocSwap/integer-mult-bounds",
+  "pull_request": 5775,
+  "head": "56dc0a9ec02020f5e035c7d83f078fb2b27ac76a",
+  "files": [
+    {
+      "retained_path": "premises/RESULT.json",
+      "source_path": "research/p104-tail-feasible-envelope/RESULT.json",
+      "git_blob": "a30006be845abb830d4c9f953c828a4b2444fe0a",
+      "sha256": "bd8b2572ba9d64421dfef00440ae2f5e7f7d0c98875111e4d29ac4eb63e55531",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/56dc0a9ec02020f5e035c7d83f078fb2b27ac76a/research/p104-tail-feasible-envelope/RESULT.json"
+    },
+    {
+      "retained_path": "premises/PROOF.md",
+      "source_path": "research/p104-tail-feasible-envelope/PROOF.md",
+      "git_blob": "5611eb8f8611d9dd2c7748d163b0db540ebe2831",
+      "sha256": "39c32069071950dbbb65211c4b857291d92103d7801b70eec78667a0c8e397e7",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/56dc0a9ec02020f5e035c7d83f078fb2b27ac76a/research/p104-tail-feasible-envelope/PROOF.md"
+    },
+    {
+      "retained_path": "premises/INVOICE.json",
+      "source_path": "research/p104-tail-feasible-envelope/inputs/RESULT.json",
+      "git_blob": "9d47144bd99dc57d799345c940232eb26afdc33c",
+      "sha256": "062fb71b92ca620cbea4a4469458ede513e4dc1039bfa783e06ed11f51335a9e",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/56dc0a9ec02020f5e035c7d83f078fb2b27ac76a/research/p104-tail-feasible-envelope/inputs/RESULT.json"
+    }
+  ],
+  "use": "Cited mathematical premises, retained verbatim; predecessor theorem not replayed."
+}

research/p104-minimum-tail-block/PROOF.md

@@ -0,0 +1,124 @@
+# A sharp minimum block exponent
+
+## Statement and inherited premises
+
+Fix the complete PR5756 paid and target histograms `P_r,T_r`, with
+`C = 622627591/200000000000`, `t=1-C`,
+`T = sum_r T_r r^t`, and `N = sum_r T_r = 13390`. Define
+
+```text
+g(c,u) = sum_r P_r r^(t+u) / (c^u T),
+d(c,b) = N b / (c^C T).
+```
+
+The declared gate family has integers `L>=3`, `c>=1`, `b>=1`, real `u>0`,
+and rational `0<rho<1`. Its complete set of inequalities is
+
+```text
+g(c,u) < rho,
+d(c,b) < rho,
+rho^L < 1/16,
+c^L < b^(L-2).
+```
+
+For `L=128`, the last condition is equivalent to `c^64<b^63`, so this is
+exactly PR5775's two-tail/capacity subsystem. Allowing other `L` defines a
+new algebraic family. No compiler implementing it is assumed to exist.
+
+**Theorem.** Subject to the cited scalar premises below, this family is
+feasible exactly for integer `L>=112`. At `L=112`, its unique integer
+cutoff/floor pair is `(16,17)`. An explicit witness is
+
+```text
+L=112, c=16, b=17, u=1/7, rho=1951/2000.
+```
+
+The theorem remains true if `L` must be even or if `u` must be rational.
+
+Ali Romman's [PR5775](https://github.com/CrocSwap/integer-mult-bounds/pull/5775),
+head `56dc0a9ec02020f5e035c7d83f078fb2b27ac76a`, supplies these premises:
+
+| Quantity | Cited rational lower bound |
+| --- | --- |
+| `inf_{u>0} g(15,u)` | `983563652257169/1000000000000000` |
+| `inf_{u>0} g(16,u)` | `a = 487740894096357/500000000000000` |
+| `d(17,18)` | `999697814388247/1000000000000000` |
+| `d(16,18)` | `999886507972867/1000000000000000` |
+
+Each cited lower bound is strict and exceeds `a`, except the row defining
+`a` itself. The retained [result](premises/RESULT.json) and
+[proof](premises/PROOF.md) specify their scope. PR5775 also retains PR5756's
+[source invoice](premises/INVOICE.json), whose `strictification` records
+upper bounds for `g(16,1/7)` and `d(16,17)`. Exact comparison gives
+
+```text
+g(16,1/7) < 975485/1000000 < 1951/2000,
+d(16,17) < 945/1000 < 1951/2000.
+```
+
+These are cited mathematical premises, not independently rederived results
+of this package. `ORIGINS.json` binds the verbatim source bytes to their
+repository, head, paths, Git blobs and SHA256 hashes. Authentication does not
+prove the predecessor's mathematics. This contribution proves the new
+block-exponent consequence of those premises.
+
+## Exclusion of every smaller block
+
+The capacity inequality implies `b>=c+1`. Indeed, `b<=c` would give
+`b^(L-2)<=c^(L-2)<=c^L`, a contradiction.
+
+For fixed `u>0`, `g(c,u)` decreases with `c`. Thus every `c<=15` has
+`g(c,u)>983563652257169/1000000000000000>a`.
+
+The function `d(c,b)` increases with `b`. On real `c>=1`, the derivative of
+`(c+1)/c^C` has the sign of `(1-C)c-C`, which is positive since `0<C<1/2`.
+Consequently every `c>=17` and every capacity-compatible `b` has
+`d(c,b)>=d(17,18)>a`.
+
+For `c=16`, every `b>=18` has `d(c,b)>=d(16,18)>a`. The only remaining
+integer pair is `(16,17)`, and its paid tail is at least the cited infimum,
+which exceeds `a`. Therefore every capacity-compatible pair and every
+positive offset satisfy `max(g(c,u),d(c,b))>a`.
+
+The new exact integer comparison is
+
+```text
+16 * 487740894096357^111 > 500000000000000^111.
+```
+
+It says `a^111>1/16`. Since `0<a<1`, every integer `3<=L<=111` has
+`a^L>=a^111>1/16`. Any passing tail choice requires `rho>a`, hence
+`rho^L>1/16`. This contradicts the reserve gate. This argument covers all
+cutoffs, floors, offsets and decays in the declared model.
+
+## A passing block and all larger blocks
+
+The cited upper bounds give both tail inequalities for the displayed
+rational witness. The remaining new checks are integer comparisons:
+
+```text
+16 * 1951^112 < 2000^112,
+16^112 < 17^110.
+```
+
+These prove the strict reserve and capacity gates at length 112. For larger
+`L`, the same witness still works. Its reserve `rho^L` decreases, and its
+capacity ratio is `17^2*(16/17)^L`, which also decreases. The two tails are
+independent of `L` in the declared family. This proves the exact feasibility
+set, without an upper cutoff on `L`.
+
+At `L=112`, each of the other three cited lower bounds has its 112th power
+strictly greater than `1/16`. The same case split therefore excludes every
+integer cutoff/floor pair except `(16,17)` at the minimum.
+
+## Meaning and limits
+
+The new minimum is 16 below the predecessor's fixed length 128, a fractional
+shortening of `1/8` within this gate family. This is a parameter-existence
+result and a sharp obstruction below 112. It does not show that a complete
+compiler can use 112, reduce carrier height, preserve another gate, or earn
+a new exponent saving. Changing a block can change normalization, exit,
+rounding and nonrecursive charges. Those changes require a separate complete
+construction and bill. No source operator replay or predecessor audit is
+part of this proof, and no physical supplier or complete multiplication theorem
+follows.

research/p104-minimum-tail-block/README.md

@@ -0,0 +1,89 @@
+# Minimum block length 112 for a fixed two-tail gate family
+
+The fixed PR5756 two-tail/capacity inequalities, with a variable integer block
+exponent, are feasible exactly at lengths **112 and above**. At the minimum,
+the unique integer cutoff/floor pair is `(16,17)`. A rational witness is
+`offset=1/7`, `decay=1951/2000`. This shortens the predecessor's fixed block
+length 128 by `1/8` within the stated inequality family.
+
+Claim type: a scoped written proof using explicitly cited scalar bounds from
+Ali Romman's [PR5775](https://github.com/CrocSwap/integer-mult-bounds/pull/5775).
+Those bounds are premises, not audited or independently replayed here.
+[PROOF.md](PROOF.md) gives the complete model, case split and new exact integer
+comparisons. The new result changes the block exponent, leaving the complete
+paid/target bill and both charged tails explicit.
+
+A complete changed compiler, all other gates, physical realization and new
+carrier-size or kappa claims remain open. The selected frontier is unchanged.
+The theorem also applies when block lengths must be even or offsets rational.
+
+## Reproduce
+
+From the repository root, using standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/p104-minimum-tail-block/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-minimum-tail-block
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-minimum-tail-block --check-source-history
+```
+
+Expected direct output:
+
+```text
+PASS_MINIMUM_TAIL_BLOCK minimum=112 cutoff=16 floor=17 excluded_lengths=109 controls=10
+```
+
+`VERIFY.json` registers warning-strict normal and isolated optimized commands.
+The verifier uses exact rational arithmetic and integer powers. It enumerates
+all 109 lengths from 3 through 111 as finite corroboration of the monotonicity
+proof, checks the new witness and the unique minimal integer pair, and rejects
+ten semantic or source-corruption controls. Controls distinguish the old decay,
+old offset, larger completion floor, strict reserve/capacity equalities, and
+unsupported lower bounds or thresholds. They do not audit the source theorem.
+
+The direct command is read-only and Git-free. Optional `--receipt /absolute/path`
+writes a generated receipt outside this package, binding every package file to
+its SHA256 and recording the actual interpreter version. No receipt is required
+as an input and no handwritten receipt is supplied. `SOURCES.json` pins the
+historical catalogue and selected record. `ORIGINS.json` authenticates three
+verbatim predecessor files retained locally, so no unmerged Git object or
+network fetch is needed to reproduce the new arithmetic.
+
+## Open next questions
+
+Can length 112 be realized by a complete charged compiler for this invoice?
+First specify its changed block decomposition and rederive normalization,
+exit, rounding and nonrecursive costs. Then check the remaining gates against
+the exact source. The missing block rule and complete cost ledger prevent a
+carrier-height or admission conclusion. [TASK.json](TASK.json) records this
+question and the scope change from the independent-moment card.
+
+## Implementation limits
+
+The script has no recursion, network calls, solver, dynamic imports or local
+source-module execution. File inputs have a 128 KiB cap and an exact three-file
+allowlist. Its largest explicit loop has 109 iterations. Public arithmetic
+checks cap finite test lengths and widths at 4096; the written theorem covers
+unbounded lengths by monotonicity. Explicit exceptions remain active under
+optimized Python. All functions are below 60 lines.
+
+Power of Ten rule 3 has a managed-runtime deviation in `verify.py`: Python's
+exact integers, fractions and JSON parser allocate dynamically. The file cap,
+fixed source inventory and bounded arithmetic inputs limit live data. There
+are no persistent buffers or background processes. Normal and optimized runs
+exercise these bounds and the invalid-input paths. A fixed-allocation port
+would be needed if this offline checker were used in a real-time environment.
+Python supplies no static pointer-dereference or compile-time allocation
+checks; direct local values and explicit calls keep the equivalent paths
+visible. The registered warning-strict replays provide recurring diagnostics.
+
+## Credit
+
+New block-threshold proof and checker produced by Nick Petalas. Credit
+Ali Romman's PR5775 for the fixed-length envelope and cited scalar premises;
+Joel Pulikkan / GamingPuzzled's PR5756 for the complete invoice; and the retained
+Ali Romman PR5751, flyingviper PR5718, P104/native/controller and Jacob Alan
+Sussman, zxv and Cao Yifan compiler lineage. The retained predecessor files
+are unchanged. Elementary monotonicity and integer-power comparisons are
+classical. Independent human and formal proof-kernel review are unclaimed.
+Apache-2.0.

research/p104-minimum-tail-block/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}

research/p104-minimum-tail-block/TASK.json

@@ -0,0 +1,104 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does a changed construction's serialized target/paid invoice independently support its claimed improvement?",
+    "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",
+      "docs/research/recursive-invoice-preflight.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": "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_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": "Independently recount one changed emitted word and its complete caller, importing no constructor or pricing engine. Include target losses, owned lifetimes, native orientation and extra charges. Check existing #5633/#5708/#5717/#5719 coverage to avoid duplicate audits and preserve its exact head. Stop after the chosen missing implication; a correct root alone is not supplier admission.",
+    "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": [
+      "invoice",
+      "signed moment",
+      "productive target",
+      "independent recount"
+    ],
+    "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": "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": "changed",
+  "actual_scope": "Sharp minimum block exponent of the fixed PR5756 two-tail/capacity inequality family, using cited PR5775 scalar bounds.",
+  "scope_change_reason": "Original research rather than a repeated moment audit: change the fixed block exponent 128 to an arbitrary integer L>=3 and determine the exact feasibility threshold.",
+  "bottleneck_link": "A scoped compiler-parameter result. It identifies a shorter candidate block and a sharp obstruction below it; complete compiler costs and admission remain open.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first exact threshold and rational witness; do not optimize other gates or the invoice.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and verify.py: minimum L=112, explicit witness, 109 excluded lengths and strict-boundary controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does block length 112 extend to a complete charged compiler for this invoice?",
+      "why_it_matters": "The gate theorem alone does not lower carrier height or establish a legal compiler.",
+      "first_step": "Write the changed block decomposition and rederive its normalization, exit, rounding and nonrecursive charges before testing other gates.",
+      "blocked_by": "No source-bound changed block rule or complete cost ledger is supplied."
+    }
+  ],
+  "claim_type": "Scoped proof conditional on explicitly cited predecessor scalar bounds.",
+  "predecessor_pr": 5775,
+  "predecessor_head": "56dc0a9ec02020f5e035c7d83f078fb2b27ac76a",
+  "upstream_checked_at": "2026-10-27T12:02:44.189218+00:00",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19216140"
+}