diff --git a/research/p104-6030-outer-row-binding/README.md b/research/p104-6030-outer-row-binding/README.md new file mode 100644 index 0000000000..0fc9106dd8 --- /dev/null +++ b/research/p104-6030-outer-row-binding/README.md @@ -0,0 +1,198 @@ +# PR6030 outer rows: the remaining 30 strict and 4 functional checks bound to written sources + +**Result (no new κ).** The selected PR6030 record (κ = 781451/250000000 = +0.003125804) has 54 strict and 4 functional outer checks. PR6109 tied 24 of the +strict checks to written sources. This package ties the other 30 and all 4 +functional checks to written sources. Each row's formula is restated from a +written statement, evaluated with exact rationals on PR6030's parameter point, +and matched to the value serialized in PR6030's `RESULT.json`. All 34 agree and +are strictly positive. No discrepancy was found. + +The code imports no repository code: not `endpoint.py`, `pricing.py` or any +outer ledger. Every file that carries a row is byte-identical to a file in the +selected source manifest `certificates/frontier6030-source.json`, sometimes at a +vendored path. The verifier checks this. + +Two scope notes: + +- **One hypothesis has no row.** The stopped-recursion layer theorem in the + selected proof supplement `notes/batched-complex-rows.tex` assumes + `max{σ+β(1−σ), 1−c, 0} < λ'`. Here c is the compact-control exponent + (`K ≥ d^c/2`). No ledger row or parameter corresponds to c. With the selected + K = 128G = Θ(log p), no fixed c > 0 satisfies `K ≥ d^c/2`, so the theorem's + `1−c` term cannot be instantiated as written. The selected chain replaces it + in PR1673's `SUPPLIER-SUPPORT-AUDIT.md` §4–6. That replacement charges exposure + at `O(V h^(1−a) polylog p)` = `O(V h^τ polylog p)` with `h_(j+1) ≤ h_j/16`, so the + condition needed becomes τ < λ', which the λ rows imply. This bridge is my + reading of the sources and is **not verified here**: the verifier checks only + τ < λ', not that PR1673's separate argument replaces the theorem's full + `d^max(1−c,0)` charge under the selected call conditions. It is not a claimed + gap either. PR1673 itself records that the old `K/log p → ∞` wording fails and + gives a replacement. That file is in the source manifest but is not one of the + selected record's proof supplements. +- **One row is stronger than the theorem.** The ledger's + `leaf_saving_above_effective`, (1−β)b > a, is stronger than the layer + theorem's leaf condition, which needs only (1−β)b > q. It comes from PR1673's + note: "a strict leaf saving above a_eff and q". At β = d/b every + checked order hypothesis of the layer theorem holds, but this row rejects. + +## The stopped-recursion layer theorem + +`notes/batched-complex-rows.tex`, "Stopping and weighted-tree bounds", is a proof +supplement of the selected record, and its SHA256 equals the selected record's +pin. Its hypotheses and their rows, with β = stop, σ = 1−b, τ = 1−a, +χ = τ+(1−β)max{σ−τ,0}, leaf = σ+β(1−σ), λ' = 1−q and λ = (τ+λ')/2: + +| Written hypothesis | Ledger row(s) | Value at PR6030 | +|---|---|---| +| rational 0 < β < 1 | `stop_positive`, `stop_below_one` | d, 1−d | +| max{τ,σ,χ} < λ | `lambda_above_tau`, `lambda_above_sigma`, `lambda_above_internal` | d/2, 3d/2, d/2 | +| λ < λ' | `lambda_prime_above_lambda` | d/2 | +| λ' < 1 | `q_positive` | q | +| σ+β(1−σ) < λ' | `lambda_prime_above_leaf`, `q_below_leaf` (the same expression) | d(2−b) | +| 1−c < λ' | none (see above) | — | +| Ψ_c(σ) < 1 | not checked: stated for the theorem's own motif moment; the PR6030 counterpart is the complex uniform supplier's saving, and only `new_complex_uniform_saving_above_b` (b < uniform) is checked | d | +| 0 < τ < 1 (`compact-control-layout.tex`) | implied by `q_positive`, `q_below_effective` | — | + +Here d = (C−κ)/7 = 1/1400000000. At PR6030, σ < τ, so χ = τ, as +`notes/stopped-product-assembly.tex` and ENDPOINT.md also state. Two further +rows bind to written sentences rather than to this theorem. +`q_below_internal` (χ < λ') is in OUTER-TRANSFER-AUDIT.md §6: "internal and leaf +exponents are strictly below the selected `lambda` and `lambda_prime`". +`leaf_saving_above_effective` is in PR1673's `phase_fusion_note.tex`. + +## The other 19 strict rows and 4 functional rows + +| Group | Rows | Written source | +|---|---|---| +| Effective-saving chain | `q_below_effective`, `complex_endpoint`, `complex_above_effective`, `actual_bit_above_effective`, `complex_below_one_over_32`, `short_record_fallback` | OUTER-TRANSFER-AUDIT.md §6 ("The effective BIT saving is below both the actual ordinary BIT saving and the selected complex saving"); PR1673 SUPPLIER-SUPPORT-AUDIT.md §6 (q < a, τ = 1−a); ENDPOINT.md (`0 < q < a < b < uniform`, `b < 1/32`, `epsilon>a`) | +| Halo and locality | `microbox_halo_volume`, `halo_covers_generic_inverse_radius`, `cap_below_phase_cell_power`, `fine_prime_halo_umbrella`, `theta_positive_polynomial_power`; functional `fixed_halo_explicit_metadata_branch` | PR1786 FINE-PRIME-PADDING.md §5 and its side conditions (`128-48-beta>0, 48>43`, `xi<2`, cost power `epsilon+beta+48-128+2`, J = p^42 and bandwidth 2WJ+W, the p^10 conditioning bound from p^2 and θ^−2 ≤ 16p^4); ENDPOINT.md (theta power 2) | +| Logarithmic guards and record geometry | `actual_logarithmic_group_guard`, `actual_logarithmic_gamma_guard`, `alpha_logarithm_absorption`, `group_key_fits_record`, `support_router_span`, `new_semantic_guard_with_C1_one`; functional `new_semantic_group_guard` | FINE-PRIME-PADDING.md side conditions (`1-epsilon-r0>0`, `1-(2xi-2)-r0-beta>0`); OUTER-TRANSFER-AUDIT.md §5–6 (`group_beta<1`; ε < 1 absorbs semantic and description constants); ENDPOINT.md (group key gap 2d) | +| BIT stock | functional `new_BIT_row_stock_sublinear_in_active_group`, `actual_new_BIT_stock_sublinear` | OUTER-TRANSFER-AUDIT.md §6 (`group_beta*(1-0.003) > 0`, "the changed BIT reserve is sublinear in the active grouped width"); the current atom 1/250 and admitted BIT 17/5000 read from `research/query-thinned-controllers/RESULT.json` | +| Reporting | `improvement_over_user_baseline` | ENDPOINT.md: "a reporting check, rather than an admission hypothesis" | + +Each row has a status: + +- 11 are hypotheses of a written theorem. +- 16 are inequalities a written sentence asserts. +- 3 are fixed written constants. +- 2 are implied by a stronger written margin. `actual_logarithmic_group_guard` + and `actual_logarithmic_gamma_guard` drop the r0 that the written conditions + `1-(2xi-2)-r0-beta>0` and `1-epsilon-r0>0` carry. The verifier computes the + written margins too and checks that they are positive. +- 1 is substituted. `actual_new_BIT_stock_sublinear` is the written rule + `group_beta*(1-0.003) > 0` with PR6030's current atom 1/250 in place of 0.003. + The atom is a data input from `query-thinned-controllers/RESULT.json`, not a + written inequality. +- 1 is a reporting check. + +The verifier prints the table with values and sources. The functional +`fixed_halo_explicit_metadata_branch` is computed literally as one minus the +written paid cost power, 1 − (ε+β+48−128+2) = 79 − ε − β. + +The `fine_prime_halo_umbrella` row is 10 − (2·2+2+1/2). FINE-PRIME-PADDING.md +gives the 4 (from θ^−2 ≤ 16p^4) and the 2 (the exponential factor p^2). The +extra 1/2 has no written counterpart that I found. It only makes the row +stricter, since α^5 is polylogarithmic. + +## Other observations + +- **ENDPOINT.md's stated premises do not hold at PR6030.** Its written family + proof assumes `q < 0.002306` and the ordinary BIT saving 0.0027. PR6030 has + q = 21880643/7000000000 ≈ 0.0031258 and admitted BIT 17/5000. Its closed-form + gaps still hold as identities in d and b: (1−stop)b−a = d(1−b), + λ'−leaf = d(2−b), λ−τ = d/2 and λ−σ = 3d/2. The general case is + Nick Petalas's PR5984 region theorem, OLD < κ < min(U, B, 1/32). The verifier + checks that PR6030 lies inside it. +- **Rows with identical expressions.** Grouping by value at PR6030 and at two + points with independent parameters gives these groups: + - `q_below_leaf` = `lambda_prime_above_leaf` + - `q_below_internal` = `q_below_effective` (on the σ < τ branch) + - `group_key_fits_record` = `group_below_dimension` + - `support_router_span` = `union_header_fits_record` = functional `new_semantic_group_guard` + - `new_semantic_guard_with_C1_one` = `actual_logarithmic_gamma_guard` = `epsilon_below_one` = `source_axis_superpolynomial` + - `lambda_above_tau` = `lambda_prime_above_lambda`, since λ is the midpoint + + `lambda_above_internal` equals `lambda_above_tau` on the σ < τ branch. So the + 54 strict checks contain fewer distinct inequalities than rows. This is + informational; duplicates are harmless. + +## Controls + +Each control changes one input, and each is rejected: + +- β = 0 fails 0 < β. +- β = 1 − q/b puts the leaf exponent at λ'. +- q = a collapses λ onto τ. +- BIT saving 0.0027, PR4359's value, fails `actual_bit_above_effective`. +- β = d/b passes the layer theorem's checked order hypotheses but fails the ledger's stronger leaf ordering. +- A RESULT.json row perturbed by 10⁻³⁰ is caught. +- Halo exponent 43 fails the radius row. +- Core exponent 50 fails the core-face saving. + +The last two changes go through the same row evaluator. + +The verifier also fails if any pinned byte changes, if any of the 41 statement +fragments is missing, or if a written source is absent from the selected +manifest. + +## Reproduce + +```sh +python3 -I -B research/p104-6030-outer-row-binding/verify.py +``` + +This prints a JSON summary and `PASS_P104_6030_OUTER_ROW_BINDING` in under +0.1 s. It was run with CPython 3.10–3.14, with and without `-O`, and needs no +dependencies. + +## Scope and limits + +This checks that each outer row instantiates a written statement and that its +value at PR6030 is right. The exceptions are labelled: two rows are implied by +stronger written margins, one substitutes the current atom, and +`fine_prime_halo_umbrella` carries an extra 1/2 with no written counterpart. It does not re-prove those statements. It does not +check the layer theorem's moment hypothesis Ψ_c(σ) < 1 or its `1−c` term, +PR1673's support-local replacement, +PR1786's locality and conditioning bounds, or the outer analytic decomposition. +The five framework assumptions (native_all_columns, owned_erasure, compiler, +precision_tape, analytic_recovery) are unchanged. The formulas were transcribed +by hand from the written sources. Those sources and the ledger code share +authors, so this is source binding and independent evaluation, not an +independent derivation. This is an agent check, not human or proof-kernel +acceptance, and it changes no selected record. + +With PR6109, every one of PR6030's 54 strict and 4 functional outer predicates is +now tied to a written source by code outside the PR4359 ledger lineage. + +## Open next questions + +- **Cite the replacement for the 1−c hypothesis.** Relevance: the selected + supplement's layer theorem is not instantiated literally at K = 128G. First + step: a maintainer note in the selected review citing SUPPLIER-SUPPORT-AUDIT.md + §4–6 as the replacement of the d^max(1−c,0) term. Blocker: a maintainer + decision. No mathematical gap is claimed. +- **Audit the PR1673 replacement itself.** Relevance: this package binds rows to + statements and does not check them. First step: check SUPPLIER-SUPPORT-AUDIT.md + §6's geometric sum, and its "same strict complex/leaf margin" claim, against + the batched-complex-rows theorem. Blocker: none. +- **Controller batches against the compiler's §4 premises** (from PR6109). + Blocker: the compiler framework assumption. + +## Credit + +DreamingOfClouds (PR6030, PR5907). zxv (PR4359 outer ledger, ENDPOINT.md family +proof and OUTER-TRANSFER-AUDIT.md). Vlado Vojdanovski (PR1673 capped phase +fusion, support-local supplier and SUPPLIER-SUPPORT-AUDIT.md). Chafik Boukhalfa +(PR1786 fine-prime padding, halo/core powers). icekylinx (the stopped +product-ring construction behind the internal and leaf exponents). The upstream +and compact-control authors of the stopped-recursion layer theorem in `notes/`. +Nick Petalas (PR5984 κ-region theorem, which this package cites rather than +repeats). Douglas Colkitt with OpenAI Codex (PR6030 application review). PR6109 +(JosieElliston), whose open question this answers. + +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 review led to the r0-carrying written margins, the substituted-atom label, +the conditional wording of the `1−c` bridge, the explicit unchecked Ψ_c +hypothesis and the evaluator-based halo/core controls. Apache-2.0. diff --git a/research/p104-6030-outer-row-binding/SOURCES.json b/research/p104-6030-outer-row-binding/SOURCES.json new file mode 100644 index 0000000000..1d664f4bff --- /dev/null +++ b/research/p104-6030-outer-row-binding/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "certificates/frontier6030-source.json", + "usage": "input", + "git_blob": "e58847094e2f631665030bb6f045f8bebe638c6c", + "sha256": "95ddc380f6b05499fccd8820ab7f84fb6d287b4e66a721ed41ca9d293c4eaa3e" + }, + { + "path": "research/p104-helper470-twin-rung-removal/RESULT.json", + "usage": "input", + "git_blob": "e4a03118d585fb80c9ac932281b528ac394ccc5f", + "sha256": "84fcbe2a0b64307b5703c363408042bdd91555b0419509aa50daa43b3b1924ad" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "notes/batched-complex-rows.tex", + "usage": "input", + "git_blob": "e13bd96eb29bdc6526f10dc32e0a146bc17848a4", + "sha256": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c" + }, + { + "path": "notes/compact-control-layout.tex", + "usage": "input", + "git_blob": "16f4d233471a7d189163ae7e7902becadecbba64", + "sha256": "2bc28e50f3eb092195294cafa81213e520f6d42e7935e9905ad8a6199e2a7c87" + }, + { + "path": "notes/stopped-product-assembly.tex", + "usage": "input", + "git_blob": "3932d3ade5ddeae127c246aed515e0346a40f067", + "sha256": "1c3c7147851f30f1ff97679cfcda157b1cbe2655b8766e34f1345f20c630eaec" + }, + { + "path": "research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md", + "usage": "input", + "git_blob": "72404c42d77d4267105e8528cecff3327dfdd38c", + "sha256": "bd5b06eca043c5c871227264f6a954473c55cd16ec85bb420ff538fb8ec1d8d6" + }, + { + "path": "research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex", + "usage": "input", + "git_blob": "4351a73450dadd043aa7aca33fb6cf0dd01d6df3", + "sha256": "b5957f38c98a68f2584a42cedf91d753180dab438129fdf749b441074f00d4e1" + }, + { + "path": "research/selective-borrowing-outer-retune/vendor/pr1786/FINE-PRIME-PADDING.md", + "usage": "input", + "git_blob": "bf9899ee21be4058e4aac0b64bfa67d01ee8ddd3", + "sha256": "47d1b1b4df28aadda3cd6bdeb1fbc47290595e9208cd09c1a1f338520d33fdce" + }, + { + "path": "research/pr4359-p7-padding/source/research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "usage": "input", + "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535", + "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779" + }, + { + "path": "research/pr4359-compiler-refill/ENDPOINT.md", + "usage": "input", + "git_blob": "fe591883cfe85e869fd131579f7c2f339c47e721", + "sha256": "9b8d08cddbe8cbaeffee9d83ace37ae55b7432e534649bd8a6eabe670d5388ae" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "provenance", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/outer-ledger-kappa-region/PROOF.md", + "usage": "provenance", + "git_blob": "300f2dd0dc745a6f55fbdb26c4abf70db7e2d5fa", + "sha256": "ee523eeca3fc344fd4177ac345f605dbb04edad9732da2c23ca60365f56897e9" + }, + { + "path": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "26f2f6324bce57e69e861d2aae5a27c9de325a8e", + "sha256": "8bd158b8ef68202000f167b9b78db0b31531b5b067b5cbd91b5bf35f3ddd1ab6" + } + ] +} diff --git a/research/p104-6030-outer-row-binding/TASK.json b/research/p104-6030-outer-row-binding/TASK.json new file mode 100644 index 0000000000..276a5a345d --- /dev/null +++ b/research/p104-6030-outer-row-binding/TASK.json @@ -0,0 +1,111 @@ +{ + "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": "Theorem-to-row binding of the 30 strict and 4 functional outer checks of the selected PR6030 record that PR6109 left open: stopped-supplier lambda/leaf/internal/stop rows against the stopped-recursion layer theorem in notes/batched-complex-rows.tex (a selected proof supplement); effective-saving, halo/locality, logarithmic-guard and BIT-stock rows against written sentences of PR4359's OUTER-TRANSFER-AUDIT.md and ENDPOINT.md, PR1673's SUPPLIER-SUPPORT-AUDIT.md and phase_fusion_note.tex, and PR1786's FINE-PRIME-PADDING.md, each byte-identical to a selected-manifest file. Every row is recomputed by stdlib exact rationals from its written formula and matched to RESULT.json.", + "scope_change_reason": "The card's invoice recount for PR6030 is covered (maintainer application review; PR6043). PR6109 bound the compiler and 24 of 54 strict outer checks and left the other 30 and the 4 functional checks open as its open question 1. PR5984 already restates all 54 checks symbolically as a kappa-region theorem; it does not bind rows to the written theorems they encode, which is what this package adds.", + "bottleneck_link": "Side result for the selected record: every outer predicate behind kappa .003125804 is now tied to a written statement or labelled as a constant/reporting row. It does not change kappa.", + "budget_minutes": 60, + "stop_rule": "Stop when each of the 34 rows is bound to a written statement, a written constant or a written reporting label, and each hypothesis of the stopped-recursion theorem is mapped to a row or recorded as unmapped.", + "outcome": "completed", + "evidence": "research/p104-6030-outer-row-binding/verify.py (stdlib, under 0.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": "Should the selected proof supplement notes/batched-complex-rows.tex carry the PR1673 replacement of its 1-c0 with K >= d^c/2, so the supplement's theorem is not instantiated literally; the selected chain relies on SUPPLIER-SUPPORT-AUDIT.md sections 4-6, which is in the source manifest but not among the selected proof supplements.", + "first_step": "A maintainer note in the selected review citing SUPPLIER-SUPPORT-AUDIT.md sections 4-6 as the replacement of the compact-field term d^max(1-c,0).", + "blocked_by": "Maintainer decision; no mathematical gap is claimed." + }, + { + "question": "Is the written sufficiency of the PR1673 replacement (exposure O(V h^(1-a) polylog p), h_(j+1)<=h_j/16) independently checked?", + "why_it_matters": "This package binds the rows to statements; it does not re-prove the support-local supplier.", + "first_step": "Audit SUPPLIER-SUPPORT-AUDIT.md section 6's geometric sum and the 'same strict complex/leaf margin' claim against the batched-complex-rows theorem.", + "blocked_by": "None; it is a written-proof audit." + }, + { + "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-outer-row-binding/VERIFY.json b/research/p104-6030-outer-row-binding/VERIFY.json new file mode 100644 index 0000000000..9458d44669 --- /dev/null +++ b/research/p104-6030-outer-row-binding/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/frontier6030-source.json", + "certificates/selected-result.json", + "notes/batched-complex-rows.tex", + "notes/compact-control-layout.tex", + "notes/stopped-product-assembly.tex", + "research/p104-6030-outer-row-binding/SOURCES.json", + "research/p104-6030-outer-row-binding/verify.py", + "research/p104-helper470-twin-rung-removal/RESULT.json", + "research/pr4359-compiler-refill/ENDPOINT.md", + "research/pr4359-p7-padding/source/research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "research/query-thinned-controllers/RESULT.json", + "research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md", + "research/selective-borrowing-outer-retune/vendor/pr1673/capped-phase-fusion/phase_fusion_note.tex", + "research/selective-borrowing-outer-retune/vendor/pr1786/FINE-PRIME-PADDING.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Pinned inputs; 41 verbatim statement fragments; written-source files byte-identical to selected-manifest copies; PR6030 outer parameters equal the review family; admitted BIT 17/5000 and atom 1/250 from query-thinned-controllers; 30 strict and 4 functional outer rows recomputed from written formulas, positive and equal to RESULT.json; the order hypotheses of the stopped-recursion layer theorem (notes/batched-complex-rows.tex), with Psi_c(sigma)<1 and 1-c 0.'), + 'reserve_why': ('transfer', 'The last\nensures the changed BIT reserve is sublinear in the active grouped width'), + 'sublog': ('transfer', 'Polynomial description/preparation\ncosts are absorbed by the retained complete superpolynomial record fibers\nwhen `epsilon<1`'), + 'theta2': ('endpoint', 'halo power `48`, core power `128`, and theta power `2`.'), + 'chain': ('endpoint', '0 < q < a < b < uniform < C_test < 0.002306 < 0.0027,'), + 'geo': ('endpoint', '`0 < beta < epsilon`, `b < 1/32`, `epsilon>a`, and the unchanged integer'), + 'internal_tau': ('endpoint', 'For the stopped supplier, `sigma=1-b < tau=1-a`, so its internal exponent is\n`tau`.'), + 'leafeff': ('note1673', r'Using supplier stopping exponent $10^{-9}$ gives a strict leaf saving above $a_{\rm eff}$ and $q$.'), + 'leafgap': ('endpoint', '(1-stop)*b-a = d*(1-b),'), + 'lamdef': ('endpoint', 'With `lambda=1-(q+a)/2` and `lambda_prime=1-q`, the delicate gaps are'), + 'xidef': ('endpoint', 'xi = epsilon*(1+q) - 3/32 + layout = 29/32 + (1-d)*q.'), + 'keygap': ('endpoint', 'and the group key gap is `2*d`.'), + 'baseline': ('endpoint', "The source's historical-baseline comparison is a\nreporting check, rather than an admission hypothesis"), + 'bit27': ('endpoint', 'Keep the ordinary BIT saving `0.0027`'), + # PR1786 fine-prime padding: halo, core, locality and conditioning. + 'halo_side': ('fine', '128-48-beta>0, 48>43.'), + 'xi2': ('fine', '1/20`."), + 'halo48': ('fine', 'a halo `A=C_A p^48` covers it.'), + 'neumann': ('fine', 'With `J=ceil(p^42)`'), + 'band': ('fine', 'The bandwidth is at most `2WJ+W`.'), + 'p10': ('fine', 'a conservative common eventual bound p^10 covers'), + 'cond': ('fine', 'the exponential\nfactor is at most p^2 eventually, theta^-2<=16p^4, and alpha^5 is'), + 'gamma': ('fine', '1-epsilon-r0>0,'), + 'gauge': ('fine', '1-(2xi-2)-r0-beta=0.184140990423...>0,'), +} + + +def need(ok, what): + if not ok: + raise SystemExit('FAIL: ' + what) + + +def load(): + src = json.loads((HERE / 'SOURCES.json').read_text()) + pinned = {row['path']: row['sha256'] for row in src['files']} + text = {} + for key, rel in P.items(): + need(rel in pinned, f'{rel} is pinned in SOURCES.json') + raw = (ROOT / rel).read_bytes() + need(sha256(raw).hexdigest() == pinned[rel], f'pinned bytes of {rel}') + text[key] = raw.decode() + for name, (key, frag) in FRAG.items(): + need(frag in text[key], f'statement fragment {name!r} in {P[key]}') + return text + + +def family(kappa, tested): + """The review's parameter family (PR6030 PROOF-REVIEW.md), restated here.""" + d = (tested - kappa) / 7 + return {'kappa': kappa, 'tested_saving': tested, 'd': d, + 'complex_uniform_saving': kappa + 6 * d, 'b': kappa + 5 * d, + 'a': kappa + 4 * d, 'q': kappa + 3 * d, 'epsilon': 1 - d, + 'beta': 1 - 3 * d, 'r0': d / 10, 'stop': d, 'layout': d} + + +def derived(p, bit_saving, atom, **over): + p = dict(p) + sigma, tau = 1 - p['b'], 1 - p['a'] + stop = p['stop'] + chi = tau + (1 - stop) * max(sigma - tau, Q(0)) # written chi, beta := stop + leaf = sigma + stop * (1 - sigma) # written leaf exponent + lam_p = 1 - p['q'] # layer exponent; saving q + lam = (tau + lam_p) / 2 # PR141/assembly choice + xi = p['epsilon'] * (1 + p['q']) - Q(3, 32) + p['layout'] + return dict(p, sigma=sigma, tau=tau, chi=chi, leaf=leaf, lam=lam, lam_p=lam_p, + xi=xi, bit=bit_saving, atom=atom, **dict(dict(halo=48, core=128, radius=43), **over)) + + +# (row, group, status, fragments, written formula as a function of derived values) +# status: theorem = hypothesis of a written theorem; statement = a written +# sentence asserts the inequality; constant = a fixed written constant; +# reporting = written as a reporting check, not an admission hypothesis. +ROWS = [ + # Stopped-recursion layer theorem, notes/batched-complex-rows.tex. + ('stop_positive', 'stopped', 'theorem', ['beta'], lambda v: v['stop']), + ('stop_below_one', 'stopped', 'theorem', ['beta'], lambda v: 1 - v['stop']), + ('lambda_above_tau', 'stopped', 'theorem', ['lam', 'lamdef'], lambda v: v['lam'] - v['tau']), + ('lambda_above_sigma', 'stopped', 'theorem', ['lam', 'lamdef'], lambda v: v['lam'] - v['sigma']), + ('lambda_above_internal', 'stopped', 'theorem', ['lam', 'chi', 'lamdef'], lambda v: v['lam'] - v['chi']), + ('lambda_prime_above_lambda', 'stopped', 'theorem', ['lam', 'lamdef'], lambda v: v['lam_p'] - v['lam']), + ('q_positive', 'stopped', 'theorem', ['lam', 'lamdef'], lambda v: 1 - v['lam_p']), + ('lambda_prime_above_leaf', 'stopped', 'theorem', ['lamp', 'leafwork', 'lamdef'], lambda v: v['lam_p'] - v['leaf']), + ('q_below_leaf', 'stopped', 'theorem', ['lamp', 'leafwork', 'lamdef'], lambda v: 1 - v['leaf'] - v['q']), + ('q_below_internal', 'stopped', 'statement', ['below', 'chi'], lambda v: 1 - v['chi'] - v['q']), + ('leaf_saving_above_effective', 'stopped', 'statement', ['leafeff', 'leafgap'], lambda v: (1 - v['stop']) * v['b'] - v['a']), + # Effective-saving chain. + ('q_below_effective', 'effective', 'statement', ['tau_a', 'chain'], lambda v: v['a'] - v['q']), + ('complex_endpoint', 'effective', 'statement', ['chain'], lambda v: v['b'] - v['q']), + ('complex_above_effective', 'effective', 'statement', ['eff', 'chain'], lambda v: v['b'] - v['a']), + ('actual_bit_above_effective', 'effective', 'statement', ['eff'], lambda v: v['bit'] - v['a']), + ('new_complex_uniform_saving_above_b', 'effective', 'statement', ['psi', 'chain'], lambda v: v['complex_uniform_saving'] - v['b']), + ('complex_below_one_over_32', 'effective', 'statement', ['geo'], lambda v: Q(1, 32) - v['b']), + ('short_record_fallback', 'effective', 'statement', ['geo'], lambda v: v['epsilon'] - v['a']), + # Fine-prime halo, locality and conditioning (PR1786). + ('microbox_halo_volume', 'halo', 'theorem', ['halo_side', 'halo_cost'], lambda v: v['core'] - v['halo'] - v['beta']), + ('halo_covers_generic_inverse_radius', 'halo', 'constant', ['halo_side', 'halo48', 'neumann', 'band'], lambda v: Q(v['halo'] - v['radius'])), + ('cap_below_phase_cell_power', 'halo', 'statement', ['xi2', 'xidef'], lambda v: 2 - v['xi']), + ('fine_prime_halo_umbrella', 'halo', 'constant', ['p10', 'cond'], lambda v: 10 - (2 * 2 + 2 + Q(1, 2))), + ('theta_positive_polynomial_power', 'halo', 'constant', ['theta2'], lambda v: Q(2)), + # Logarithmic guards and record geometry. + # Written: 1-(2xi-2)-r0-beta>0 and 1-epsilon-r0>0. The serialized rows drop + # r0 (r0>0), so the written margins imply them; see WRITTEN_STRONGER. + ('actual_logarithmic_group_guard', 'guards', 'implied', ['gauge', 'xidef'], lambda v: 1 - (2 * v['xi'] - 2) - v['beta']), + ('actual_logarithmic_gamma_guard', 'guards', 'implied', ['gamma'], lambda v: 1 - v['epsilon']), + ('alpha_logarithm_absorption', 'guards', 'statement', ['gamma', 'gauge'], lambda v: v['r0']), + ('group_key_fits_record', 'guards', 'statement', ['keygap'], lambda v: 1 - (v['beta'] + 1 - v['epsilon'])), + ('support_router_span', 'guards', 'statement', ['groupbeta'], lambda v: 1 - v['beta']), + ('new_semantic_guard_with_C1_one', 'guards', 'statement', ['eps_abs', 'sublog'], lambda v: 1 - v['epsilon']), + ('improvement_over_user_baseline', 'guards', 'reporting', ['baseline'], lambda v: v['kappa'] - OLD_BASELINE), +] +FUNCTIONAL = [ + ('new_semantic_group_guard', 'statement', ['groupbeta', 'eps_abs'], lambda v: 1 - v['beta']), + ('new_BIT_row_stock_sublinear_in_active_group', 'statement', ['reserve', 'reserve_why'], lambda v: v['beta'] * (1 - Q(3, 1000))), + # Written with the PR4359 atom 0.003; PR6030 substitutes the current atom + # 1/250 (a data input, not a written inequality). + ('actual_new_BIT_stock_sublinear', 'substituted', ['reserve', 'reserve_why'], lambda v: v['beta'] * (1 - v['atom'])), + # Saving = 1 - (written paid cost power epsilon+beta+48-128+2). + ('fixed_halo_explicit_metadata_branch', 'theorem', ['halo_cost'], + lambda v: 1 - (v['epsilon'] + v['beta'] + v['halo'] - v['core'] + 2)), +] +WRITTEN_STRONGER = { + 'actual_logarithmic_group_guard': lambda v: 1 - (2 * v['xi'] - 2) - v['r0'] - v['beta'], + 'actual_logarithmic_gamma_guard': lambda v: 1 - v['epsilon'] - v['r0'], +} +# PR4359's historical baseline constant; the row is a reporting check only. +OLD_BASELINE = Q('0.001730970419199163702738') +PR6109_COVERED = 24 + + +# Hypotheses of the written layer theorem that this verifier does not check. +NOT_CHECKED = { + 'Psi_c(sigma)<1': 'stated for the theorem\'s own motif moment; for PR6030 the corresponding premise is the ' + 'complex uniform supplier saving above b (compiler obligation, PR6109 sec. 2/4); only ' + 'b < uniform < C is checked here', + "1-c0 has K>=d^c/2. Proposed reading, not ' + 'verified: PR1673 SUPPLIER-SUPPORT-AUDIT.md sec. 4-6 replaces the d^max(1-c,0) term by ' + 'support-local exposure O(V h^(1-a) polylog p); only tau 0, f'{name} strictly positive') + need(name in result_strict, f'{name} serialized in RESULT.json') + need(val == result_strict[name], f'{name} equals RESULT.json ({val} vs {result_strict[name]})') + rows[name] = {'group': group, 'status': status, 'value': str(val), + 'sources': sorted({P[FRAG[x][0]] for x in frags})} + func = {} + for name, status, frags, f in FUNCTIONAL: + val = f(v) + need(val > 0, f'{name} strictly positive') + need(val == result_functional[name], f'functional {name} equals RESULT.json') + func[name] = {'status': status, 'value': str(val), + 'sources': sorted({P[FRAG[x][0]] for x in frags})} + return rows, func + + +def main(): + text = load() + selected = json.loads(text['selected']) + need(selected['kappa'] == '781451/250000000', 'selected record is PR6030 kappa') + need(selected['proof_supplements'].get(P['rows']) == sha256(text['rows'].encode()).hexdigest(), + 'the stopped-recursion theorem file is the selected proof supplement byte for byte') + # Every source carrying a row is byte-identical to a file in the selected + # record's source manifest (possibly at a vendored path). The two notes + # outside it are cited as lineage context only. + manifest = json.loads(text['manifest'])['files'] + need(selected['source_manifest'] == P['manifest'], 'manifest is the selected source manifest') + by_hash = {} + for path, digest in manifest.items(): + by_hash.setdefault(digest, []).append(path) + in_manifest = {} + for key in ('result', 'bit', 'rows', 'support', 'note1673', 'fine', 'transfer', 'endpoint'): + hits = by_hash.get(sha256(text[key].encode()).hexdigest(), []) + need(hits, f'{P[key]} is byte-identical to a selected-manifest file') + in_manifest[P[key]] = P[key] if P[key] in hits else sorted(hits)[0] + context_only = [P[k] for k in ('layout', 'assembly')] + result = json.loads(text['result'])['complete_cost'] + outer = result['outer'] + par = {k: Q(x) for k, x in outer['parameters'].items()} + strict = {k: Q(x) for k, x in outer['strict_checks'].items()} + functional = {k: Q(x) for k, x in outer['functional_checks'].items()} + need(len(strict) == 54 and len(functional) == 4, 'RESULT.json has the 54 + 4 inventory') + kappa, tested = Q(result['kappa']), Q(result['strictification']['tested']) + need(kappa == Q(selected['kappa']), 'RESULT kappa is the selected kappa') + + fam = family(kappa, tested) + for k, x in fam.items(): + need(par[k] == x, f'parameter {k} is the review family value') + bit = json.loads(text['bit'])['ordinary_BIT'] + admitted, atom = Q(bit['admitted']), Q(bit['atom']) + need(par['bit_saving'] == admitted == Q(17, 5000), 'bit_saving is the admitted BIT saving 17/5000') + v = derived(fam, admitted, atom) + need(par['lambda_'] == v['lam'] and par['lambda_prime'] == v['lam_p'] and par['cap_xi'] == v['xi'], + 'serialized lambda, lambda_prime and xi equal the written definitions') + + rows, func = evaluate(v, strict, functional) + need(len(rows) + PR6109_COVERED == 54 and len(set(rows)) == 30, '30 rows here + 24 in PR6109 = 54') + hyp = theorem_hypotheses(v) + need(all(hyp.values()), 'every checked order hypothesis of the layer theorem holds at PR6030') + stronger = {} + for name, f in WRITTEN_STRONGER.items(): + need(f(v) > 0 and f(v) < Q(strict[name]), f'written margin of {name} (with r0) is positive and implies the row') + stronger[name] = str(f(v)) + need(v['sigma'] < v['tau'] and v['chi'] == v['tau'], 'sigma= d^c/2 for c>0), and + # the compact-field term is replaced by exposure charges O(V h^(1-a)) = + # O(V h^tau); the replacement condition tau < lambda' follows from the + # lambda rows. + need(v['tau'] < v['lam'] < v['lam_p'], "replacement condition tau < lambda' holds") + + # ENDPOINT.md's written family proof states q < 0.002306 and BIT 0.0027. + # Neither premise holds at PR6030; the identities it derives still hold. + premise = {'q_below_0.002306': v['q'] < Q('0.002306'), 'bit_is_0.0027': admitted == Q('0.0027')} + need(not any(premise.values()), 'ENDPOINT.md loose premises do not apply verbatim to PR6030') + need((1 - v['stop']) * v['b'] - v['a'] == v['d'] * (1 - v['b']) + and v['lam_p'] - v['leaf'] == v['d'] * (2 - v['b']) + and v['lam'] - v['tau'] == v['d'] / 2 and v['lam'] - v['sigma'] == 3 * v['d'] / 2, + 'ENDPOINT.md closed-form gaps hold as identities at the PR6030 point') + need(kappa < min(v['complex_uniform_saving'], admitted, Q(1, 32)) and kappa > OLD_BASELINE, + "inside PR5984's region OLD < kappa < min(U, B, 1/32)") + + # Rows that are the same expression in the free outer parameters (not + # merely equal on the one-parameter family): group by values at PR6030 and + # at two points whose parameters are chosen independently of each other. + reference = {'epsilon_below_one (PR6109)': lambda w: 1 - w['epsilon'], + 'source_axis_superpolynomial (PR6109)': lambda w: 1 - w['epsilon'], + 'group_below_dimension (PR6109)': lambda w: w['epsilon'] - w['beta'], + 'union_header_fits_record (PR6109)': lambda w: 1 - w['beta']} + for name in reference: + need(reference[name](v) == strict[name.split(' ')[0]], f'{name} reference formula') + formulas = {name: f for name, _, _, _, f in ROWS} + formulas.update({name + ' (functional)': f for name, _, _, f in FUNCTIONAL}) + formulas.update(reference) + free = [dict(kappa=Q(1, 500), tested_saving=Q(1, 300), d=Q(1, 7000), complex_uniform_saving=Q(1, 310), + b=Q(1, 320), a=Q(1, 350), q=Q(1, 410), epsilon=Q(97, 100), beta=Q(91, 100), + r0=Q(1, 900), stop=Q(1, 77), layout=Q(1, 130)), + dict(kappa=Q(1, 450), tested_saving=Q(1, 290), d=Q(1, 9000), complex_uniform_saving=Q(1, 295), + b=Q(1, 301), a=Q(1, 333), q=Q(1, 380), epsilon=Q(99, 101), beta=Q(89, 97), + r0=Q(1, 1300), stop=Q(1, 61), layout=Q(1, 170))] + points = [v] + [derived(f, Q(1, 250), Q(1, 300)) for f in free] + groups = {} + for name, f in formulas.items(): + groups.setdefault(tuple(f(w) for w in points), []).append(name) + coincident = sorted(sorted(g) for g in groups.values() if len(g) > 1) + + # Controls. Each one changes one input and must be rejected. + controls = {} + + def rejects(mod, label, test): + w = derived(dict(fam, **mod.get('fam', {})), mod.get('bit', admitted), atom) + ok = test(w) + need(not ok, f'control {label} is rejected') + controls[label] = 'rejected' + + rejects({'fam': {'stop': Q(0)}}, 'stop = 0 (beta must be positive)', lambda w: theorem_hypotheses(w)['0 0) + # The ledger's leaf ordering (1-stop)b > a is stronger than the theorem's + # sigma+beta(1-sigma) < lambda', i.e. (1-stop)b > q. At stop = d/b every + # theorem hypothesis holds, but the ledger row (and the PR1673 note's + # "leaf saving above a_eff") rejects. + edge = derived(dict(fam, stop=fam['d'] / fam['b']), admitted, atom) + need(all(theorem_hypotheses(edge).values()), 'stop = d/b satisfies the layer theorem') + need((1 - edge['stop']) * edge['b'] - edge['a'] == 0, 'stop = d/b is the leaf-ordering edge') + controls['stop = d/b (layer theorem holds; ledger leaf ordering (1-stop)b > a rejects)'] = 'rejected' + low = derived(fam, admitted, atom, halo=43) + for name in ('halo_covers_generic_inverse_radius',): + f = next(r[4] for r in ROWS if r[0] == name) + need(not f(low) > 0, 'halo exponent 43 fails the radius row') + controls['halo exponent 43 (radius row through the row evaluator)'] = 'rejected' + fat = derived(fam, admitted, atom, core=50) + f = next(r[3] for r in FUNCTIONAL if r[0] == 'fixed_halo_explicit_metadata_branch') + need(not f(fat) > 0, 'core exponent 50 fails the core-face saving') + controls['core exponent 50 (core-face saving through the row evaluator)'] = 'rejected' + bad = dict(strict) + bad['lambda_above_tau'] += Q(1, 10**30) + try: + evaluate(v, bad, functional) + except SystemExit: + controls['RESULT.json lambda_above_tau perturbed by 1e-30'] = 'rejected' + need('RESULT.json lambda_above_tau perturbed by 1e-30' in controls, 'perturbed RESULT row is caught') + + status = {} + for r in list(rows.values()) + list(func.values()): + status[r['status']] = status.get(r['status'], 0) + 1 + print(json.dumps({ + 'selected_kappa': str(kappa), 'd': str(v['d']), + 'stopped_theorem': {'source': P['rows'], 'selected_proof_supplement': True, + 'checked_order_hypotheses': {k: bool(x) for k, x in hyp.items()}, + 'not_checked': NOT_CHECKED, + 'chi_branch': 'sigma