From 947f4e425a6190dc38a3d3ea54f5f60564942843 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 21:14:03 +0000 Subject: [PATCH] feat(research): raise partial-cache observer floor to sqrt(7/92) Compute the exact 150-dimensional scalar kernel of the PR5498 observation channel and certify that the best scalar witness under PR5537's physical norm gives squared floor 7/92, up from 1/19. --- .../README.md | 128 ++++ .../RESULT.json | 687 ++++++++++++++++++ .../SOURCES.json | 66 ++ .../TASK.json | 95 +++ .../VERIFY.json | 43 ++ .../verify.py | 291 ++++++++ 6 files changed, 1310 insertions(+) create mode 100644 research/partial-cache-scalar-witness-floor/README.md create mode 100644 research/partial-cache-scalar-witness-floor/RESULT.json create mode 100644 research/partial-cache-scalar-witness-floor/SOURCES.json create mode 100644 research/partial-cache-scalar-witness-floor/TASK.json create mode 100644 research/partial-cache-scalar-witness-floor/VERIFY.json create mode 100644 research/partial-cache-scalar-witness-floor/verify.py diff --git a/research/partial-cache-scalar-witness-floor/README.md b/research/partial-cache-scalar-witness-floor/README.md new file mode 100644 index 0000000000..ea4083c31f --- /dev/null +++ b/research/partial-cache-scalar-witness-floor/README.md @@ -0,0 +1,128 @@ +# Best scalar witness for the partial-cache observer: floor sqrt(7/92) + +**Scoped exact finite certificate. No new κ.** This sharpens the +`1/sqrt(19)` error floor of Ali Romman's +[PR #5537](https://github.com/CrocSwap/integer-mult-bounds/pull/5537) +(`research/partial-cache-minimax-floor`) to `sqrt(7/92) ≈ 0.27584`, and proves +that `7/92` is the exact optimum over every scalar witness. The previous value +`1/sqrt(19) ≈ 0.22942` used one fixed kernel vector. + +## Result + +Use the observation channel of JoyboyBrian's +[PR #5498](https://github.com/CrocSwap/integer-mult-bounds/pull/5498): every +full-nine-axis-frame value of the raw PR5402 backward word, plus the eight +endpoint partial caches. Use #5537's physical input norm and the eight-mode +physical target `T`. A *scalar witness* is a displacement `k ⊗ v`: rational +scalars `k` on the 632 original roles times one arbitrary field value `v`, +with zero on the nine owned inputs. + +1. The scalar witnesses whose free-word coefficients vanish on every observed + row form a rational space of dimension **150**. The 4,858 distinct + (row, free word) forms have rank 482 on the 632 roles. +2. Over that space, + + max ||T J(k⊗v)||^2 / ||J(k⊗v)||^2 = 7/92, + + and the optimum is isotropic: the 8x8 matrix `C^T G^-1 C` equals + `(7/92) I`. Here `G` is the physical Gram matrix of a kernel basis and `C` + is its target matrix. +3. For each of the eight modes there is an integer witness attaining `7/92` + whose target lies only in that mode. The mode-1 witness has 156 raw roles: + 56 X roles at ±13, 56 Y roles at ±1 and 44 helpers. Its physical image has + 113 nonzero roles, and `||T J||^2 / ||J||^2 = 784/10304 = 7/92`. + +PR #5537's argument is unchanged: the antipodal pair `±J(k⊗v)` has identical +observations at every positive width. So every decoder, including nonlinear +ones using the complete supplied history, has uniform error at least +`sqrt(7/92)` on the physical unit ball. A randomized decoder has worst-case +expected squared error at least `7/92`. The old witness of #5498 is in the same +kernel and gives exactly #5537's `1/19`. The verifier checks this as a control. + +### Why 7/92 is optimal among scalar witnesses + +Write a witness as `k = B c` for the kernel basis `B`. The target is `C^T c` and +the physical squared norm is `c^T G c`, with `G` positive definite. Every +Gauss-Jordan pivot of `G` is checked positive. For any unit `u` in R^8, +Cauchy-Schwarz in the `G` inner product gives + + (u^T C^T c)^2 <= (u^T C^T G^-1 C u)(c^T G c) = (7/92)(c^T G c). + +Taking the supremum over `u` gives `||C^T c||^2 <= (7/92) c^T G c`. The +verifier checks `G X = C` and `C^T X = (7/92) I` exactly, and checks that the +explicit witnesses `B X e_a` attain the bound. + +## Scope and limits + +- **Claim type:** an exact finite certificate (rational linear algebra on the + pinned word) plus the short Cauchy-Schwarz argument above. The all-width + transfer is #5498's coefficientwise free-word argument. It applies unchanged + because every scalar witness in the kernel is coefficientwise zero. +- **Not the full norm.** This is the optimum over the scalar class `k ⊗ v` only. + It is a lower bound on `||T restricted to ker O||`, #5537's Open next + question 2. Operator-valued kernel elements, such as width-dependent or + role-dependent maps of `v`, are not covered. The exact norm may be larger. +- **Inherited premises.** These are cited, not re-proved: the free-word + grammar of #5498 and its replay of the PR5402 word; the PR5402 target + formula `b_k = (1/2) K_m,k^-1 R sum_j M_kj y_j`; the unitary wrappers, + frames, `2Km` mode entrances and helper basis `L` of PR5402, as used by #5537 + for its physical norm; and the all-width physical realization of these maps. +- **Free-word grammar.** Constraints are taken coefficientwise in reduced free + words, as in #5498. Extra operator relations among actual monomial matrices + could enlarge the true kernel. That would only raise the floor further. +- No supplier admission, paid-call bound, κ change or complete multiplication + theorem follows. + +## Controls + +The verifier must reject or detect each of the following: + +- One perturbed coordinate of the optimal witness must leave the kernel. +- Dropping the eight endpoint caches enlarges the kernel to dimension 158. The + diagonal optimum then reaches `105/8`, so the caches carry real information. +- The raw (non-physical) norm gives `7/204` for the same witness. The helper + basis and mode entrance normalization therefore matter. +- Every input byte is checked against `SOURCES.json` before the PR5498 replay + module is imported. The emitted receipt must equal `RESULT.json`, which was + generated by `verify.py --emit`. + +## Reproduce + +From the repository root, with CPython 3.12 (about 25 s per run): + +```sh +python3.12 -I -W error -B research/partial-cache-scalar-witness-floor/verify.py +python3.12 -I -W error -B -O research/partial-cache-scalar-witness-floor/verify.py +python3.12 -B scripts/research_package.py --package research/partial-cache-scalar-witness-floor +``` + +A sparse checkout must include `research/partial-cache-history-observer`, +`research/native-rank8-helper-provider`, `research/coded-native-caller`, +`research/kappa-round3-warp-20261022` and `research/partial-cache-minimax-floor`. + +## Open next questions + +1. **What is the full norm of T on ker O?** This scalar optimum is a lower + bound only. First step: allow role-dependent unitary or monomial + coefficients on `v` at width one, and test whether the kernel strictly + grows past the 150-dimensional scalar space. The blocker is an all-width + argument for non-scalar kernel elements. +2. **Why is the optimum isotropic?** `C^T G^-1 C = (7/92) I` for all eight + modes. A symmetry of the PR5402 mode boundaries may explain it and give a + closed-form witness. First step: compare the eight integer witnesses under + the provider's mode permutation. +3. **Can one retained observation lower the floor?** #5537 asks whether one + extra observation separates `J(V)`. With the 150-dimensional kernel in hand, + the useful test is how much one versioned partial-history row lowers the + `7/92` optimum. Physical availability and retention of that row remain + unpriced. + +## Credit + +Produced by Nick Petalas. JoyboyBrian (@JoyboyBrian) supplied the PR5498 +observation channel, free-word replay and the first kernel witness. Ali Romman +(@aliromman) supplied the PR5537 physical norm, minimax argument and the open +question this answers in part. Dillon Amburgey (@dillona) supplied the PR5402 +provider, helper basis and target formula. The retained Mark/Matarener, THU New +Media Research Center, zxv and native-compiler lineage is credited in those +sources. Apache-2.0. diff --git a/research/partial-cache-scalar-witness-floor/RESULT.json b/research/partial-cache-scalar-witness-floor/RESULT.json new file mode 100644 index 0000000000..20e691e9b5 --- /dev/null +++ b/research/partial-cache-scalar-witness-floor/RESULT.json @@ -0,0 +1,687 @@ +{ + "constraint_rank": 482, + "controls": { + "cache_free_mode_diagonal_max": "105/8", + "kernel_dim_without_caches": 158, + "perturbed_witness_rejected": true, + "raw_norm_ratio_of_mode1_witness": "7/204" + }, + "distinct_full_frame_histories": 4891, + "distinct_word_constraints": 4858, + "endpoint_caches": 8, + "gram_positive_pivots": 150, + "mode1_witness": { + "mode": 1, + "nonzero_physical_roles": 113, + "nonzero_raw_roles": 156, + "physical_norm_squared": "10304", + "raw": [ + [ + 0, + "-13" + ], + [ + 1, + "-13" + ], + [ + 6, + "-13" + ], + [ + 7, + "13" + ], + [ + 12, + "-13" + ], + [ + 13, + "-13" + ], + [ + 14, + "-13" + ], + [ + 15, + "-13" + ], + [ + 16, + "-13" + ], + [ + 17, + "13" + ], + [ + 18, + "13" + ], + [ + 19, + "13" + ], + [ + 27, + "13" + ], + [ + 28, + "13" + ], + [ + 29, + "13" + ], + [ + 30, + "13" + ], + [ + 31, + "-13" + ], + [ + 38, + "13" + ], + [ + 39, + "13" + ], + [ + 40, + "13" + ], + [ + 41, + "-13" + ], + [ + 42, + "-13" + ], + [ + 43, + "-13" + ], + [ + 44, + "-13" + ], + [ + 51, + "-13" + ], + [ + 52, + "-13" + ], + [ + 53, + "-13" + ], + [ + 54, + "-13" + ], + [ + 55, + "-13" + ], + [ + 56, + "-13" + ], + [ + 57, + "-13" + ], + [ + 58, + "13" + ], + [ + 59, + "13" + ], + [ + 60, + "13" + ], + [ + 73, + "-13" + ], + [ + 74, + "-13" + ], + [ + 75, + "-13" + ], + [ + 76, + "-13" + ], + [ + 77, + "13" + ], + [ + 78, + "-13" + ], + [ + 81, + "13" + ], + [ + 82, + "-13" + ], + [ + 83, + "-13" + ], + [ + 84, + "-13" + ], + [ + 86, + "13" + ], + [ + 87, + "13" + ], + [ + 92, + "-13" + ], + [ + 93, + "13" + ], + [ + 99, + "-13" + ], + [ + 100, + "-13" + ], + [ + 101, + "-13" + ], + [ + 102, + "-13" + ], + [ + 103, + "13" + ], + [ + 104, + "-13" + ], + [ + 105, + "-13" + ], + [ + 106, + "-13" + ], + [ + 112, + "1" + ], + [ + 113, + "1" + ], + [ + 118, + "1" + ], + [ + 119, + "-1" + ], + [ + 124, + "1" + ], + [ + 125, + "1" + ], + [ + 126, + "1" + ], + [ + 127, + "1" + ], + [ + 128, + "1" + ], + [ + 129, + "-1" + ], + [ + 130, + "-1" + ], + [ + 131, + "-1" + ], + [ + 139, + "-1" + ], + [ + 140, + "-1" + ], + [ + 141, + "-1" + ], + [ + 142, + "-1" + ], + [ + 143, + "1" + ], + [ + 150, + "-1" + ], + [ + 151, + "-1" + ], + [ + 152, + "-1" + ], + [ + 153, + "1" + ], + [ + 154, + "1" + ], + [ + 155, + "1" + ], + [ + 156, + "1" + ], + [ + 163, + "1" + ], + [ + 164, + "1" + ], + [ + 165, + "1" + ], + [ + 166, + "1" + ], + [ + 167, + "1" + ], + [ + 168, + "1" + ], + [ + 169, + "1" + ], + [ + 170, + "-1" + ], + [ + 171, + "-1" + ], + [ + 172, + "-1" + ], + [ + 185, + "1" + ], + [ + 186, + "1" + ], + [ + 187, + "1" + ], + [ + 188, + "1" + ], + [ + 189, + "-1" + ], + [ + 190, + "1" + ], + [ + 193, + "-1" + ], + [ + 194, + "1" + ], + [ + 195, + "1" + ], + [ + 196, + "1" + ], + [ + 198, + "-1" + ], + [ + 199, + "-1" + ], + [ + 204, + "1" + ], + [ + 205, + "-1" + ], + [ + 211, + "1" + ], + [ + 212, + "1" + ], + [ + 213, + "1" + ], + [ + 214, + "1" + ], + [ + 215, + "-1" + ], + [ + 216, + "1" + ], + [ + 217, + "1" + ], + [ + 218, + "1" + ], + [ + 224, + "-28" + ], + [ + 227, + "-14" + ], + [ + 229, + "14" + ], + [ + 233, + "-14" + ], + [ + 234, + "-14" + ], + [ + 237, + "14" + ], + [ + 238, + "14" + ], + [ + 272, + "-14" + ], + [ + 276, + "-14" + ], + [ + 280, + "14" + ], + [ + 283, + "28" + ], + [ + 286, + "-14" + ], + [ + 287, + "28" + ], + [ + 336, + "-14" + ], + [ + 340, + "-14" + ], + [ + 347, + "28" + ], + [ + 350, + "-14" + ], + [ + 351, + "14" + ], + [ + 352, + "-14" + ], + [ + 356, + "-14" + ], + [ + 366, + "-14" + ], + [ + 367, + "14" + ], + [ + 400, + "-14" + ], + [ + 401, + "-14" + ], + [ + 402, + "14" + ], + [ + 403, + "-28" + ], + [ + 405, + "-14" + ], + [ + 406, + "-14" + ], + [ + 409, + "-14" + ], + [ + 410, + "14" + ], + [ + 411, + "-28" + ], + [ + 413, + "-14" + ], + [ + 414, + "-14" + ], + [ + 416, + "-14" + ], + [ + 417, + "-14" + ], + [ + 418, + "14" + ], + [ + 419, + "-28" + ], + [ + 421, + "-14" + ], + [ + 422, + "-14" + ], + [ + 425, + "-14" + ], + [ + 426, + "14" + ], + [ + 427, + "-28" + ], + [ + 429, + "-14" + ], + [ + 430, + "-14" + ] + ], + "target_norm_squared": "784" + }, + "optimal_floor_decimal_lower": "0.27583", + "optimal_squared_floor": "7/92", + "optimum_matrix": "(7/92) I_8", + "per_mode_witness_supports": [ + [ + 158, + 113 + ], + [ + 156, + 113 + ], + [ + 157, + 113 + ], + [ + 157, + 113 + ], + [ + 159, + 113 + ], + [ + 158, + 113 + ], + [ + 158, + 113 + ], + [ + 160, + 113 + ] + ], + "previous_squared_floor": "1/19", + "scalar_kernel_dimension": 150, + "scope": "exact optimum over scalar witnesses k(x)v in the PR5498 free-word observation grammar under PR5537 physical norms; lower bound on ||T restricted to ker O||, not that norm; no kappa change", + "status": "PASS_PARTIAL_CACHE_SCALAR_WITNESS_FLOOR" +} diff --git a/research/partial-cache-scalar-witness-floor/SOURCES.json b/research/partial-cache-scalar-witness-floor/SOURCES.json new file mode 100644 index 0000000000..730321b268 --- /dev/null +++ b/research/partial-cache-scalar-witness-floor/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + { + "path": "research/native-rank8-helper-provider/PROVIDER.json", + "usage": "input", + "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455", + "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65" + }, + { + "path": "research/native-rank8-helper-provider/WORD.json.gz", + "usage": "input", + "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc" + }, + { + "path": "research/partial-cache-history-observer/KERNEL.json", + "usage": "input", + "git_blob": "92ca0f83330a8e6ef265ca05df2b5f6b472af9a0", + "sha256": "def77e3bcd50a4c992d9fecc660bbbc9dcdad37da22151351e346f62c9c4593f" + }, + { + "path": "research/partial-cache-history-observer/SOURCES.json", + "usage": "input", + "git_blob": "2c13b8463d4b22c4314f7773bf85782f65b55937", + "sha256": "d6d69fa82e4cc2d9cbecd18db01e05fce82b502a8b463aca63a4050d9ccc9097" + }, + { + "path": "research/partial-cache-history-observer/verify.py", + "usage": "input", + "git_blob": "a615ddfc9c7dae7534348915ae9d63af79385737", + "sha256": "ddc1f5b84a1b2154c757e0cce0adf89c67938cdfddfb14c984b7d569721c28ce" + }, + { + "path": "research/partial-cache-minimax-floor/README.md", + "usage": "input", + "git_blob": "ad504234f8f7c586147d799775c9997764ab956f", + "sha256": "ed980fc43f4b8530fbd3918fd8ff351c955b4a8bf8165b9dc12db59f06f821fc" + } + ] +} diff --git a/research/partial-cache-scalar-witness-floor/TASK.json b/research/partial-cache-scalar-witness-floor/TASK.json new file mode 100644 index 0000000000..265c3b6841 --- /dev/null +++ b/research/partial-cache-scalar-witness-floor/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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": "What is the best scalar-witness error floor for the PR5498 partial-cache observation channel under PR5537's physical norm? Exact optimum over all scalar kernel witnesses k(x)v.", + "scope_change_reason": "The card asks for one quantified implication at an actual caller. This takes Open next question 2 of PR5537 (full norm of T on ker O) and settles its scalar-witness part, a quantified statement about the actual PR5402 observer contract; no selected assumption is discharged.", + "bottleneck_link": "Side result on an observer contract: it quantifies how far the partial-cache observation channel is from identifying the consumer target, which bounds any repair that keeps this channel. It does not change \u03ba.", + "budget_minutes": 60, + "stop_rule": "Stop at the exact scalar-witness optimum; do not attempt the operator-valued kernel in this session.", + "outcome": "completed", + "evidence": "verify.py replays the pinned PR5498 observation rows, computes the exact 150-dimensional scalar kernel, certifies C^T G^-1 C = (7/92) I with a positive-pivot Gram solve, constructs eight attaining integer witnesses, and checks the PR5498 witness gives 1/19. RESULT.json is the --emit receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the full norm of T restricted to ker O, beyond scalar witnesses?", + "why_it_matters": "It gives the sharp linear-information error on the full physical ball; 7/92 is only a lower bound.", + "first_step": "At width one, allow role-dependent unitary/monomial coefficients on v and test whether the kernel grows past dimension 150.", + "blocked_by": "An all-width argument for non-scalar kernel elements." + }, + { + "question": "Why is the scalar optimum isotropic, C^T G^-1 C = (7/92) I?", + "why_it_matters": "A symmetry explanation could give a closed-form witness and transfer to related observers.", + "first_step": "Compare the eight integer witnesses under the provider's mode permutation and signs.", + "blocked_by": "None identified." + }, + { + "question": "How much does one extra retained observation lower the 7/92 optimum?", + "why_it_matters": "PR5537 asks whether one more observation separates J(V); the scalar kernel now measures it.", + "first_step": "Append one versioned partial-history row to the constraints and recompute the optimum.", + "blocked_by": "Physical availability and retention cost of that row are unpriced." + } + ] +} diff --git a/research/partial-cache-scalar-witness-floor/VERIFY.json b/research/partial-cache-scalar-witness-floor/VERIFY.json new file mode 100644 index 0000000000..9baa5a9e73 --- /dev/null +++ b/research/partial-cache-scalar-witness-floor/VERIFY.json @@ -0,0 +1,43 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coded-native-caller/NORMALIZERS.json", + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/native-rank8-helper-provider/PROVIDER.json", + "research/native-rank8-helper-provider/WORD.json.gz", + "research/partial-cache-history-observer/KERNEL.json", + "research/partial-cache-history-observer/SOURCES.json", + "research/partial-cache-history-observer/verify.py", + "research/partial-cache-minimax-floor/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Pinned PR5498 replay, exact scalar kernel, (7/92) I optimum certificate, attaining witnesses, PR5537 1/19 control and mutation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Same checks under -O; all assertions are explicit exceptions." + } + ] +} diff --git a/research/partial-cache-scalar-witness-floor/verify.py b/research/partial-cache-scalar-witness-floor/verify.py new file mode 100644 index 0000000000..2eeebdb681 --- /dev/null +++ b/research/partial-cache-scalar-witness-floor/verify.py @@ -0,0 +1,291 @@ +#!/usr/bin/env python3 +"""Exact optimum of the scalar-witness error floor for the partial-cache observer. + +The observation rows come from JoyboyBrian's PR5498 replay, imported only after +its bytes match SOURCES.json. The physical norm convention is Ali Romman's +PR5537; the provider basis and target are Dillon Amburgey's PR5402. +New optimization and certificate: Nick Petalas. Apache-2.0. +""" +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import argparse +import importlib.util +import json + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +ORIGINAL = 632 +MODES = 8 +FLOOR = F(7, 92) +KERNEL_DIM = 150 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def pinned(): + manifest = json.loads((HERE/'SOURCES.json').read_text()) + out = {} + for pin in manifest['files']: + if pin['usage'] != 'input': + continue + raw = (ROOT/pin['path']).read_bytes() + need(sha256(raw).hexdigest() == pin['sha256'], 'source drift '+pin['path']) + out[pin['path']] = raw + return out + + +def observer_module(): + path = ROOT/'research/partial-cache-history-observer/verify.py' + spec = importlib.util.spec_from_file_location('pr5498_observer', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def constraint_rows(rows): + """One linear form on the 632 original roles per (observed row, free word).""" + out = {} + for row in rows: + by_word = {} + for (owner, word), value in row.items(): + need(owner < ORIGINAL, 'observed row carries owned-input dirt') + by_word.setdefault(word, {})[owner] = value + for form in by_word.values(): + out[tuple(sorted(form.items()))] = form + return list(out.values()) + + +def reduce_against(row, pivots): + while True: + hit = next((j for j in row if j in pivots), None) + if hit is None: + return row + factor = row[hit] + for k, v in pivots[hit].items(): + value = row.get(k, F(0)) - factor*v + if value: + row[k] = value + else: + row.pop(k, None) + + +def kernel_basis(forms): + """Exact reduced row echelon form; returns free roles and kernel basis.""" + pivots = {} + for form in forms: + row = reduce_against(dict(form), pivots) + if not row: + continue + lead = min(row) + scale = row[lead] + row = {k: v/scale for k, v in row.items()} + for other in pivots.values(): + factor = other.get(lead) + if factor: + for k, v in row.items(): + value = other.get(k, F(0)) - factor*v + if value: + other[k] = value + else: + other.pop(k, None) + pivots[lead] = row + free = [j for j in range(ORIGINAL) if j not in pivots] + basis = [] + for f in free: + vector = [F(0)]*ORIGINAL + vector[f] = F(1) + for lead, row in pivots.items(): + vector[lead] = -row.get(f, F(0)) + basis.append(vector) + return free, basis + + +def run_basis(ops, vector): + out = list(vector) + for op in ops: + if op[0] == 'add': + out[op[1]] += F(op[3])*out[op[2]] + else: + need(op[0] == 'scale' and F(op[2]) != 0, 'basis operation') + out[op[1]] *= F(op[2]) + return out + + +def physical(provider, raw): + """PR5537 convention: decode the helper basis, then undo the 2Km mode entrance.""" + decoded = run_basis(provider['output_basis_program'], list(raw)+[F(0)]*9) + for role in provider['mode_owners']: + decoded[role] /= 2 + return decoded[:ORIGINAL] + + +def target(mode_columns, raw): + return [sum(F(a)*b for a, b in zip(row, raw[112:224]))/2 for row in mode_columns] + + +def dot(u, v): + return sum(a*b for a, b in zip(u, v)) + + +def solve_spd(gram, rhs): + """Gauss-Jordan without row swaps; every pivot must be positive (G is SPD).""" + n = len(gram) + a = [gram[i][:]+rhs[i][:] for i in range(n)] + pivots = [] + for c in range(n): + need(a[c][c] > 0, 'Gram matrix is not positive definite') + pivots.append(a[c][c]) + inv = 1/a[c][c] + a[c] = [x*inv for x in a[c]] + for r in range(n): + if r != c and a[r][c]: + f = a[r][c] + a[r] = [x-f*y for x, y in zip(a[r], a[c])] + return [row[n:] for row in a], pivots + + +def integral(vector): + from math import lcm, gcd + den = 1 + for x in vector: + den = lcm(den, x.denominator) + ints = [int(x*den) for x in vector] + g = 0 + for x in ints: + g = gcd(g, x) + return [F(x, g) for x in ints] + + +def ratio(provider, mode_columns, k): + return dot(target(mode_columns, k), target(mode_columns, k)), dot(physical(provider, k), physical(provider, k)) + + +def annihilates(observer, rows, k): + displacement = {j: x for j, x in enumerate(k) if x} + return all(not observer.residual(row, displacement) for row in rows) + + +def verify(): + pinned() + observer = observer_module() + data = observer.inputs() + provider, normal = data['PROVIDER.json'], data['NORMALIZERS.json'] + m = normal['mode_columns'] + histories, rows, frames, touches = observer.replay( + data['ACTUAL-WORD.json.gz']['canonical'], data['WORD.json.gz']['word']) + need(len(histories) == 4891, 'PR5498 distinct full-frame history count') + observed = [row for _, _, row in histories]+[rows[j] for j in range(633, 641)] + forms = constraint_rows(observed) + free, basis = kernel_basis(forms) + need(len(basis) == KERNEL_DIM, 'scalar kernel dimension') + for vector in basis: + need(annihilates(observer, observed, vector), 'basis vector leaves the kernel') + + phys = [physical(provider, b) for b in basis] + gram = [[dot(u, v) for v in phys] for u in phys] + c = [target(m, b) for b in basis] + x, gram_pivots = solve_spd(gram, c) + for i in range(len(basis)): + need([dot(gram[i], [x[r][a] for r in range(len(basis))]) for a in range(MODES)] == c[i], + 'G X = C') + s = [[sum(c[i][a]*x[i][b] for i in range(len(basis))) for b in range(MODES)] for a in range(MODES)] + need(s == [[FLOOR if a == b else F(0) for b in range(MODES)] for a in range(MODES)], + 'C^T G^-1 C = (7/92) I') + + witnesses = [] + for a in range(MODES): + k = integral([sum(x[i][a]*basis[i][r] for i in range(len(basis))) for r in range(ORIGINAL)]) + need(annihilates(observer, observed, k), 'optimal witness annihilates every observation') + t = target(m, k) + need(all(t[b] == 0 for b in range(MODES) if b != a) and t[a] != 0, 'one-mode target') + top, bottom = ratio(provider, m, k) + need(top/bottom == FLOOR, 'witness attains 7/92') + witnesses.append({'mode': a, 'nonzero_raw_roles': sum(1 for v in k if v), + 'nonzero_physical_roles': sum(1 for v in physical(provider, k) if v), + 'target_norm_squared': str(top), 'physical_norm_squared': str(bottom), + 'raw': [[j, str(v)] for j, v in enumerate(k) if v]}) + + old = [F(0)]*ORIGINAL + for j, value in json.loads((ROOT/'research/partial-cache-history-observer/KERNEL.json').read_text())[ + 'original_input_displacement']: + old[j] = F(value) + need(annihilates(observer, observed, old), 'PR5498 witness lies in the scalar kernel') + old_top, old_bottom = ratio(provider, m, old) + need(old_top/old_bottom == F(1, 19) < FLOOR, 'PR5537 floor 1/19 is strictly smaller') + return {'basis': basis, 'free': free, 'forms': forms, 'gram_pivots': gram_pivots, + 'observed': observed, 'observer': observer, 'provider': provider, 'm': m, + 'witnesses': witnesses, 'touches': touches, 'histories': len(histories), + 'old': (old_top, old_bottom)} + + +def controls(state): + """Each mutation must be rejected or must change the computed optimum.""" + out = {} + observer, observed = state['observer'], state['observed'] + k = [F(0)]*ORIGINAL + for j, v in state['witnesses'][1]['raw']: + k[j] = F(v) + support = [j for j, v in enumerate(k) if v] + bumped = list(k) + bumped[support[0]] += 1 + need(not annihilates(observer, observed, bumped), 'perturbed witness accepted') + out['perturbed_witness_rejected'] = True + # Without the eight PR5498 caches the scalar kernel is larger and the optimum differs. + full_only = constraint_rows(observed[:-8]) + free, basis = kernel_basis(full_only) + need(len(basis) > KERNEL_DIM, 'caches add no constraint') + out['kernel_dim_without_caches'] = len(basis) + phys = [physical(state['provider'], b) for b in basis] + gram = [[dot(u, v) for v in phys] for u in phys] + c = [target(state['m'], b) for b in basis] + x, _ = solve_spd(gram, c) + diag = [sum(c[i][a]*x[i][a] for i in range(len(basis))) for a in range(MODES)] + need(max(diag) > FLOOR, 'cache-free optimum must exceed the observed-channel optimum') + out['cache_free_mode_diagonal_max'] = str(max(diag)) + # The raw (non-physical) norm gives a different constant: the basis matters. + raw_top = dot(target(state['m'], k), target(state['m'], k)) + need(raw_top/dot(k, k) != FLOOR, 'raw norm coincides with physical norm') + out['raw_norm_ratio_of_mode1_witness'] = str(raw_top/dot(k, k)) + return out + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + state = verify() + w1 = state['witnesses'][1] + result = { + 'status': 'PASS_PARTIAL_CACHE_SCALAR_WITNESS_FLOOR', + 'distinct_full_frame_histories': state['histories'], + 'endpoint_caches': 8, + 'distinct_word_constraints': len(state['forms']), + 'constraint_rank': ORIGINAL-len(state['basis']), + 'scalar_kernel_dimension': len(state['basis']), + 'gram_positive_pivots': len(state['gram_pivots']), + 'optimal_squared_floor': str(FLOOR), + 'optimal_floor_decimal_lower': '0.27583', + 'previous_squared_floor': str(state['old'][0]/state['old'][1]), + 'optimum_matrix': '(7/92) I_8', + 'mode1_witness': w1, + 'per_mode_witness_supports': [[w['nonzero_raw_roles'], w['nonzero_physical_roles']] + for w in state['witnesses']], + 'controls': controls(state), + 'scope': 'exact optimum over scalar witnesses k(x)v in the PR5498 free-word observation ' + 'grammar under PR5537 physical norms; lower bound on ||T restricted to ker O||, ' + 'not that norm; no kappa change', + } + need(F(27583, 100000)**2 < FLOOR, 'decimal floor is a lower bound') + if not args.emit: + expected = json.loads((HERE/'RESULT.json').read_text()) + need(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + 'receipt mismatch') + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == '__main__': + main()