diff --git a/research/direct-flow-leaf-tariff/PROOF.md b/research/direct-flow-leaf-tariff/PROOF.md new file mode 100644 index 0000000000..4bb2442024 --- /dev/null +++ b/research/direct-flow-leaf-tariff/PROOF.md @@ -0,0 +1,177 @@ +# The power-tariff transition of the fixed direct-flow leaves + +## Statement and inherited inputs + +This is a scoped proof about the historical raw-p7 leaf measure. It does not +establish a complete multiplication theorem, a full-flow invoice or a new κ. +The leaf model and inventory are Ryanson Jonathan / pinterbanget's +[PR #4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467). +DLamdata's [PR #6118](https://github.com/CrocSwap/integer-mult-bounds/pull/6118), +at `6310550e932de70243fc2aaab6f4885688b6fe21`, proves saturation of its +conditional log-deficit. We use its tilted nonlattice local-limit framework as +a cited mathematical input, without replaying its certificate or claiming its +source-law derivation as new work. The new result is the complete real-power +moment asymptotic, including its critical and divergent regimes. + +Let + +``` +P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300, + 8:1464, 16:448, 32:448, 48:448}, m = 121, +Z(s) = sum_r P[r] r^s, mu(s) = (log Z)'(s), +a = log 5, mu(alpha) = a, +lambda = t-alpha > 0, sigma^2 = (log Z)''(alpha). +``` + +The theorem holds for **every fixed real t > alpha**. Its intended application +uses the raw-p7 crossing exponent `t` of #4467/#6118. We inherit, rather than +recertify, #6118's numerical identification of that exponent. No numerical root +or onset estimate is needed for the result below. Since `P` has positive mass +at 1 and 48, `mu` is strictly increasing from 0 to log48; hence alpha exists +uniquely and sigma is positive. The support contains 1, 2 and 3, so the log-rank +law is nonlattice, as in #6118. + +For each fixed integer `G >= 0` and real `delta in [0,a]`, put +`N=m exp(Ga+delta)` and define the fixed-depth leaf measure below. At the closed +endpoint `delta=a`, **keep this G**: this is a fixed-depth extension, not a +recalculation of the floor. For actual integer ranks `N >= m`, instead select +`G=floor(log_5(N/m))` and `delta=log(N/m)-Ga in [0,a)`; that selects the original +leaf model from this family. Let `c_G(rho)` be the weighted count +of ordered G-tuples of paid ranks with product rho, retaining `m*rho <= N`. +Each tuple has weight the product of its P multiplicities. The leaf multiset +has `c_G(rho)*P[r]` leaves at rank `ell=r*rho`, using **every** terminal r, +without truncating the terminal rank again. This is the inherited #4467 leaf +model, separated from the other exit components by #6118. + +For any fixed real shift u, define its normalized power tariff + +``` +M_G(u,delta) = sum_ell L_N(ell) ell^(t+u) + / (N^u sum_ell L_N(ell) ell^t), +A(u) = m^(-u) Z(t+u)/Z(t), v = lambda+u. +``` + +**Theorem.** Uniformly over `delta in [0,a]` (and therefore along every integer +rank sequence as `G -> infinity`), the following three regimes hold: + +1. If `v > 0`, then + + `M_G(u,delta) -> A(u) lambda/v`. + +2. If `v = 0`, then + + `M_G(u,delta) ~ A(u) lambda sigma sqrt(pi/2) sqrt(G)`. + +3. If `v < 0`, put + + `R(u) = [Z(t+u)/Z(alpha)] exp(-v a)`. + + Then `R(u)>1` and + + `M_G(u,delta) ~ A(u) lambda sigma sqrt(2*pi*G) exp(-v delta) R(u)^G`. + +Here `~` means the ratio tends to one, uniformly in delta. The exponent +threshold is exactly `t+u=alpha`. The boundary offset disappears from the first +two leading terms but survives in the third. + +## 1. Exact finite identity + +Give each prefix step the probability `p_s(r)=P[r]r^s/Z(s)`. Set +`S_G=sum_i log R_i`, `B=Ga+delta`, and `Y=B-S_G`. Expectations `E_s` refer to +independent prefix steps with law p_s. The independent, untruncated terminal +step has law p_t. Weighting the leaf multiset by ell^t therefore gives exactly + +`M_G(u,delta) = A(u) E_t[exp(-uY) | S_G <= B]`. (1) + +For any real v define the finite quantity + +`J_G(v,delta)=E_alpha[exp(-vY) 1_{Y>=0}]`. + +Changing the prefix measure from t to alpha in numerator and denominator of +(1) cancels `(Z(alpha)/Z(t))^G exp(lambda B)`. Thus, for every finite G, + +`M_G(u,delta) = A(u) J_G(lambda+u,delta)/J_G(lambda,delta)`. (2) + +The denominator is positive because the all-ones prefix is admissible. In +particular `M_G(0,delta)=1` exactly. No asymptotic interchange or extra terminal +barrier occurs in (1) or (2). + +## 2. Positive tilt + +We use the following standard consequence of the nonlattice interval local +limit theorem, in the precise form used in #6118 §§3–4: + +`J_G(w,delta) ~ 1/[w sigma sqrt(2*pi*G)]`, for each fixed w>0. (3) + +For clarity, the inputs to (3) are explicit. Under p_alpha, the centered +variable `log R-a` has zero mean, positive finite variance sigma^2 and a +nonlattice law. The uniform interval local limit theorem gives convergence of +the scaled measure near any bounded delta to Lebesgue measure divided by +`sigma sqrt(2*pi)`. It also bounds the scaled probability of every unit interval +by a constant. Integrating exp(-w y) on y>=0 follows by compact step-function +approximation and the summable tail `sum_{j>=J} exp(-w j)`. Atoms at the barrier +are negligible by the same interval theorem with arbitrarily small fixed +interval width. These facts give uniformity in bounded delta and the constant +`integral_0^infinity exp(-wy)dy=1/w`. + +This use requires no strong nonlattice condition and claims no convergence +rate. The classical input is C. Stone, *A local limit theorem for nonlattice +multi-dimensional distribution functions*, Ann. Math. Statist. 36 (1965), +546–551, Corollary 1, equation (7): +[DOI](https://doi.org/10.1214/aoms/1177700165). We cite the source-relative +specialization in #6118; we do not assert an independent audit of that paper. + +Apply (3) at w=lambda and w=v>0 in (2). Their ratio tends to lambda/v, +proving regime 1. Weak convergence to the exponential law alone would not +justify its negative-u part: (3) supplies the necessary tail control. + +## 3. The critical tilt + +When v=0, `J_G(0,delta)=P_alpha(S_G<=Ga+delta)`. The ordinary central limit +theorem gives + +`J_G(0,delta) -> 1/2` (4) + +uniformly in bounded delta. Indeed the standardized endpoint is +`delta/(sigma sqrt(G)) -> 0` uniformly, and the normal distribution is +continuous at zero. Divide (4) by (3) at w=lambda in (2). The resulting +constant is `A(u) lambda sigma sqrt(2*pi)/2`, giving regime 2. + +## 4. Below the critical exponent + +For v<0 put beta=alpha+v=t+u. A second exact change of measure gives + +`J_G(v,delta) = exp(-v delta) R(u)^G P_beta(S_G<=Ga+delta)`. (5) + +The signs and offset in (5) follow directly from +`p_beta(tuple)/p_alpha(tuple)=(Z(alpha)/Z(beta))^G exp(v S_G)`. +Since beta1`, uniformly for delta in [0,a]. +For example, the complementary event is contained in `S_G/G>a`, whose +probability is at most `Var_beta(log R)/(G(a-mu(beta))^2)` by Chebyshev. +Strict convexity of log Z gives + +`log R(u)=log Z(beta)-log Z(alpha)-(beta-alpha)a > 0`. + +Divide (5) by (3) at w=lambda in (2) to obtain regime 3. + +## 5. Consequence and scope + +The normalized leaf tariff has a finite limit precisely when `t+u>alpha`; +it grows as sqrt(G) at equality and exponentially in G below it. Thus a finite +mean log-depth does not authorize substituting an arbitrary power tariff or +exchanging that tariff with the limiting exponential law. The finite limit +above the threshold is explicit, including the independent terminal-rank +factor `Z(t+u)/Z(t)`. + +This settles the leaf component only. Relative source, boundary and leaf +masses, their joint normalization, a total refined-induction ceiling, explicit +finite-depth error bounds, physical delivery and every supplier-admission +obligation remain open. The fixed historical raw-p7 law is not the selected +#6030 invoice. Neither the three regimes nor their finite checks change κ. + +New proof produced by Nick Petalas. Credit DLamdata (#6118) for the saturation +framework; Ryanson Jonathan / pinterbanget (#4467/#4465/#4459) for the leaf law +and diagnostics; zxv (#4436) for the direct flow; Cinna Davis / 1337isnot1337 +(#4405) for refined induction; Jacob Alan Sussman for the lockstep compiler; +and Stone for the classical local limit theorem. Apache-2.0. diff --git a/research/direct-flow-leaf-tariff/README.md b/research/direct-flow-leaf-tariff/README.md new file mode 100644 index 0000000000..e26d2edaaa --- /dev/null +++ b/research/direct-flow-leaf-tariff/README.md @@ -0,0 +1,109 @@ +# Exact power-tariff asymptotics for direct-flow leaves + +Scoped proof produced by Nick Petalas. No new κ. + +For the fixed historical raw-p7 leaf measure of Ryanson Jonathan's +[PR #4467](https://github.com/CrocSwap/integer-mult-bounds/pull/4467), this +package derives the full power-tariff asymptotic from the tilted local-limit +framework in DLamdata's +[PR #6118](https://github.com/CrocSwap/integer-mult-bounds/pull/6118) +(`6310550e932de70243fc2aaab6f4885688b6fe21`). This extends that saturation +result; its certificate is not rerun or audited here. + +Write `Z(s)=sum_r P[r]r^s`, `a=log5`, `mu(alpha)=a`, `lambda=t-alpha>0`, +`sigma^2=(log Z)''(alpha)`, and `N=121 exp(Ga+delta)`. Define + +``` +M_G(u,delta) = sum_leaves ell^(t+u) / (N^u sum_leaves ell^t), +A(u) = 121^(-u) Z(t+u)/Z(t), v=lambda+u. +``` + +Multiplicities are included in both sums. The new theorem is + +``` +v > 0: M_G -> A(u) lambda/v +v = 0: M_G ~ A(u) lambda sigma sqrt(pi G/2) +v < 0: M_G ~ A(u) lambda sigma sqrt(2 pi G) exp(-v delta) R(u)^G, + R(u)=Z(t+u)/Z(alpha) exp(-v a) > 1. +``` + +Each statement is for a fixed real u, uniformly over `delta in [0,log5]` in +the fixed-depth family: keep G at the upper endpoint. Actual integer ranks use +`G=floor(log_5(N/121))`, hence `delta in [0,log5)`. +See [PROOF.md](PROOF.md) for the exact finite quotient, the nonlattice +local-limit dependency, critical CLT argument and second change of measure. +In particular, convergence of the mean log-depth does not imply that all +power tariffs converge. The exact threshold is `t+u=alpha`. + +## Evidence and reproduction + +The infinite-parameter result is a written scoped proof. The standard-library +verifier checks its new finite factorization and tilted quotient using exact +rational arithmetic. It imports no predecessor verifier and computes no +predecessor root, saturation value or full-flow result. It authenticates two +main-branch input files and reads their literal P/M inventory without executing +them. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/direct-flow-leaf-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/direct-flow-leaf-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/direct-flow-leaf-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/direct-flow-leaf-tariff --check-source-history +``` + +Other hosts can use their CPython 3.12 executable. Direct replay prints +`PASS_DIRECT_FLOW_LEAF_TARIFF_FINITE_IDENTITIES`: 15 finite fixtures, +225 moment identities, 450 tilted-quotient identities, 210 second-measure-change +identities, 10,191 accepted ordered +prefixes counted across fixtures, and eight rejecting controls. The five +semantic controls omit the terminal factor, truncate the terminal rank, reverse +the power sign, drop the lockstep offset or reverse the tilt shift. Three +boundary/source controls reject excessive depth, an empty barrier domain and +corrupted source bytes. Finite exponent choices are integral so these checks +are exact; they do not certify the asymptotic theorem by enumeration. + +All loops are bounded by depth four, nine paid ranks and fixed fixture lists. +The largest ordered-word enumeration has 9^4 tuples. Python's managed allocation +is a Power-of-Ten deviation, with live collections bounded by these fixed +inputs. If a later version accepts variable depth or inventories, it must +replace these fixed bounds with enforced resource limits before reuse. +Functions are below 60 lines, no recursion, callback dispatch or dynamic code +execution is used, and normal/optimized warning-as-error runs exercise the same +explicit checks. Ruff, mypy, Pyright and Pylint are unavailable in the local PATH +and environment; stronger static-analysis coverage is unclaimed. A future +language/toolchain change should add its available diagnostics to VERIFY.json. +No generated receipt is committed or hand-written. + +## Limitations + +The local-limit theorem is a cited classical mathematical dependency, following +#6118's specialization; independent human and formal proof-kernel review are +unclaimed. The theorem uses any fixed t>alpha and inherits #6118's identification +of the raw-p7 crossing exponent for that application. It does not reverify that +identification. No finite-depth rate or practical rank threshold is supplied. +Relative source/boundary/leaf masses, a complete direct-flow invoice, native +operators, compiler realization, physical costs and selected supplier admission +are unproved here. The historical raw-p7 law is not the selected #6030 invoice; +all five selected framework assumptions remain. + +## Open next questions + +- Determine the full source/boundary/leaf-normalized exit coefficient, using + compatible tilted measures and retaining the offset. The missing non-leaf + asymptotics and relative masses block a complete refined-induction ceiling. +- Give explicit finite-depth errors for these three regimes. Start with a + quantitative interval local-limit bound for the fixed log{2,3,5} support; + recurrent finite-support phases prevent assuming strong nonlattice decay. + +The relevance, first steps and blockers are also in [TASK.json](TASK.json). + +## Credit + +New theorem and verifier produced by Nick Petalas. DLamdata (#6118) supplies the +saturation framework; Ryanson Jonathan / pinterbanget (#4467/#4465/#4459) +supplies the leaf law and diagnostics; zxv (#4436) supplies the direct flow; +Cinna Davis / 1337isnot1337 (#4405) supplies refined induction; Jacob Alan +Sussman supplies the lockstep compiler; Stone supplies the classical local +limit theorem. All predecessor files and credit remain unchanged. Apache-2.0. diff --git a/research/direct-flow-leaf-tariff/SOURCES.json b/research/direct-flow-leaf-tariff/SOURCES.json new file mode 100644 index 0000000000..408da6b263 --- /dev/null +++ b/research/direct-flow-leaf-tariff/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/direct-flow-leaf-walk/README.md", + "usage": "input", + "git_blob": "02ddde948f2e94874850eadd70d7d32559916848", + "sha256": "bf79c953cd02ad62ffd44c58ae4f5b78f2b3439574176140ba6eceb1b77430cc" + }, + { + "path": "research/direct-flow-leaf-walk/verify.py", + "usage": "input", + "git_blob": "42440e630a46c6e581797f52bfb4c0c87bbdac3a", + "sha256": "2030d79d7f136b39b4e2a3f5b033af4bba18ab87579ec352267dc1697e02157d" + } + ] +} diff --git a/research/direct-flow-leaf-tariff/TASK.json b/research/direct-flow-leaf-tariff/TASK.json new file mode 100644 index 0000000000..50b8fc00d6 --- /dev/null +++ b/research/direct-flow-leaf-tariff/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "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": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "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": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "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": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "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": "Prove the three-regime real-power tariff asymptotic for the fixed historical direct-flow leaf measure, including sharp critical and subcritical growth.", + "scope_change_reason": "The card targets productive target credit. This contribution instead resolves a scoped historical compiler-cost component left unevaluated by the leaf saturation theorem of PR6118; it does not change a supplier or the current frontier.", + "bottleneck_link": "Exact leaf power costs distinguish a bounded log-depth from a bounded recursive tariff and supply one missing component of the historical direct-flow invoice. Full source/boundary shares remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved leaf-tariff theorem; do not extend into full-flow shares or finite-depth rate research.", + "outcome": "completed", + "evidence": "PROOF.md establishes all real shifts using the cited nonlattice local-limit input; verify.py corroborates the new finite factorization and tilt quotient with exact rational arithmetic.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the complete source/boundary/leaf-normalized exit coefficient at each power exponent?", + "why_it_matters": "The leaf component alone cannot set the refined-induction ceiling.", + "first_step": "Express the source and boundary components under compatible tilted measures, retaining the lockstep offset.", + "blocked_by": "Asymptotics of the non-leaf components and their relative masses." + }, + { + "question": "Can the three leaf asymptotics receive explicit finite-depth errors?", + "why_it_matters": "A limit gives no usable rank threshold.", + "first_step": "Develop a quantitative interval local-limit bound for the fixed log{2,3,5} support.", + "blocked_by": "No strong nonlattice bound is assumed; finite-support phase recurrences must be controlled." + } + ], + "mathematical_dependencies": [ + { + "pr": 6118, + "head": "6310550e932de70243fc2aaab6f4885688b6fe21", + "author": "DLamdata", + "usage": "Cited tilted nonlattice local-limit framework and fixed leaf-measure interpretation, not executable input or an audited predecessor result.", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/6118" + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19241776", + "upstream_checkpoint": { + "commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "priority_revision": 8, + "checked_utc": "2026-10-28T12:58:17.921015+00:00", + "selected_kappa": "781451/250000000" + } +} diff --git a/research/direct-flow-leaf-tariff/VERIFY.json b/research/direct-flow-leaf-tariff/VERIFY.json new file mode 100644 index 0000000000..3e9c73f6ef --- /dev/null +++ b/research/direct-flow-leaf-tariff/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-flow-leaf-walk/README.md", + "research/direct-flow-leaf-walk/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate two exact source inputs; enumerate finite leaf moment, tilted quotient and second-measure-change identities; reject five semantic and three boundary/source mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same finite identity and rejection coverage with assertions disabled." + } + ] +} diff --git a/research/direct-flow-leaf-tariff/verify.py b/research/direct-flow-leaf-tariff/verify.py new file mode 100644 index 0000000000..4b35d4882a --- /dev/null +++ b/research/direct-flow-leaf-tariff/verify.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the new leaf moment identities; no asymptotic replay.""" + +import ast +from collections import defaultdict +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +MAX_DEPTH = 4 +P = {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, + 8: 1464, 16: 448, 32: 448, 48: 448} +M = 121 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def check_digest(data, expected): + need(sha256(data).hexdigest() == expected, "source SHA256 mismatch") + + +def authenticate(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + need(len(manifest["files"]) <= 10, "source inventory bound") + checked = 0 + for row in manifest["files"]: + if row["usage"] != "input": + continue + source = ROOT / row["path"] + need(source.stat().st_size <= 1048576, "source size bound") + data = source.read_bytes() + check_digest(data, row["sha256"]) + checked += 1 + if row["path"].endswith("verify.py"): + values = {} + for node in ast.parse(data).body: + if isinstance(node, ast.Assign) and len(node.targets) == 1: + target = node.targets[0] + if isinstance(target, ast.Name) and target.id in {"P", "M"}: + values[target.id] = ast.literal_eval(node.value) + need(values == {"P": P, "M": M}, "inventory binding") + need(checked == 2, "exactly two live source bindings") + return checked + + +def prefix_table(depth, cap): + """Bounded DP for the moment factorization, retaining each prefix barrier.""" + need(0 <= depth <= MAX_DEPTH and cap >= 1, "prefix domain") + table = {1: 1} + for _ in range(depth): + following = defaultdict(int) + for rho, count in table.items(): + for rank, multiplicity in P.items(): + if rho * rank <= cap: + following[rho * rank] += count * multiplicity + table = dict(following) + return table + + +def ordered_leaves(depth, n): + """Independent ordered-word enumeration, truncating only the final prefix.""" + need(0 <= depth <= MAX_DEPTH and n >= M, "leaf domain") + leaves = defaultdict(int) + accepted = 0 + for word in product(tuple(P), repeat=depth): + rho, count = 1, 1 + for rank in word: + rho *= rank + count *= P[rank] + if M * rho > n: + continue + accepted += 1 + for rank, multiplicity in P.items(): + leaves[rho * rank] += count * multiplicity + need(accepted > 0, "all-ones prefix exists") + return dict(leaves), accepted + + +def partition(exponent): + return sum(Fraction(count) * Fraction(rank) ** exponent + for rank, count in P.items()) + + +def moment(histogram, exponent): + return sum(Fraction(count) * Fraction(rank) ** exponent + for rank, count in histogram.items()) + + +def normalized(leaves, n, t, shift): + return moment(leaves, t + shift) / (Fraction(n) ** shift * moment(leaves, t)) + + +def tilted_j(prefix, depth, n, alpha, tilt): + # exp(-tilt*Y)=(M*rho/n)^tilt; all exponents here are integral. + return (Fraction(M, n) ** tilt * moment(prefix, alpha + tilt) + / partition(alpha) ** depth) + + +def finite_checks(): + fixtures = identities = words = tilt_identities = second_changes = 0 + for depth in range(MAX_DEPTH + 1): + start = M * 5 ** depth + for n in (start, 2 * start, 5 * start - 1): + prefix = prefix_table(depth, n // M) + leaves, accepted = ordered_leaves(depth, n) + fixtures += 1 + words += accepted + for t in (-1, 0, 1): + for shift in (-2, -1, 0, 1, 2): + observed = normalized(leaves, n, t, shift) + terminal = partition(t + shift) / partition(t) + factor = (Fraction(n) ** (-shift) * terminal + * moment(prefix, t + shift) / moment(prefix, t)) + need(observed == factor, "finite leaf factorization") + identities += 1 + for alpha in (0, 1): + lam = t - alpha + ratio = (Fraction(M) ** (-shift) * terminal + * tilted_j(prefix, depth, n, alpha, lam + shift) + / tilted_j(prefix, depth, n, alpha, lam)) + need(observed == ratio, "exact tilted quotient") + tilt_identities += 1 + for alpha in (0, 1): + for beta in range(-3, 4): + v = beta - alpha + survival = moment(leaves, beta) / partition(beta) ** (depth + 1) + changed = ((partition(beta) / partition(alpha)) ** depth + * Fraction(M, n) ** v * survival) + need(changed == tilted_j(prefix, depth, n, alpha, v), + "second exact change of measure") + second_changes += 1 + return fixtures, identities, tilt_identities, second_changes, words + + +def rejection_controls(): + depth, n, t, shift, alpha = 2, 2 * M * 25, 1, 1, 0 + prefix = prefix_table(depth, n // M) + leaves, _ = ordered_leaves(depth, n) + observed = normalized(leaves, n, t, shift) + terminal = partition(t + shift) / partition(t) + lam = t - alpha + no_terminal = observed / terminal + extra_truncation = {rank: c for rank, c in leaves.items() if M * rank <= n} + reversed_power = normalized(leaves, n, t, -shift) + dropped_offset = normalized(leaves, M * 25, t, shift) + wrong_tilt = (Fraction(M) ** (-shift) * terminal + * tilted_j(prefix, depth, n, alpha, lam - shift) + / tilted_j(prefix, depth, n, alpha, lam)) + variants = (no_terminal, normalized(extra_truncation, n, t, shift), + reversed_power, dropped_offset, wrong_tilt) + for variant in variants: + need(variant != observed, "semantic mutation must be distinguished") + rejected = len(variants) + for depth_arg, cap_arg in ((MAX_DEPTH + 1, 1), (0, 0)): + try: + prefix_table(depth_arg, cap_arg) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid domain was accepted") + try: + check_digest(b"changed", sha256(b"original").hexdigest()) + except ValueError: + rejected += 1 + else: + raise ValueError("corrupted source was accepted") + return rejected + + +def main(): + sources = authenticate() + fixtures, identities, tilts, second_changes, words = finite_checks() + controls = rejection_controls() + print(json.dumps({ + "status": "PASS_DIRECT_FLOW_LEAF_TARIFF_FINITE_IDENTITIES", + "source_bindings": sources, + "finite_fixtures": fixtures, + "ordered_prefixes_accepted_across_fixtures": words, + "moment_identities": identities, + "tilted_quotient_identities": tilts, + "second_measure_change_identities": second_changes, + "rejecting_controls": controls, + "scope": "Exact finite identities only; asymptotics are the written proof.", + }, sort_keys=True)) + + +if __name__ == "__main__": + main()