[petalas]

Summary

Scoped proof with an exact finite numerical certificate, produced by Nick Petalas. In the declared homogeneous PR5037 local-ledger model, height 65 fails after 111 bare Pascal steps for every starting population. A pure lowest-grade start attains the optimal fraction and passes through step 110. The original equal-population start fails after its first reuse, with surplus in [-17.553090674, -17.553090235].

population <- (I + upward_shift)^e population
minimum top fraction = binom(e,H) / sum(k=0..H) binom(e,k)
best normalized surplus = A - B * minimum top fraction
H=65, C=.0034: depth 110 passes; depth 111 fails

Yiyang / Lyy-iiis's PR5037 supplies the recurrence and published local invoice and already observes qualitative top-grade domination. The new step optimizes all starting populations, proves the equality cases and strict depth monotonicity, and certifies the first impossible depth. Its operator/native counts are cited premises, not a replay deliverable. Credit Cao Yifan's round-three source, Dillon's border recovery, Jacob Alan Sussman and the retained compiler/native/helper/precision lineage. The binomial theorem and weighted-average method are classical.

Only research/pascal-lane-depth/ is added. The selected frontier is unchanged; no new kappa is claimed. Advance CLAIM.

Evidence

Before, the source identified eventual domination without an optimal finite-depth cutoff. After, the written proof gives the sharp fraction at every height and depth, and integer-only power comparisons certify the depth-110/111 signs. Both modes pass 4,654 literal-versus-binomial population/depth cases, 65 attainers, 3,360 equality-case fixtures, monotonicity through depth 256, maximum valid input limits, eight invalid inputs and four false extrapolation controls.

Local CPython 3.12.15, macOS 27.0.1 arm64, standard library only. Each registered command took about 0.6 seconds locally, below its 60-second timeout. Normal and optimized receipts agree. Registered replay, exact committed bytes for all eight package/input files, source ancestry, executable modes, official export integrity and read-only Git-free normal/optimized replay pass at 3805599b64d21332ac2036a9656fdf083755bfed.

Exact reproduction from the repository root:

/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 --check-modes

A portable Python 3.12 interpreter can replace the absolute path. Direct replay prints a generated SHA256-bound receipt and writes nothing. It needs only the package plus its two declared predecessor inputs, without Git or network access.

Limitations

The homogeneous ledger is a declared extension: each population unit gets the same T/P profile, and each top-grade unit loses 112 rank-17 targets. PR5037 does not establish that actual graded main/helper inventories realize it. The theorem rejects bare iteration in this scalar relaxation. It does not exclude changed matching, replenishment, increasing height or a nonhomogeneous invoice. Depth counts population steps, not multiplication recursion.

Actual coherent shears, complete graded source/exit/complement matching, native/physical ownership, routing, restoration, precision, stock, BIT transfer and outer admission remain unresolved or inherited. No native or selected cold replay, Lean, Docker, complete multiplier, independent human acceptance or formal-kernel proof is claimed. Universal coverage rests on the written proof; the bounded checks corroborate it.

Open next questions

• Construct and fully price one legal grade-reset or replenishment operation, preserving independent inputs and restoring helpers. Legal transport, ownership and reset costs are the first blockers.
• Export one literal matched parent/child slice with its full nonhomogeneous per-grade paid/productive profiles. A native caller and graded adapters are prerequisites; the present proof does not supply them.

Related open work

• PR6068 cites PR5037 in the denominator-13 stochastic inverse context. It studies bias/abort/stopping tariffs; this contribution assumes the published exact local invoice and proves a population obstruction without sampling.
• PR6096 studies actual /52 inverse residues and sampler applicability in that context. No residue or rounding calculation is used here, and no same-instance number is compared.
• No open PR specifically studying the bare Pascal population optimum or this depth cutoff was found in the inspected live searches. Merged PR5037 is the source; merged PR5117 treats the separate root-only sign-extraction problem.

Completion refresh checked the 14 other open account PRs created since the advance CLAIM. None studies this bare Pascal population optimum, grade-depth cutoff or equal-population ledger; no same-instance disagreement was found. PR6068 and PR6096 remain open with the distinct scopes described above.

CI notes

CI is uncertified. The package replay did not run in CI. At contribution commit 3805599b64d21332ac2036a9656fdf083755bfed, run 40726511382 cancelled plan after 10m03s, from 16:29:47 to 16:39:50 UTC. GitHub's annotation states: "The job has exceeded the maximum execution time of 10m0s". The workflow sets timeout-minutes: 10. replay (research/pascal-lane-depth) was skipped. The raw plan log places cancellation during checkout/fetch at 16:39:48, and the job API marks Onboarding helper tests skipped; no onboarding test execution is claimed for this run. The timeout is outside this six-file research package's change.

A separate unchanged-main blocker would fail planning even without the timeout. Main 721c03822c421b7f7fcbb2598993b947c4d88419, the PR6030 admission with [skip ci], changes the selected record without satisfying two documentation synchronization tests:

• test_research_current_status.CurrentStatusTests.test_current_section_matches_selected_record expects the exact **0.003125804** marker in docs/research/current-status.md; that file bolds the decimal and fraction together.
• test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record expects make frontier6030-verify in docs/ci.md; that file still describes PR5599 and its replay.

Both exact assertion failures were read in PR6150 run 40724809789. The same two failures are also reported for PR6120 run 40691776027. Open PR6050 targets the navigation repair. These docs and the workflow are unchanged here.

Local verification remains passing as recorded above. No push, CI re-run or main-document repair was made for these blockers. A maintainer re-run is needed after main is fixed and planning can complete; there is no hosted package certification or scientific acceptance from this run.

Merge Danger

Door: two-way.

Blast Radius: research.

One isolated new package. Shared code, frozen sources, predecessor credit and the selected frontier are unchanged.