From 729842c7a3ea54d5f8a17bfb20dd528fd8d736a5 Mon Sep 17 00:00:00 2001 From: josie Date: Wed, 28 Oct 2026 04:00:53 -0400 Subject: [PATCH] research: independent source binding of PR6030's uniform compiler and outer rows (no new kappa) Stdlib verifier recomputes the higher-moment tail (sec. 2) and logarithmic majorant (sec. 4) hypotheses for the selected PR6030 invoice with directed-rounding intervals, without importing any repository engine; j=47005 is the first passing grid point. It also recomputes the nine outer savings and 24 of the 54 strict outer checks from PR1673's written cost table and FINE-PADDING-COMPOSITION.md, matching RESULT.json exactly. Co-Authored-By: Claude Opus 5.5 --- research/p104-6030-compiler-binding/README.md | 175 +++++++++ .../p104-6030-compiler-binding/SOURCES.json | 54 +++ research/p104-6030-compiler-binding/TASK.json | 105 +++++ .../p104-6030-compiler-binding/VERIFY.json | 28 ++ research/p104-6030-compiler-binding/verify.py | 369 ++++++++++++++++++ 5 files changed, 731 insertions(+) create mode 100644 research/p104-6030-compiler-binding/README.md create mode 100644 research/p104-6030-compiler-binding/SOURCES.json create mode 100644 research/p104-6030-compiler-binding/TASK.json create mode 100644 research/p104-6030-compiler-binding/VERIFY.json create mode 100644 research/p104-6030-compiler-binding/verify.py diff --git a/research/p104-6030-compiler-binding/README.md b/research/p104-6030-compiler-binding/README.md new file mode 100644 index 0000000000..64d062e567 --- /dev/null +++ b/research/p104-6030-compiler-binding/README.md @@ -0,0 +1,175 @@ +# PR6030 uniform compiler and outer rows: independent source binding + +**Result (no new κ).** Every numerical hypothesis that the selected PR6030 record +(κ = 781451/250000000 = 0.003125804) uses from the uniform compiler holds. So do +the nine outer savings and 24 of the 54 strict outer checks. This package +recomputes them with stdlib code that imports no repository engine. It does not +use PR6030's `pricing.py`, `higher-moment-strictification/verify.py`, +`mixed_target_probe.py` or the outer `ledger()` code. Each check is tied to the +written statement it instantiates. No discrepancy was found. The claimed complex +uniform rank N = 2^65807000000000 is the first passing point of the stated grid. + +This answers open question 1 of PR6043 (the corroborating PR6030 audit): "can the +outer conditions and the compiler threshold be recomputed by code that does not +descend from PR5827's `pricing.py`?" The compiler half is answered in full. For +the outer half, the limiting rows now come from written sources, and 30 strict +checks stay open (Part B). + +## Part A: compiler hypotheses + +Sources: `research/higher-moment-strictification/README.md` §2 (higher-moment +paid-tail theorem) and §4 (logarithmic majorant with any power p > 0). The +definitions of m, k_min and r_max come from its vendored +`FINITE-PRECOMPILATION.md` (m = largest target rank). The invoice is the +`targets`/`paid` histogram in `research/p104-helper470-twin-rung-removal/RESULT.json`. +The verifier checks the statement fragments it relies on by text, and all six +inputs by SHA256. + +| Theorem hypothesis | PR6030 instance | Checked here | +|---|---|---| +| §2: 0 0.19351 | interval | +| §4: m^(1−t) < 2^p | 145^(1024C) < 2^1024 | interval | +| §4: (1+H)^p < 2^((z−t)H) | z−t = (C−κ)/7 = 1/1400000000 = uniform-saving gap; (1.4·10⁹ j + 1)^1024 < 2^j | exact, j = 47005 passes, 47004 fails | +| claim row | H = 1.4·10⁹ · 47005 = 65807000000000 and N = 2^H in `CLAIM.json` | exact | + +The same pass also recounts 13,444 productive fields, 66,834 paid calls and a +rank-mass surplus of 760. Extreme ranks are 72 paid and 145 productive. The +author's 30-digit intervals for α, γ, δ and η contain the enclosures computed here. + +Real quantities are enclosed with directed-rounding interval arithmetic at 90 +digits. Addition, subtraction, multiplication and division use decimal contexts +that round toward −∞ or +∞. Python documents decimal's `ln`/`exp` as correctly +rounded, so each such result is widened outward by |r|·10⁻⁸⁹, which exceeds half +an ulp. Every real comparison (α, γ, δ, η, the initial range and the least p) +uses the appropriate endpoint. The smallest real margin is about 2.6·10⁻⁹ (α +against 1 − 10⁻¹²). + +**First passing grid point.** g(j) = j ln 2 − p ln(1 + 1.4·10⁹ j) has g(0) = 0, +g′(0) < 0 and g″ > 0. The passing grid points therefore form a single final ray, +so 47005 is the first one, as the author states. Like the source, this is a +sufficient threshold for this majorant. It is not a least native program. + +**Headroom (information only).** At θ̄ = 63/64 the least admissible logarithm +power is 1012, so p = 1024 has a margin of 12. The finite threshold does not +affect κ. + +## Part B: outer savings from written sources + +The nine outer savings and their strict checks are computed from two written +sources, not from ledger code: + +- PR1673's cost table (`research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/OUTER-AUDIT.md`, + "Cost ledger"). This gives the main transform, global router, Gaussian, grouped + BIT router, group scans and polynomial rows, and the Strassen bound ω < 45/16 + (checked by 7^16 < 2^45). +- `research/selective-borrowing-outer-retune/outer/FINE-PADDING-COMPOSITION.md` §1–2. + This gives the PR1786 halo/core powers 48/128 that replace PR1673's 3/8 in the + core-face row. It also gives ξ = ε(1+q) − c + s with c = 3/32, boundary = main + s, + union = main + s + 13/32, and the list of ε/β constraints. + +The parameters are the review's family: d = (C−κ)/7, b = κ+5d, a = κ+4d, q = κ+3d, +ε = 1−d and β = 1−3d, with layout s = d and r₀ = d/10 as recorded. All nine +savings equal the RESULT.json values exactly. All exceed κ, and main transform +(ε·q) is the minimum, with slack 20978119357/9800000000000000000. + +These 24 strict checks are recomputed and match exactly: the nine +`*_above_kappa` rows, `gaussian_above_main`, `membership_arithmetic_fits_record`, +`union_header_fits_record`, `union_tag_work_per_visit_fits_record`, +`group_below_dimension`, `global_gamma_power_slack`, `source_axis_superpolynomial`, +`cap_below_cell`, `cap_above_band`, `group_gauge_power_slack`, +`strassen_integer_power_gap`, `epsilon_positive`, `epsilon_below_one`, +`group_positive` and `positive_layout_slack`. The other 30 are not covered, and +the verifier prints them. They are the stopped-supplier and controller rows +(λ, λ′, leaf, internal, stop, q bounds), the BIT/effective rows, the halo radius +and volume rows, and the fixed constants. The 4 functional checks are also not +covered. + +The cost formulas were transcribed by hand. They share their written sources +with the ledger code, so Part B is source binding and an independent evaluation, +not an independent derivation of the cost rows. + +## Semantic controls + +Input-sensitive controls, which run on the live inputs: + +- Removing the 208 productive rank-145 jobs from the same invoice makes the + α lower bound 1.14, so the α test rejects. +- Taking the ambient rank as the 9-qubit dimension 512 rejects p = 1024 (the + least admissible p would then be 1269). The definition requires the largest + target rank 145, so this misreading is caught, not silently accepted. +- The power p = 1011 = p_min − 1 rigorously fails θ̄^p < η, and j = 47004 fails + the threshold. +- Any changed byte in the six pinned inputs, any missing statement fragment, or + any outer value that differs from RESULT.json fails. + +Fixed demonstrations, which show that the written conditions have content but do +not depend on the inputs: + +- The §2 counterexample for σ < 1 (t = 1/2, σ = 3/4, R = 100, J = 1): the actual + split charge 100 exceeds the false bound 73.25. +- Decay 127/128 fails the block test (127/128)^128 < 1/16. +- θ̄ = 45/46 fails θ < θ̄, since 16^46 ≥ 17^45. + +## Reproduce + +```sh +python3 -I -B research/p104-6030-compiler-binding/verify.py +``` + +This prints a JSON summary and `PASS_P104_6030_COMPILER_BINDING` in well under +a second, with Python 3.10–3.14 and no dependencies. + +## Scope and limits + +This checks the numerical instantiation of two written theorems, part of the +written outer ledger, and their binding to the PR6030 record. It does not +re-prove the theorems. §2 is in the higher-moment package; §4 extends PR4411, +whose majorant proof was independently reviewed in PR4425. It also does not +check the integer-flow batch identity, the exit bound e ≤ r_max(n/m)^θ or the +complementary-source capacity for the P104 controller's actual batches. Those +stay under the inherited compiler and native_all_columns assumptions, together +with owned_erasure, precision_tape and analytic_recovery. + +The invoice is read from the author's RESULT.json rather than re-derived from the +word. The independent word-to-invoice recount is in the admission review +(Matarener's interpreter) and in PR6043. This is an agent check, not human or +proof-kernel acceptance, and it changes no selected record. + +## Open next questions + +- **The remaining 30 strict outer checks from written sources.** They are still + checked by only one code lineage + (`research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py`, from + PR4359's `outer_parameters.py`). The λ/leaf/internal/stop rows decide whether + the stopped supplier's internal and leaf savings fit. First step: bind them to + the stopped support-local supplier's written statement, where + `research/selective-borrowing-outer-retune/outer/independent_check.py` has the + `(1-stop)*b > eff` precedent. Blocked on locating that statement. +- **Controller batches against the §4 premises.** For one small n ≥ m, bind the + P104 controller's batch sizes to n/m < s ≤ n and its exits to e ≤ r_max(n/m)^θ. + Blocked by the compiler framework assumption. + +## Credit + +DreamingOfClouds (PR6030, PR5907). Ali Romman (PR5827 and the P104 pricing chain). +zxv and Cao Yifan (interval and compiler bounds, as credited in PR6030's +`pricing.py`). Jacob Alan Sussman (productive recursion, finite precompilation). +zxv (the higher-moment strictification package and PR4411's logarithmic +majorant) and pinterbanget (the PR4425 independent review of that majorant). +Vlado Vojdanovski (PR1673 outer cost table), Chafik Boukhalfa (PR1758/PR1786 +fine-prime padding and halo/core powers) and the selective-borrowing outer +package authors. Matarener and the PR6043 audit (JosieElliston) for the invoice +recount this package relies on. Douglas Colkitt with OpenAI Codex (PR6030 +application review). + +Prepared for JosieElliston with Claude Opus 5.5 (Anthropic) via Claude Code, in +an unattended donated session. Codex (OpenAI) gave a read-only adversarial review +that led to the directed-rounding intervals. Apache-2.0. diff --git a/research/p104-6030-compiler-binding/SOURCES.json b/research/p104-6030-compiler-binding/SOURCES.json new file mode 100644 index 0000000000..8529e3fd97 --- /dev/null +++ b/research/p104-6030-compiler-binding/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/frontier6030/CLAIM.json", + "usage": "input", + "git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406", + "sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e" + }, + { + "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/higher-moment-strictification/README.md", + "usage": "input", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "path": "research/higher-moment-strictification/vendor/FINITE-PRECOMPILATION.md", + "usage": "input", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "path": "research/p104-helper470-twin-rung-removal/RESULT.json", + "usage": "input", + "git_blob": "e4a03118d585fb80c9ac932281b528ac394ccc5f", + "sha256": "84fcbe2a0b64307b5703c363408042bdd91555b0419509aa50daa43b3b1924ad" + }, + { + "path": "research/selective-borrowing-outer-retune/outer/FINE-PADDING-COMPOSITION.md", + "usage": "input", + "git_blob": "41efb17c1ee7dfffb471be0fecff3e4dc5472734", + "sha256": "331189874c79c2fbfb839838ec8ea61c09a7f0769098af88716ad6e7c54c0b5a" + }, + { + "path": "research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/OUTER-AUDIT.md", + "usage": "input", + "git_blob": "974b8db67f4f556bddd55904f47ec145c629f1e6", + "sha256": "94799bfa2794eb867d6ba68593c3e92988ade083e74d895e8d07ae3b8d0670dc" + } + ] +} diff --git a/research/p104-6030-compiler-binding/TASK.json b/research/p104-6030-compiler-binding/TASK.json new file mode 100644 index 0000000000..9f8feb17e7 --- /dev/null +++ b/research/p104-6030-compiler-binding/TASK.json @@ -0,0 +1,105 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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": "Independent theorem-to-caller binding of the selected PR6030 uniform compiler: the higher-moment paid-tail theorem (sec. 2) and logarithmic-majorant theorem (sec. 4) of research/higher-moment-strictification/README.md, instantiated with PR6030's serialized target/paid invoice, recomputed by stdlib code that imports no repository engine. Part B: the nine outer savings and 24 of the 54 strict outer checks recomputed from PR1673's written cost table and FINE-PADDING-COMPOSITION.md.", + "scope_change_reason": "The card's invoice recount for PR6030 is already covered (maintainer application review; PR6043 corroborating audit). PR6043's open question 1 names the compiler threshold and outer ledger as checked only through the author pricing chain. This package covers the compiler half fully and the outer ledger's nine savings plus 24 strict checks; 30 strict and 4 functional outer checks stay open.", + "bottleneck_link": "Side result for the selected record: the complex uniform template rank 2^65807000000000 is one of the claimed finite constants behind kappa .003125804. It does not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after every sec. 2/sec. 4 hypothesis used by PR6030 is recomputed or named as an inherited premise, and the outer rows that the written PR1673/PR1786 sources state are bound; leave the stopped-supplier and controller rows open.", + "outcome": "completed", + "evidence": "research/p104-6030-compiler-binding/verify.py (stdlib, under 1 s)", + "author": "JosieElliston (Claude Opus 5.5 via Claude Code)", + "ai_assistance": "Claude Opus 5.5 (Anthropic) via Claude Code, unattended donated session for JosieElliston; no human review.", + "open_questions": [ + { + "question": "Can the remaining 30 strict outer checks (stopped-supplier lambda/leaf/internal/stop rows, BIT/effective rows, halo radius/volume, fixed constants) and 4 functional checks be bound to written sources?", + "why_it_matters": "They are still checked by one code lineage (endpoint.py from PR4359 outer_parameters.py).", + "first_step": "Bind the lambda/leaf/internal rows to the stopped support-local supplier's written statement; selective-borrowing outer independent_check.py has the (1-stop)*b > eff precedent.", + "blocked_by": "Locating that written statement." + }, + { + "question": "Do the sec. 4 premises not recomputed here (integer-flow batch identity, exit bound e <= r_max (n/m)^theta, complementary-source capacity) hold for the P104 controller's actual batches?", + "why_it_matters": "They are inherited from FINITE-PRECOMPILATION.md and the PR4411/PR4425 review; this package checks only their numerical instantiation.", + "first_step": "Bind the controller's batch sizes s to n/m < s <= n for one small n >= m.", + "blocked_by": "The compiler and native_all_columns framework assumptions." + } + ] +} diff --git a/research/p104-6030-compiler-binding/VERIFY.json b/research/p104-6030-compiler-binding/VERIFY.json new file mode 100644 index 0000000000..6ec51a2dfe --- /dev/null +++ b/research/p104-6030-compiler-binding/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/frontier6030/CLAIM.json", + "research/higher-moment-strictification/README.md", + "research/higher-moment-strictification/vendor/FINITE-PRECOMPILATION.md", + "research/p104-6030-compiler-binding/SOURCES.json", + "research/p104-6030-compiler-binding/verify.py", + "research/p104-helper470-twin-rung-removal/RESULT.json", + "research/selective-borrowing-outer-retune/outer/FINE-PADDING-COMPOSITION.md", + "research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/OUTER-AUDIT.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned inputs; theorem/definition text fragments; invoice totals; sec.2 premises and tail ratios (directed-rounding intervals); exact tail assembly; sec.4 theta 0, 'positive divisor interval') + lo = min(DN.divide(x, y) for x in a for y in b) + hi = max(UP.divide(x, y) for x in a for y in b) + return (lo, hi) + + +def widen(r): + w = UP.multiply(abs(r), ULP) + return (DN.subtract(r, w), UP.add(r, w)) + + +def ln_i(a): + need(a[0] > 0, 'positive logarithm argument') + return (widen(NEAR.ln(a[0]))[0], widen(NEAR.ln(a[1]))[1]) + + +def exp_i(a): + return (widen(NEAR.exp(a[0]))[0], widen(NEAR.exp(a[1]))[1]) + + +def power(r, s): + """Enclosure of r^s for integer r >= 1 and rational s.""" + if r == 1: + return (D(1), D(1)) + return exp_i(mul(qi(s), ln_i(qi(r)))) + + +def moment(inv, s): + total = (D(0), D(0)) + for r, n in inv.items(): + total = add(total, mul(qi(n), power(r, s))) + return total + + +def theorem_text(): + text = THEOREM.read_text(encoding='utf-8') + # Statement fragments this checker instantiates; a changed statement fails. + for frag in ('u >= C, sigma = t+u >= 1,', 'J = c^v, L = b^v.', + 'alpha^v + 2 gamma_u^v + 2 delta^v,', 'alpha = P_t / T_t,', + 'gamma_u = P_(t+u) / (c^u T_t),', 'delta = B b / (c^C T_t).', + 'theta = log(r_max)/log(k_min) < 1.', + '2^(b−a) r_max^b <= m^a,', 'theta_bar^p < eta = t m^(t−1),', + 'm^(1−t) < 2^p.', '(1+H)^p < 2^((z−t)H)'): + need(frag in text, f'theorem statement fragment present: {frag!r}') + # m is the largest productive (target) rank, k_min the least, r_max the largest paid. + pre = PRECOMPILE.read_text(encoding='utf-8') + for frag in ('Put `m=max{k:W_k>0}`, `k_min=min{k:W_k>0}`, and', '`r_max=max{r_j}`. Require `r_max= epsilon q', '1 - beta - 2(1-epsilon) > 0', + 'header / tag per visit: 1 - beta > 0; group below dimension: epsilon - beta > 0', + '**1 - epsilon - r0 > 0**', '`source_axis_superpolynomial` 1 - epsilon > 0', + 'xi = 0.9079 < epsilon (cap_below_cell), xi - 1/2 > 0, guard 1 - (2 xi - 2) - r0 - beta', + 'core-face corrections epsilon + beta + 48 - 128 + 2 < 0'): + need(frag in fine, f'fine-padding statement present: {frag!r}') + outer = res['complete_cost']['outer'] + par = {k: Q(v) for k, v in outer['parameters'].items()} + # Parameter family from the admission review text: d=(C-kappa)/7, b=k+5d, a=k+4d, + # q=k+3d, eps=1-d, beta=1-3d; layout s=d and r0=d/10 as recorded. + C = Q(3125809, 10 ** 9) + d = (C - kappa) / 7 + a, b, q, eps, beta = kappa + 4 * d, kappa + 5 * d, kappa + 3 * d, 1 - d, 1 - 3 * d + s_, r0 = par['layout'], par['r0'] + need((par['d'], par['a'], par['b'], par['q'], par['epsilon'], par['beta']) == (d, a, b, q, eps, beta), + 'recorded outer parameters equal the review family') + need(s_ == d and r0 == d / 10 and par['bit_saving'] == Q(17, 5000), 'layout, r0, admitted BIT') + tau = Q(45, 16) + need(7 ** 16 < 2 ** 45, 'omega < 45/16') + c = Q(3, 32) + need(c == (3 - tau) / 2, 'c = (3 - tau)/2 = 3/32 (Strassen boundary)') + xi = eps * (1 + q) - c + s_ + need(xi == par['cap_xi'], 'xi as written') + halo, core = 48, 128 + cost = { # power-of-p costs; saving = 1 - cost + 'main_transform': 1 - eps * q, + 'global_coordinate_router': 1 - a, + 'fused_gaussian': eps - q * beta, + 'group_bit_router': eps - a * beta, + 'group_scans': eps - beta, + 'polynomial_products': 1 - eps, + 'microbox_face_corrections': eps + beta + halo - core + 2, + } + saving = {k: 1 - v for k, v in cost.items()} + main = saving['main_transform'] + saving['boundary_algebraic_matrix'] = main + s_ # written: boundary = main + s + saving['sparse_union_movement'] = main + s_ + Q(13, 32) # written: union = main + s + 13/32 + need(saving['boundary_algebraic_matrix'] == c + xi - eps, 'boundary = c + xi - eps') + shown = {k: Q(v) for k, v in outer['margins'].items()} + need(set(saving) == set(shown) and len(saving) == 9, 'nine outer rows') + for k, v in saving.items(): + need(v == shown[k], f'outer saving {k} equals RESULT') + need(v > kappa, f'outer saving {k} above kappa') + need(min(saving.values()) == main and min(saving, key=saving.get) == 'main_transform', + 'main transform is the limiting row') + sc = {k: Q(v) for k, v in outer['strict_checks'].items()} + written = { + 'main_transform_above_kappa': main - kappa, + 'gaussian_above_main': saving['fused_gaussian'] - main, + 'membership_arithmetic_fits_record': 1 - beta - 2 * (1 - eps), + 'union_header_fits_record': 1 - beta, + 'union_tag_work_per_visit_fits_record': 1 - beta, + 'group_below_dimension': eps - beta, + 'global_gamma_power_slack': 1 - eps - r0, + 'source_axis_superpolynomial': 1 - eps, + 'cap_below_cell': eps - xi, + 'cap_above_band': xi - Q(1, 2), + 'group_gauge_power_slack': 1 - (2 * xi - 2) - r0 - beta, + 'strassen_integer_power_gap': Q(2 ** 45 - 7 ** 16), + 'epsilon_positive': eps, 'epsilon_below_one': 1 - eps, + 'group_positive': beta, 'positive_layout_slack': s_, + } + written.update({k + '_above_kappa': v - kappa for k, v in saving.items()}) + for k, v in written.items(): + need(k in sc and v == sc[k] and v > 0, f'strict check {k} equals RESULT and is positive') + need(len(sc) == 54, 'author lists 54 strict checks') + return {'limiting_row': 'main_transform', 'limiting_slack': str(main - kappa), + 'strict_checks_recomputed_from_written_sources': sorted(written), + 'strict_checks_not_covered': sorted(set(sc) - set(written))} + + +def lemma_controls(): + """Semantic controls: the checks below can fail.""" + out = {} + # sec. 2 sigma>=1 restriction: README counterexample t=1/2, sigma=3/4, R=100, J=1. + with localcontext() as ctx: + ctx.prec = 40 + false_bound = D(100).sqrt() + 2 * (D(100) ** D('0.75')) + need(false_bound < 74 < 100, 'sigma<1 extension is false (split charge 100)') + out['sigma_below_one_counterexample'] = 'actual charge 100 > false bound ' + str(false_bound)[:8] + # A weaker decay block does not reach 1/16. + need(not Q(127, 128) ** 128 < Q(1, 16), 'decay 127/128 rejected') + out['decay_127_128'] = 'rejected: (127/128)^128 >= 1/16' + # theta_bar too small: 45/46 < log16/log17. + need(not 16 ** 46 < 17 ** 45, 'theta_bar=45/46 rejected') + out['theta_bar_45_46'] = 'rejected: 16^46 >= 17^45' + return out + + +def main(): + pins() + theorem_text() + res = json.loads(RESULT.read_text()) + claim = json.loads(CLAIM.read_text()) + cc = res['complete_cost'] + T = {int(k): int(v) for k, v in cc['targets'].items()} + P = {int(k): int(v) for k, v in cc['paid'].items()} + kappa = Q(claim['kappa']) + need(kappa == Q(781451, 250000000) == Q(cc['kappa']), 'selected kappa') + # Independent recount of the invoice totals quoted in the admission review. + need(sum(T.values()) == 13444 and sum(P.values()) == 66834, 'field and call totals') + need(sum(r * n for r, n in T.items()) - sum(r * n for r, n in P.items()) == 760, + 'rank-mass surplus 760') + need(max(P) == 72 and max(T) == 145 and min(T) == 1, 'extreme ranks') + + # Parameters, taken from the admission review text, not from pricing.py. + C = Q(3125809, 10 ** 9) # tested saving + t, u, v, c, b, m = 1 - C, Q(1, 7), 1024, 16, 17, 145 + theta_bar, p = Q(63, 64), 1024 + d = (C - kappa) / 7 + z_minus_t = d # uniform saving kappa+6d vs tested kappa+7d + uniform = Q(claim['uniform_templates'][0]['saving']) + need(claim['uniform_templates'][0]['family'] == 'complex', 'complex template row') + need(uniform == kappa + 6 * d and (1 - uniform) - t == z_minus_t, 'z-t = d') + need(Q(cc['strictification']['tested']) == C, 'tested saving recorded') + + # sec. 2 premises. + need(0 < C < 1 and u >= C and t + u >= 1, '0=C, sigma=t+u>=1') + need(1 < c < b < m and isinstance(v, int) and v >= 1, '1 0, 'theta_bar^p < eta = t m^(v(t-1))') + need(mul(qi(v * C), ln_m)[1] < mul(qi(p), ln_i(qi(2)))[0], 'm^(v(1-t)) < 2^p') + eta = exp_i(ln_eta) + shown = cc['compiler']['eta'] + need(D(shown['lower']) <= eta[0] and eta[1] <= D(shown['upper']), 'eta inside the author interval') + # Least p for theta_bar=63/64 (headroom, information only), rigorously bracketed. + p_min = int(ln_eta[1] / ln_theta[0]) + while not mul(qi(p_min), ln_theta)[1] < ln_eta[0]: + p_min += 1 + need(mul(qi(p_min - 1), ln_theta)[0] > ln_eta[1], 'p_min - 1 rejected: least admissible power') + # Control: m must be the largest target rank (145^v after completion). A + # misreading as the 9-qubit dimension 512 would reject p=1024. + ln_eta_512 = sub(ln_i(qi(t)), mul(qi(v * C), ln_i(qi(512)))) + p1024_ok_512 = not (ln_eta_512[1] < p_ln_theta[0]) + p_512 = int(ln_eta_512[1] / ln_theta[0]) + while not mul(qi(p_512), ln_theta)[1] < ln_eta_512[0]: + p_512 += 1 + + # Input-sensitive control: drop the 208 productive rank-145 jobs from the + # same invoice; the alpha test must then reject. + T_bad = {r: n for r, n in T.items() if r != 145} + alpha_bad = div(moment(P, t), moment(T_bad, t)) + need(not alpha_bad[1] < qi(1 - reserve)[0], 'control: invoice without rank-145 targets rejected') + # Exact tail assembly: alpha^v + 2 gamma^v + 2 delta^v < 1. + need(decay ** 128 < Q(1, 16), '(125/128)^128 < 1/16') + need(v % 128 == 0, 'v is a whole number of decay blocks') + need(1 / (1 + v * reserve) + Q(4, 2 ** 32) < 1, + '(1-x)^v <= 1/(1+vx) and 4*(1/16)^(v/128) charge') + need(c ** v < b ** v, 'max paid c^v < min target b^v') + + # sec. 4 premises with r_max=c^v, k_min=b^v, m^v. theta = log16/log17. + a_, b_ = theta_bar.numerator, theta_bar.denominator + need(c ** b_ < b ** a_, 'theta = log c/log b < theta_bar = 63/64') + need(2 ** (b_ - a_) * (c ** v) ** b_ <= (m ** v) ** a_, + 'shifted exits 2^(b-a) r_max^b <= m^a') + + # Final threshold (1+H)^p < 2^((z-t)H) on the grid H = j/(z-t). + need(z_minus_t.numerator == 1, 'z-t is a unit fraction') + step = z_minus_t.denominator + wins = lambda j: (step * j + 1) ** p < 2 ** j + j = cc['compiler']['integer_test_exponent'] + need(j == 47005 and wins(j) and not wins(j - 1), 'j=47005 passes, 47004 fails') + # Convexity: g(j)=j ln2 - p ln(1+step j) has g(0)=0, g'(0)=ln2-p*step<0, + # g''>0, so passing grid points form one final ray and j is the first. + need(p * step > 1, "g'(0) < 0 (ln2 < 1 < p*step)") + H = step * j + need(H == cc['compiler']['H'] == 65807000000000, 'H') + need(claim['uniform_templates'][0]['rank_encoding'] == f'2^{H}', 'claimed N = 2^H') + need(H > 8 * v and 2 ** 8 > m, 'N = 2^H exceeds the ambient rank m^v') + + out = { + 'marker': MARKER, + 'inputs_sha256': {str(k.relative_to(ROOT)): v for k, v in PINS.items()}, + 'invoice': {'productive_fields': B, 'paid_calls': sum(P.values()), + 'rank_mass_surplus': 760, 'max_paid': 72, 'max_target': 145}, + 'section2': {'C': str(C), 'u': '1/7', 'v': v, 'c': c, 'b': b, 'm': m, + 'alpha_upper': str(alpha[1])[:22], 'gamma_upper': str(gamma[1])[:22], + 'delta_upper': str(delta[1])[:22]}, + 'section4': {'theta_bar': '63/64', 'p': p, 'ln_eta_minus_p_ln_theta_bar_lower': str(margin_eta[0])[:20], + 'least_p_at_theta_bar_63_64': p_min, + 'control_if_m_were_512': {'p_1024_passes': p1024_ok_512, 'least_p': p_512}, + 'grid_step': step, 'j': j, 'H': H}, + 'outer_partB': outer_rows(res, kappa), + 'controls': dict(lemma_controls(), invoice_without_rank145_targets='rejected: alpha lower bound ' + + str(alpha_bad[0])[:12]), + } + need(not p1024_ok_512, 'control: m=512 rejects p=1024') + print(json.dumps(out, indent=1)) + print(MARKER) + + +if __name__ == '__main__': + main()