Prove bare Pascal lane iteration fails by depth 111 (no new κ)

research/pascal-lane-depth/PROOF.md

@@ -0,0 +1,166 @@
+# The optimal boundary fraction under bare Pascal iteration
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped mathematical proof with an exact finite numerical certificate.
+Independent human and formal proof-kernel review are unclaimed.
+
+## 1. Declared model and predecessor boundary
+
+Yiyang / Lyy-iiis's PR #5037, retained in
+`research/bounded-lane-border-core/core/PROOF.md`, Section 7, gives the formal
+population recurrence
+
+```text
+d'_h = d_h + d_(h-1),   0 <= h <= H,   d_(-1) = 0.
+```
+
+The term above grade H is omitted. The source already observes eventual
+top-grade domination. We take that recurrence and its published local invoice
+as premises. We do not establish a native implementation of the recurrence or
+recount the source word. The new result optimizes the boundary fraction over
+every starting population and certifies an exact failure depth.
+
+Let d be any nonzero vector in R_(>=0)^(H+1), let K=I+S where S shifts grades
+up by one and truncates above H, and put d^(e)=K^e d for an integer e>=0.
+Let D_e be the sum of its entries and z_e its grade-H entry.
+
+We declare the homogeneous local-ledger extension explicitly. Each unit of
+population receives the same complete local target and paid profiles T and P;
+each top-grade unit loses 112 rank-17 productive targets. At exponent t the
+signed surplus is therefore
+
+```text
+A(t) = sum_k T_k k^t - sum_r P_r r^t,
+B(t) = 112 * 17^t,
+M_e(d) = A(t) D_e - B(t) z_e.
+```
+
+This is a scalar accounting relaxation of a potential recursive caller.
+The source does not prove that actual graded main/helper inventories realize
+this homogeneous extension. The theorem below concerns this declared ledger,
+not arbitrary implementations of the border core. Extra costs can only worsen
+this ledger when its productive contract is held fixed. Changed profiles,
+new productive outputs or paid grade-reset mechanisms require a new analysis.
+
+## 2. Sharp population theorem
+
+Use binom(e,k)=0 for k>e. For every H,e>=0 and every permitted d,
+
+```text
+z_e / D_e >= q_H(e),
+q_H(e) = binom(e,H) / sum_(k=0)^H binom(e,k).
+```
+
+Equality is attained simultaneously at every depth by d=(1,0,...,0).
+If e>=H>=1, equality holds exactly when all initial grades above zero vanish.
+For fixed H>=1, q_H(e) is zero for e<H, strictly increases for e>=H,
+and tends to one as e tends to infinity.
+
+**Proof.** Since S^(H+1)=0, the binomial theorem gives
+
+```text
+d^(e)_h = sum_(j=0)^h binom(e,h-j) d_j.
+```
+
+Write a_l=binom(e,l) and s_l=sum_(k=0)^l a_k. The contribution of initial
+grade j to z_e is a_(H-j) d_j and its contribution to D_e is s_(H-j) d_j.
+Consequently z_e/D_e is a weighted average of the ratios a_l/s_l, with
+nonnegative weights s_(H-j)d_j.
+
+If e<H, the claimed lower bound is zero and the pure lowest grade attains it.
+Suppose e>=H. For 0<=l<=e,
+
+```text
+s_l/a_l = sum_(j=0)^l product_(a=0)^(j-1) (l-a)/(e-l+1+a).
+```
+
+For l<e, replacing l by l+1 increases every nonempty product already present and
+adds one positive term. Thus s_l/a_l strictly increases with l, so a_l/s_l
+strictly decreases. The weighted average is minimized at l=H, which
+corresponds to initial grade zero. Strictness gives the equality case.
+
+For e>=H, the same expression with l=H shows that 1/q_H(e) strictly
+decreases with e when H>=1: every nonempty product decreases. These products
+tend to zero, so q_H(e) tends to one. The transition from e=H-1 to e=H
+is from zero to a positive fraction. This proves every assertion. For H=0,
+q_0(e)=1 and the population ratio is identically one. QED.
+
+## 3. Exact local-ledger depth limit
+
+Suppose B>0. The largest possible surplus per unit final population is exactly
+
+```text
+max_(d != 0, d >= 0) M_e(d)/D_e = A - B q_H(e).
+```
+
+The pure lowest-grade vector attains it. Thus a positive local surplus is
+possible exactly when q_H(e)<A/B. In particular, if 0<A/B<1, every fixed
+height eventually fails, even after optimizing the initial populations.
+This sharpens the source's qualitative domination observation to an exact
+decision criterion at each depth.
+
+For the cited PR5037 invoice, take
+
+```text
+T = {4:56, 7:14, 8:94, 9:652, 17:224},
+P = {1:4656, 2:920, 3:1386},
+t = 4983/5000,   H = 65.
+```
+
+The integer-only certificate in `verify.py` proves
+
+```text
+0.015196119 < A/B < 0.015196120,
+q_65(110) < A/B < q_65(111).
+```
+
+Therefore the first impossible depth is **111 bare Pascal steps**. Through
+depth 110 the algebraic ledger has an attainer with strictly positive
+surplus; this is not an attained native construction. At every depth at
+least 111, every nonzero nonnegative initial population fails strictly.
+Depth here counts applications of K to the initial population, not actual
+recursive calls or the logarithmic depth of a multiplication algorithm.
+
+For the source's equal-population start d=(1,...,1) with 66 entries, the
+initial population has D_0=66 and z_0=1. Its first successor is
+(1,2,...,2), with D_1=131 and z_1=2. Exact enclosures give
+
+```text
+  5.551472 < 66 A - B     <   5.551475,
+-17.553092 < 131 A - 2 B < -17.553089.
+```
+
+Thus the equal-population one-shot bill already fails on the first bare
+reuse. Enlarging the initial populations can delay failure, but cannot
+pass depth 111 in this height-65 ledger. This says nothing against a
+changed matching, replenishment, filtration height or local invoice.
+
+## 4. Exact numerical certificate and finite checks
+
+No floating-point transcendental value is trusted. Rank one is exact. For
+each of the other seven distinct ranks in T and P, the checker bounds
+r^(4983/5000) between L/s and U/s, where s=10^12. It finds adjacent integers
+L,U by at most 48 bisections and directly verifies
+
+```text
+L^5000 <= r^4983 * s^5000 <= U^5000.
+```
+
+Monotonicity of the positive 5000th power proves the enclosure. Signed
+interval addition gives bounds on A and B. Exact rational comparisons with
+the binomial fractions certify the two depth signs and the equal-start
+failure. The printed intervals are rounded outward to denominator 10^9.
+
+The separate finite population engine applies the recurrence literally and
+compares it with the binomial formula, its optimal ratio and equality case
+for all nonzero vectors in {0,1,2}^(H+1), H=0,...,4, e=0,...,12.
+Pure-grade attainers and monotonicity through depth 256 are also checked.
+Invalid inputs and four false extrapolations have explicit rejection
+controls. These finite checks corroborate the proof; the universal
+quantifiers come from Sections 2 and 3.
+
+Every run prints a generated JSON receipt binding all six package files
+and the two cited inputs by SHA256. The receipt is stdout, so replay writes
+nothing into the checkout. The source numerical/operator verifiers are
+never imported or executed. Their mathematical premises retain Yiyang's
+and the underlying native/compiler contributors' credit.

research/pascal-lane-depth/README.md

@@ -0,0 +1,134 @@
+# Sharp depth limit for bare Pascal lane iteration
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Claim type: scoped proof with an exact finite numerical certificate.
+Independent human and formal proof-kernel review are unclaimed.
+
+At height 65, **no starting population passes the declared C=.0034 local
+ledger after 111 bare Pascal steps**. The bound is sharp: a pure lowest-grade
+start passes through step 110 in this algebraic relaxation. The original
+66-grade equal-population start already fails after its first bare reuse,
+with signed surplus in `[-17.553090674, -17.553090235]`.
+
+Yiyang / Lyy-iiis's [PR5037](https://github.com/CrocSwap/integer-mult-bounds/pull/5037)
+gives the reduced-domain border core, its one-shot local invoice and the
+recurrence `d'_h=d_h+d_(h-1)`. It already observes eventual top-grade
+domination. The new theorem optimizes every nonnegative starting population
+and gives an exact first-failure depth. The source operator and native counts
+are cited premises, not newly audited results.
+
+For every fixed height H and integer depth e, the sharp minimum top-grade
+fraction is
+
+```text
+q_H(e) = binom(e,H) / sum_(k=0)^H binom(e,k).
+```
+
+The surplus per unit final population is at most `A-B q_H(e)`, where A is
+the cited base target-minus-paid moment and B is its top-grade target debit.
+The pure lowest-grade vector attains this upper bound at every depth. For
+e>=H>=1 it is the unique attaining direction. See [PROOF.md](PROOF.md) for
+the weighted-average argument, equality cases and strict monotonicity.
+
+## Scope and relevance
+
+This is a partial answer to PR5037's whole-job matching question. It rules
+out keeping a favorable homogeneous local bill through unchanged fixed-height
+Pascal iteration by choosing better initial populations alone. The next
+construction needs changed matching, a priced reset or a changed per-grade
+invoice. It gives no new kappa or selected-frontier change.
+
+The accounting extension is an explicit hypothesis: each population unit
+has the same T/P ledger and each top-grade unit loses 112 rank-17 targets.
+PR5037 does not establish that actual graded main/helper inventories realize
+this extension. The theorem concerns that scalar relaxation. Depth counts
+applications of the population recurrence, not actual multiplication recursion.
+It excludes no different graded caller, replenishment or increasing height.
+Native shears, all-size source/exit/complement matching, ownership, routing,
+precision, stock, BIT transfer and outer admission remain open or inherited.
+No complete multiplication theorem or formal-kernel proof is claimed.
+
+## Evidence and reproduction
+
+CPython 3.12 and its standard library suffice. Local replay used CPython
+3.12.15 on macOS 27.0.1 arm64. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/pascal-lane-depth/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/pascal-lane-depth/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pascal-lane-depth
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pascal-lane-depth --check-source-history
+```
+
+A portable Python 3.12 interpreter can replace the absolute path. Both direct
+modes print `PASS_PASCAL_LANE_DEPTH` in a generated JSON receipt binding all
+six package files and both cited inputs by SHA256. Direct replay needs only
+these relative paths, without Git or network access. It writes nothing;
+redirect stdout outside the checkout to retain a receipt. There is no
+handwritten or frozen result receipt.
+
+The certificate uses integer powers to bound all eight rank powers. It proves
+strict signs at depths 110 and 111 and for the equal-start first reuse.
+Literal iteration and the binomial formula agree in 4,654 population/depth
+cases. The checks also cover 65 pure-grade attainers, 3,360 equality-case
+fixtures, optimal-fraction monotonicity through depth 256, eight invalid
+inputs and four false extrapolation controls. Finite checks corroborate the
+written universal proof. Predecessor scientific verifiers are never executed.
+
+## Sources and overlap
+
+Canonical base is `721c03822c421b7f7fcbb2598993b947c4d88419`, priority
+revision 8. [TASK.json](TASK.json) records the changed scope from
+`complex-rank-shape-decoder`; [SOURCES.json](SOURCES.json) pins the exact
+predecessor README and proof. The card's current first command,
+`research_selected_baseline.py`, passes source bindings only. The selected
+conditional frontier is unchanged.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19247035)
+records this question. The initial overlap cache included 407 open PR bodies and
+5,828 Discussion records with complete reported remote pagination. Sparse
+local overlap covered 78 of 8,348 tracked note paths; separate Git searches
+covered main's README corpus and merged/all-state PR searches covered Pascal,
+border, lane and grade terms. This is bounded overlap evidence, not proof of
+novelty or coverage of unpublished work. PR5117's root-only sign extraction
+is a different question and is not extended here.
+
+Credit Yiyang / Lyy-iiis for PR5037 and its bounded-lane core/recurrence/invoice;
+Cao Yifan for the round-three native source; Dillon for border recovery;
+Jacob Alan Sussman and the finite-precompiler contributors; and the retained
+native, Clifford, helper, precision and outer lineage. The binomial theorem
+and weighted-average method are classical. The new contribution is the sharp
+population optimization and its source-specific exact depth consequence.
+Predecessor files and their credit lines are unchanged.
+
+## Implementation bounds
+
+The checker uses direct calls, no recursion, subprocesses, external imports
+or network access. Population entry points enforce height <=65, depth <=256,
+and initial entries below 2^256. The exhaustive small domain has height <=4
+and depth <=12. Each rank-power root uses at most 48 iterations, with integers
+below 2^220000. Inputs and package files are each bounded below 1 MiB; the
+source manifest has exactly four declarations and two fixed input paths.
+All functions fit within sixty physical lines. Invariants use explicit
+exceptions and remain active with optimization. Both registered modes enable
+warning errors; no external static analyzer is claimed.
+
+Power of Ten rule 3 deviation: CPython allocates arithmetic objects and bounded
+collections dynamically. This one-shot exact checker cannot prohibit those
+runtime allocations. Enforced inputs bound live data, and only one small
+population or rank-power bisection is live at a time. Normal and optimized
+replay exercise the maximum height/depth and invalid-input limits. A future
+steady-operation native implementation would need fixed-capacity arithmetic
+storage before removing this deviation.
+
+## Open next questions
+
+1. Can a paid grade-reset or replenishment operation keep the complete bill
+   favorable? Start with one explicit reset, retained independent inputs,
+   restored helpers and its full signed invoice. Legal native transport,
+   ownership and reset costs are blockers. A reset is not free in this result.
+2. Can a literal whole-job caller use nonhomogeneous per-grade profiles to
+   escape the scalar ledger? Export one matched parent/child slice with
+   source, exit and complement identities, then compute its full per-grade
+   T/P profiles. Actual native shears and constructed graded adapters remain
+   prerequisites. The present theorem does not supply that caller.

research/pascal-lane-depth/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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/bounded-lane-border-core/README.md",
+      "usage": "input",
+      "git_blob": "30449eb1e9f70bbce76ee4db3046d79ea8e593c7",
+      "sha256": "78b85269d7f931e080e3ca263584761859656ea76d8ba509023101d3b04340d7"
+    },
+    {
+      "path": "research/bounded-lane-border-core/core/PROOF.md",
+      "usage": "input",
+      "git_blob": "87d0d64ac5e51da40b87aacb906200aea187faa3",
+      "sha256": "fcbc93f44eed41dd79aedd089f874a784fc0dac255a104a3cd39f08f2fcc5b38"
+    }
+  ]
+}