From 89f9f9e89210065ccd7343b4a7fb0a2fb8abf38e Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 21:59:57 -0700 Subject: [PATCH 1/2] Prove sharp scalar primes for uniform resonant recovery --- research/resonant-recovery-scalars/README.md | 237 ++++++++++++++++++ .../resonant-recovery-scalars/RESULT.json | 116 +++++++++ .../resonant-recovery-scalars/SOURCES.json | 42 ++++ research/resonant-recovery-scalars/TASK.json | 72 ++++++ .../resonant-recovery-scalars/VERIFY.json | 33 +++ research/resonant-recovery-scalars/verify.py | 151 +++++++++++ 6 files changed, 651 insertions(+) create mode 100644 research/resonant-recovery-scalars/README.md create mode 100644 research/resonant-recovery-scalars/RESULT.json create mode 100644 research/resonant-recovery-scalars/SOURCES.json create mode 100644 research/resonant-recovery-scalars/TASK.json create mode 100644 research/resonant-recovery-scalars/VERIFY.json create mode 100644 research/resonant-recovery-scalars/verify.py diff --git a/research/resonant-recovery-scalars/README.md b/research/resonant-recovery-scalars/README.md new file mode 100644 index 0000000000..98c9a9ce79 --- /dev/null +++ b/research/resonant-recovery-scalars/README.md @@ -0,0 +1,237 @@ +# Unavoidable scalar primes in uniform resonant image recovery + +For the frozen resonant channel of [PR #4797](https://github.com/CrocSwap/integer-mult-bounds/pull/4797), +exact uniform recovery of its **canonical orthogonal input projection** needs +the odd scalar primes **3, 5 and 7**, and these primes suffice. This is a +statement about a precisely defined coefficient ring and uniform linear +program, not a physical lower bound for division or a complete supplier. + +Dugongue's [PR #4885](https://github.com/CrocSwap/integer-mult-bounds/pull/4885) +already proves the all-width rank, support projectors and explicit polynomial +pseudoinverse. Those results are credited predecessors, not new claims here. +The new result shows that the odd denominators cannot all be removed by a +different finite uniform monomial-linear decoder with the same orthogonal +output contract. It distinguishes an actual arithmetic obligation from a +possibly inconvenient choice of inverse polynomial. + +Canonical claim: [Discussion #1166, comment 19138314](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138314). +Base: `b91956876e5b4122fd89179f1b57557ff8378f15`, priority revision 7. + +## Exact contract and theorem + +Let `A` be the 256 actual three-bit monomial words with rational coefficients +`±1/16` in the source `TARGET.json`. A word `g=(p,s)` acts by +`g e_j = i^s(j) e_p(j)`. Every actual central phase is retained. For positive +width `f`, evaluation is + +``` +A_f = sum_g a_g g^(tensor f). +``` + +Coefficients occur once, outside tensor powers. For a set `S` of odd rational +primes define `R_S = Z[i,1/2,{1/p : p in S}]`. In particular `S=empty` is the +Gaussian dyadic ring. Let `P_f` be the orthogonal projection onto `im A_f*`, +the canonical accessible input subspace. The desired output from observation +`z=A_f y`, for every arbitrary `y in C^(8^f)`, is exactly `P_f y`. + +**Theorem.** There is a fixed finite monomial-linear decoder with scalar +coefficients in `R_S`, valid at **every positive even width** `f=2,4,6,...`, +if and only if `{3,5,7}` is contained in `S`. + +“Fixed finite” means a finite straight-line algebraic program independent of +`f`: its scalar coefficients and its base monomial words are fixed. A lifted +base word may of course be executed by an address loop over `8^f` entries. +The program may copy registers, add them, multiply by scalars in `R_S`, and +apply lifted monomials. It can use any fixed finite number of zero registers +or independent arbitrary dirty inputs, with the declared dirty returns. +Its designated output must be `P_f y` for all those independent inputs. + +For necessity we even grant **all** fourth-root monomial three-bit base +matrices, a larger alphabet than the actual affine/phase engine. Sufficiency +uses the actual words of `A` and their products/adjoints, already certified +free in #4797. No inversion of an arbitrary register operator is a free +instruction. This theorem is not about arbitrary oblique representatives, +width-dependent scalar constants/circuit families, approximate output, +nonlinear bit arithmetic, or a decoder given extra correlated paid responses. +It determines scalar availability, not the number or runtime of divisions. + +## Source-bound projector certificate + +Write `C=A* A/16`. The authenticated #4885 checker reconstructs the exact +integer group algebra on 21,504 actual monomials. Its degree-18 polynomial is +`p(t)=t q(t)`, with + +``` +q(0) = -40131624960 = -2^19 * 3^7 * 5 * 7, +C q(C) = 0. +``` + +This integer identity, not a finite tensor-width sample or modular guess, +is replayed here. `C_f` is Hermitian positive semidefinite. Therefore + +``` +P = I - q(C)/q(0) +``` + +evaluates to `P_f` at every positive width: it is zero on the zero eigenspace +and one on each nonzero eigenspace. We use that source-bound polynomial to +compute exact coefficients; the rank formula itself need not be rerun. + +### The correct quotient for even widths + +For every even width, `[g]` and `[-g]` have the same evaluation. Define +`bar H = H/{I,-I}`. The projector coefficient of an even class is the **sum** +of the two signed-word coefficients, not a choice of one representative. +The checker normalizes a word by subtracting either 0 or 2 from every phase +exponent, so its first phase exponent lies in `{0,1}`. The central class of +`iI` remains different from identity: at width `2k` it evaluates to `(-1)^k I`. + +The full source projector has 21,056 nonzero word coefficients. Its even +quotient has 10,528 nonzero classes and minimal integer coefficient-clearing +denominator + +``` +3870720 = 2^12 * 3^3 * 5 * 7. +``` + +One explicit class simultaneously witnesses all three odd primes: + +``` +permutation = (0,1,3,2,4,5,7,6) +phase_i = (0,0,1,3,0,0,3,1) +coefficient = 1243/3870720. +``` + +The numerator is coprime to the denominator. Each separate signed word has +half this coefficient. `verify.py` recomputes all exact rational coefficients, +the entire denominator histogram and this witness from the pinned source +annihilator. The denominator is measured in the correct all-even quotient, +not in one concrete matrix or in the unreduced inverse polynomial. + +### Why all-even evaluation is faithful + +Take finitely many distinct classes represented by nonzero matrices `g_j`. +The tensors `u_j=g_j tensor g_j` are nonzero and pairwise distinct. Indeed, +`g tensor g=h tensor h` implies `h=alpha g` and `alpha^2=1`, hence precisely +`h=±g`. To see the proportionality directly, apply a nonzero coordinate of +`g` to the first factor of the equality; then substitute the proportionality +back into the equality. + +Choose a complex linear functional `ell` on the matrix-tensor space for +which all numbers `alpha_j=ell(u_j)` are distinct and nonzero. Such a choice +avoids a finite union of proper hyperplanes. If +`sum_j c_j g_j^(tensor 2k)=0` for every `k>=1`, applying `ell^(tensor k)` gives +`sum_j c_j alpha_j^k=0`. For `k=1,...,m`, the resulting Vandermonde matrix is +invertible, including the nonzero factors `alpha_j`. Thus every `c_j=0`. + +This proves faithfulness of the family of all positive even evaluations on +finite elements of `C[bar H]`. It does not assert faithfulness at any one +width. In particular quarter phases must not be discarded; restricting to +widths divisible by four would be a different quotient and a different task. + +## Necessity for every allowed decoder + +By induction over its instructions, each output of a fixed finite linear +program is a finite sum of lifted monomial words applied to each independent +input, with coefficients in `R_S`. At the designated output, independence of +the arbitrary auxiliary values forces their transfer coefficients to vanish +under every required evaluation. Zero scratch and restored dirty scratch +cannot change the coefficient of `z`. Consequently there is a finite +`L in R_S[H]` such that the output is `L_f z` for all widths in the contract. + +Exact recovery from `z=A_f y` implies `(LA)_f=P_f` at every positive even +width and for every `y`. Since `A` is dyadic, `LA` has coefficients in `R_S`. +All-even faithfulness forces equality in `C[bar H]`. The coefficient at the +explicit witness class must therefore equal `1243/3870720` in `R_S`. + +The rational elements of `R_S` have denominators supported only at 2 and +primes in `S`: take real and imaginary parts of a Gaussian-integer numerator +over such an integer denominator. Since the witness is reduced, each of +3, 5 and 7 must belong to `S`. This proves necessity for all allowed decoders, +not only for the particular pseudoinverse in #4885. + +## Sufficiency uses an actual decoder + +Being able to write `P` in a ring alone would not establish recovery from +`A y`. Instead use the explicit source inverse polynomial + +``` +R(t) = -(q(t)-q(0))/(t q(0)), +L = R(C) A* / 16. +``` + +The exact scalar identity `t R(t)=1-q(t)/q(0)` gives `LA=P`. All coefficients +of `q` are integers, `C` has dyadic coefficients, and division by `q(0)` +introduces exactly the possible odd primes 3,5,7 and no others. Therefore +this particular finite decoder lies in `Z[i,1/2,1/3,1/5,1/7][H]` and is +constructively available whenever those primes are inverted. `verify.py` +checks the scalar polynomial identity and the actual `q(0)` factorization +separately from the projector-denominator calculation. + +This is a uniform linear program with a finite number of actual monomial +passes; it is not a claim that fixed-rational scalar operations cost nothing. +Dugongue's [PR #4908](https://github.com/CrocSwap/integer-mult-bounds/pull/4908) +already implements bounded-word fixed-rational rounding with a specified +both-shifts ABI. That algorithm and its conditional tariff are credited +inputs, not newly implemented here. Exact complex-linear algebra and rounded +finite-precision execution are different contracts. + +## Validation and limits + +Run the registered package with Python 3.12: + +``` +python3 scripts/research_package.py --package research/resonant-recovery-scalars +``` + +The primary checker authenticates #4885's executable/source coefficient before +loading it, replays its exact integer annihilator, and derives the new quotient +and localization certificates. Explicit checks remain active under `-O`. +A separate independent modular witness check is planned for the next +implementation checkpoint; it is not part of this initial certificate. +Finite corroboration will not replace the written all-width proof. + +| Obligation | Status | +|---|---| +| All-width rank and explicit support inverse | Inherited from #4885 | +| Correct even-phase quotient and faithfulness | Proved here | +| Necessary scalar primes for any decoder in the declared grammar | Proved here | +| Same primes sufficient for an actual recovery decoder | Constructive source polynomial, checked here | +| Fixed-rational rounded scalar implementation | Credited #4908, conditional on its ABI and precision contract | +| Independent canonical Gaussian target encoders | Unknown | +| Missing target complement, physical preparation/routing/storage/restoration | Unknown | +| Complete paid profile, compiler funding, supplier admission and new κ | Not established | + +The original retained owners and complements of #4797 are unchanged. This +coefficient-ring obstruction gives no universal lower bound for native +restoration and excludes no approximate, oblique or width-dependent decoder. +The exact source replay and independent finite checks are not human or +proof-kernel acceptance. No selected-frontier or frozen predecessor is changed. + +## Provenance and overlap + +All-width source head: #4885 `46ece2fbfb6d7c23c82c42797855deac7204235e`. +Its executable and target are live inputs pinned by raw bytes in `SOURCES.json`. +The #4797 source channel and #4825 width-four rank are preserved through that +lineage. Credit Dugongue for the all-width projector/inverse and #4908 +(`7662641e7016a3e38826fd5a9e73c30db751452b`) arithmetic; Nick Petalas for +#4825; JoyboyBrian for #4797; and Yiyang #4710, lee-phys #4688 and Jacob +Sussman #4628 for the phase-prefix and actual free-alphabet lineage. +Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. + +Initial overlap covered 317 open PRs, 4064 Discussion records and all 6636 local +notes. Exact resonant/dyadic terms had no matching result; this is advisory, +not a novelty certificate. #4902/#4932/#4943 concern distinct coded-native +caller obligations. The former all-even rank task was explicitly replaced +because #4885 had already solved it. No scalar rounding algorithm is repeated. + +## Open next questions + +1. Can a different, oblique exact accessible-coordinate contract avoid these + primes while retaining the same amount of information? Begin with an + explicit uniform decoder/section; changing the output contract invalidates + the necessity proof above and requires a new consumer ledger. +2. Can a complete chronological consumer afford the known rational recovery + and all missing coordinates? Specify canonical encoders and every physical + preparation, complement, restoration and compiler charge before expansion. + The present ring criterion does not supply that consumer or a saving. diff --git a/research/resonant-recovery-scalars/RESULT.json b/research/resonant-recovery-scalars/RESULT.json new file mode 100644 index 0000000000..04620683f9 --- /dev/null +++ b/research/resonant-recovery-scalars/RESULT.json @@ -0,0 +1,116 @@ +{ + "denominator_histogram": { + "128": 16, + "129024": 128, + "1290240": 608, + "138240": 208, + "143360": 64, + "18432": 160, + "184320": 64, + "193536": 96, + "1935360": 1408, + "215040": 128, + "24192": 128, + "256": 32, + "258048": 320, + "27648": 48, + "276480": 192, + "28672": 64, + "322560": 128, + "3870720": 2976, + "430080": 224, + "48384": 128, + "483840": 128, + "55296": 96, + "552960": 608, + "61440": 64, + "645120": 320, + "86016": 128, + "9216": 176, + "92160": 128, + "96768": 304, + "967680": 1456 + }, + "even_projector_coefficient_lcd": 3870720, + "even_quotient_support": 10528, + "lcd_factorization": { + "2": 12, + "3": 3, + "5": 1, + "7": 1 + }, + "necessary_and_sufficient_odd_primes": [ + 3, + 5, + 7 + ], + "negative_controls": [ + "omit_scalar_prime_3", + "omit_scalar_prime_5", + "omit_scalar_prime_7", + "do_not_collapse_quarter_phase", + "do_not_drop_negative_representative", + "inverse_polynomial_sign" + ], + "recovery": { + "R_low_first": [ + "6901/1260", + "-40883/3024", + "3625927/181440", + "-5396329/272160", + "45812933/3265920", + "-7986799/1088640", + "909602303/313528320", + "-183815213/209018880", + "17206361/83607552", + "-18678097/501645312", + "3251743/627056640", + "-689681/1254113280", + "436759/10032906240", + "-713/286654464", + "971/10032906240", + "-23/10032906240", + "1/40131624960" + ], + "formula": "R(A* A / 16) A* / 16", + "q0": -40131624960, + "q0_factorization": { + "2": 19, + "3": 7, + "5": 1, + "7": 1 + } + }, + "scope": "Fixed finite uniform monomial-linear exact recovery of the canonical orthogonal input projection, over Z[i,1/2,1/S], for every positive even width. No oblique, width-dependent, approximate or physical-runtime obstruction.", + "source_group_order": 21504, + "source_pins": { + "TARGET.json": "e7df852b5c641f326ac67cd35cea8da6cfdd059fa12df1cf6fb758bb4206d684", + "verify.py": "29554fca57ad1b91469cbd65543882ebdaf8cafa93b8dc2ff37b00baef03e930" + }, + "source_projector_support": 21056, + "status": "PASS_RESONANT_RECOVERY_SCALARS", + "witness": { + "coefficient": "1243/3870720", + "permutation": [ + 0, + 1, + 3, + 2, + 4, + 5, + 7, + 6 + ], + "phase_i": [ + 0, + 0, + 1, + 3, + 0, + 0, + 3, + 1 + ], + "single_signed_word_coefficient": "1243/7741440" + } +} diff --git a/research/resonant-recovery-scalars/SOURCES.json b/research/resonant-recovery-scalars/SOURCES.json new file mode 100644 index 0000000000..9cd27fca16 --- /dev/null +++ b/research/resonant-recovery-scalars/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/resonant-all-width-projector/TARGET.json", + "usage": "input", + "git_blob": "e40739b7d5fb91c1a0473b6bb5b3f449fc9d60ae", + "sha256": "e7df852b5c641f326ac67cd35cea8da6cfdd059fa12df1cf6fb758bb4206d684" + }, + { + "path": "research/resonant-all-width-projector/verify.py", + "usage": "input", + "git_blob": "f2585ea76c22b3c9bb6e430401bf7664e1808490", + "sha256": "29554fca57ad1b91469cbd65543882ebdaf8cafa93b8dc2ff37b00baef03e930" + }, + { + "path": "research/resonant-all-width-projector/PROOF.md", + "usage": "provenance", + "git_blob": "2a65c15bebaa9096d79dea2f0e898cdeee0b4ac4", + "sha256": "a11f8a97519ae94982b1a212d2cc9789d82a4452317eb1d3843080caf910c45c" + }, + { + "path": "research/native-cyclic-recovery/README.md", + "usage": "provenance", + "git_blob": "2c509511f95b730f88b7eb6bc27eb7caad49bf87", + "sha256": "445a4258ca34b0c26dd6d569884c3f489bcaef94e1987c285f55857ac09476db" + } + ] +} diff --git a/research/resonant-recovery-scalars/TASK.json b/research/resonant-recovery-scalars/TASK.json new file mode 100644 index 0000000000..c3f65bce5a --- /dev/null +++ b/research/resonant-recovery-scalars/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "b91956876e5b4122fd89179f1b57557ff8378f15", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Determine the necessary and sufficient rational scalar primes for fixed finite uniform monomial-linear recovery of the frozen resonant channel canonical orthogonal input projection at every positive even width.", + "scope_change_reason": "The assigned general even-width rank problem is already solved by Dugongue PR4885. This complementary arithmetic question asks whether the inverse polynomial odd denominators are avoidable under a different decoder; it neither repeats that rank theorem nor PR4908 fixed-rational rounding.", + "bottleneck_link": "Separates the exact Gaussian-dyadic linear decoder contract from rational orthogonal recovery, identifying genuinely required scalar services without assigning their physical runtime zero.", + "budget_minutes": 60, + "stop_rule": "At most45 minutes for the quantified coefficient-ring theorem and exact/independent finite certificates, with15 minutes reserved for review and committed Git-free replay. Stop if the denominators disappear after the correct even phase quotient or merely restate the source inverse.", + "outcome": "partial", + "evidence": "README proves the finite-support all-even tensor faithfulness and sharp localization theorem. verify.py derives the exact even projector LCD and witness, and separately verifies the actual sufficient decoder polynomial.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, exact implementation and source review; no independent human or proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can a uniform oblique accessible-coordinate decoder avoid odd scalar services?", + "why_it_matters": "The canonical orthogonal output contract is essential to this necessity theorem.", + "first_step": "Specify an actual oblique projection and a uniform decoder/section with full information and complement accounting.", + "blocked_by": "No oblique decoder or complete charged consumer has been constructed." + }, + { + "question": "Can a complete chronological supplier afford rational recovery and missing coordinates?", + "why_it_matters": "A scalar-localization theorem is not a paid-saving theorem.", + "first_step": "Bind canonical encoders, actual scalar tariff, physical preparation, complement, storage/routing/restoration and compiler bill.", + "blocked_by": "All complete consumer and supplier obligations remain open." + } + ] +} diff --git a/research/resonant-recovery-scalars/VERIFY.json b/research/resonant-recovery-scalars/VERIFY.json new file mode 100644 index 0000000000..af2edf11d5 --- /dev/null +++ b/research/resonant-recovery-scalars/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/resonant-all-width-projector/TARGET.json", + "research/resonant-all-width-projector/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 45, + "checks": "Authenticated exact source annihilator; even-class projector LCD/witness; sharp prime requirement and actual sufficient decoder polynomial." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 45, + "checks": "Same explicit exact checks under optimized Python." + } + ] +} diff --git a/research/resonant-recovery-scalars/verify.py b/research/resonant-recovery-scalars/verify.py new file mode 100644 index 0000000000..c716c900ba --- /dev/null +++ b/research/resonant-recovery-scalars/verify.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Exact scalar localization for the source-bound resonant support recovery.""" +import argparse +from collections import Counter +from fractions import Fraction +import hashlib +import json +import math +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +SOURCE = 'research/resonant-all-width-projector' +SOURCE_PINS = { + 'verify.py': '29554fca57ad1b91469cbd65543882ebdaf8cafa93b8dc2ff37b00baef03e930', + 'TARGET.json': 'e7df852b5c641f326ac67cd35cea8da6cfdd059fa12df1cf6fb758bb4206d684', +} +WITNESS = ((0, 1, 3, 2, 4, 5, 7, 6), (0, 0, 1, 3, 0, 0, 3, 1)) +EXPECTED_COEFFICIENT = Fraction(1243, 3870720) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def factor(number): + number = abs(number) + require(number > 0, 'factor positive integer') + out = {} + prime = 2 + while prime * prime <= number: + while number % prime == 0: + out[prime] = out.get(prime, 0) + 1 + number //= prime + prime += 1 + if number > 1: + out[number] = 1 + return out + + +def even_class(word): + """Canonical representative modulo precisely the actual central {-I,I}.""" + permutation, phase = word + subtract = 2 * (phase[0] // 2) + return permutation, tuple((x - subtract) % 4 for x in phase) + + +def load_source(): + for filename, expected in SOURCE_PINS.items(): + data = (ROOT / SOURCE / filename).read_bytes() + require(hashlib.sha256(data).hexdigest() == expected, 'source hash: ' + filename) + source = ROOT / SOURCE / 'verify.py' + module = types.ModuleType('pinned_resonant_projector') + module.__file__ = str(source) + exec(compile(source.read_bytes(), str(source), 'exec'), module.__dict__) + return module + + +def verify(): + source = load_source() + raw, ds, b, d, H = source.load_factorization() + group, apply_H, identity, hv = source.build_action(b, d, H) + numer, denominator, bound = source.polynomial_certificate(group, apply_H, identity) + # Source checks the exact integer annihilator, not just a sampled spectrum. + coefficients = {g: Fraction(n, denominator) for g, n in zip(group, numer) if n} + minus = (tuple(range(8)), (2,) * 8) + for g, c in coefficients.items(): + require(coefficients.get(source.mul(minus, g), 0) == c, 'central minus invariance') + quotient = {} + for g, c in coefficients.items(): + key = even_class(g) + quotient[key] = quotient.get(key, Fraction()) + c + quotient = {g: c for g, c in quotient.items() if c} + require(len(group) == 21504 and len(coefficients) == 21056 and len(quotient) == 10528, + 'group/projector/even-class support counts') + lcd = math.lcm(*(c.denominator for c in quotient.values())) + require(lcd == 3870720, 'minimal even-class coefficient denominator') + require(factor(lcd) == {2: 12, 3: 3, 5: 1, 7: 1}, 'denominator factorization') + require(quotient[WITNESS] == EXPECTED_COEFFICIENT, 'explicit simultaneous odd-prime witness') + require(math.gcd(EXPECTED_COEFFICIENT.numerator, lcd) == 1, 'witness reduced') + + # Sufficiency concerns a decoder, not merely coefficients of P. + # q is source POLY/x; R(t)=-(q(t)-q(0))/(t*q(0)). + q = source.POLY[1:] + require(q[0] == -40131624960, 'source nonzero constant') + q0_factors = factor(q[0]) + require(q0_factors == {2: 19, 3: 7, 5: 1, 7: 1}, 'actual decoder scalar prime set') + inverse_poly = [-Fraction(c, q[0]) for c in q[1:]] + # Polynomial tR(t)=1-q(t)/q(0), before evaluating C=A*A/16. + left = [Fraction()] + inverse_poly + right = [Fraction(1)] + [Fraction()] * (len(q) - 1) + right = [a - Fraction(c, q[0]) for a, c in zip(right, q)] + require(left == right, 'actual recovery polynomial identity') + allowed = {2, 3, 5, 7} + require(all(set(factor(c.denominator)) <= allowed for c in inverse_poly), 'inverse polynomial localization') + records = json.loads(raw) + require(all(Fraction(r['coefficient']).denominator == 16 for r in records), 'A is dyadic') + # C and A*/16 add only powers of 2; R(C)A*/16 is the actual sufficient decoder. + controls = [] + for missing in (3, 5, 7): + available = allowed - {missing} + require(not set(factor(EXPECTED_COEFFICIENT.denominator)) <= available, + 'missing-prime ring incorrectly admitted') + controls.append('omit_scalar_prime_' + str(missing)) + iword = (tuple(range(8)), (1,) * 8) + require(even_class(minus) == source.IDENTITY and even_class(iword) != source.IDENTITY, + 'only signs are identified') + controls.append('do_not_collapse_quarter_phase') + require(even_class(WITNESS) == WITNESS and quotient[WITNESS] != coefficients[WITNESS], + 'both signs contribute to even coefficient') + controls.append('do_not_drop_negative_representative') + bad_left = left[:] + bad_left[1] = -bad_left[1] + require(bad_left != right, 'inverse sign mutation') + controls.append('inverse_polynomial_sign') + return { + 'status': 'PASS_RESONANT_RECOVERY_SCALARS', + 'source_pins': SOURCE_PINS, + 'source_group_order': len(group), + 'source_projector_support': len(coefficients), + 'even_quotient_support': len(quotient), + 'even_projector_coefficient_lcd': lcd, + 'lcd_factorization': {str(p): e for p, e in factor(lcd).items()}, + 'witness': {'permutation': list(WITNESS[0]), 'phase_i': list(WITNESS[1]), + 'coefficient': str(quotient[WITNESS]), + 'single_signed_word_coefficient': str(coefficients[WITNESS])}, + 'denominator_histogram': {str(d): count for d, count in sorted(Counter(c.denominator for c in quotient.values()).items())}, + 'recovery': {'q0': q[0], 'q0_factorization': {str(p): e for p, e in q0_factors.items()}, + 'R_low_first': list(map(str, inverse_poly)), 'formula': 'R(A* A / 16) A* / 16'}, + 'necessary_and_sufficient_odd_primes': [3, 5, 7], + 'negative_controls': controls, + 'scope': 'Fixed finite uniform monomial-linear exact recovery of the canonical orthogonal input projection, over Z[i,1/2,1/S], for every positive even width. No oblique, width-dependent, approximate or physical-runtime obstruction.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = verify() + target = HERE / 'RESULT.json' + if args.write: + target.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(json.loads(target.read_text()) == result, 'frozen receipt') + print(result['status']) + + +if __name__ == '__main__': + main() From 14207858d300b42cc628891f41397b124a4b8bf6 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Thu, 22 Oct 2026 22:06:42 -0700 Subject: [PATCH 2/2] Independently certify resonant denominator valuations --- .../INDEPENDENT.json | 43 ++++ research/resonant-recovery-scalars/README.md | 34 ++- research/resonant-recovery-scalars/TASK.json | 6 +- .../resonant-recovery-scalars/VERIFY.json | 21 ++ .../independent_modular.py | 208 ++++++++++++++++++ 5 files changed, 303 insertions(+), 9 deletions(-) create mode 100644 research/resonant-recovery-scalars/INDEPENDENT.json create mode 100644 research/resonant-recovery-scalars/independent_modular.py diff --git a/research/resonant-recovery-scalars/INDEPENDENT.json b/research/resonant-recovery-scalars/INDEPENDENT.json new file mode 100644 index 0000000000..dfe9b4525a --- /dev/null +++ b/research/resonant-recovery-scalars/INDEPENDENT.json @@ -0,0 +1,43 @@ +{ + "even_witness_raw_residue": 2754, + "group_size": 21504, + "modulus": 8505, + "negative_controls": [ + "omit_negative_word", + "constant_polynomial_mutation", + "quarter_phase_collapse_at_width_two", + "inverse_orientation" + ], + "odd_prime_valuations": [ + { + "denominator_valuation": 7, + "modulus": 243, + "numerator_valuation": 4, + "prime": 3, + "raw_numerator_residue": 81, + "reduced_denominator_valuation": 3 + }, + { + "denominator_valuation": 1, + "modulus": 5, + "numerator_valuation": 0, + "prime": 5, + "raw_numerator_residue": 4, + "reduced_denominator_valuation": 1 + }, + { + "denominator_valuation": 1, + "modulus": 7, + "numerator_valuation": 0, + "prime": 7, + "raw_numerator_residue": 3, + "reduced_denominator_valuation": 1 + } + ], + "scope": "Independent finite modular corroboration of the exact source projector coefficient; not a replacement for exact integer or all-even faithfulness proofs.", + "source_pins": { + "TARGET.json": "e7df852b5c641f326ac67cd35cea8da6cfdd059fa12df1cf6fb758bb4206d684", + "verify.py": "29554fca57ad1b91469cbd65543882ebdaf8cafa93b8dc2ff37b00baef03e930" + }, + "status": "PASS_INDEPENDENT_RESONANT_SCALARS" +} diff --git a/research/resonant-recovery-scalars/README.md b/research/resonant-recovery-scalars/README.md index 98c9a9ce79..9ddb799d47 100644 --- a/research/resonant-recovery-scalars/README.md +++ b/research/resonant-recovery-scalars/README.md @@ -46,8 +46,9 @@ apply lifted monomials. It can use any fixed finite number of zero registers or independent arbitrary dirty inputs, with the declared dirty returns. Its designated output must be `P_f y` for all those independent inputs. -For necessity we even grant **all** fourth-root monomial three-bit base -matrices, a larger alphabet than the actual affine/phase engine. Sufficiency +Let `H` be the group of all fourth-root monomial three-bit base matrices. +For necessity we grant this entire group, a larger alphabet than the actual +affine/phase engine. Sufficiency uses the actual words of `A` and their products/adjoints, already certified free in #4797. No inversion of an arbitrary register operator is a free instruction. This theorem is not about arbitrary oblique representatives, @@ -187,9 +188,28 @@ python3 scripts/research_package.py --package research/resonant-recovery-scalars The primary checker authenticates #4885's executable/source coefficient before loading it, replays its exact integer annihilator, and derives the new quotient and localization certificates. Explicit checks remain active under `-O`. -A separate independent modular witness check is planned for the next -implementation checkpoint; it is not part of this initial certificate. -Finite corroboration will not replace the written all-width proof. +`independent_modular.py` does not import the primary checker or execute the +source checker. It parses only the pinned literal polynomial and target, +uses packed permutation/phase bytes, a separate right-generator group +enumeration, and modular Horner arithmetic modulo `8505=3^5*5*7`. It checks +the full modular annihilator and independently recovers the combined signed +witness residue 2754. Its local valuations are: + +| Prime | Raw numerator valuation | Raw denominator valuation | Surviving denominator valuation | +|---|---:|---:|---:| +| 3 | 4 | 7 | 3 | +| 5 | 0 | 1 | 1 | +| 7 | 0 | 1 | 1 | + +Modulo 243,5,7 the raw numerator residues are 81,4,3, respectively. These +nonzero finite residues prove the stated exact numerator valuations, with +the exact denominator supplied by the pinned polynomial. This independent +finite check corroborates the odd-prime witness; it does not replace the +primary unbounded-integer certificate or the written all-even proof. +It also rejects omission of a negative-word representative, a changed +polynomial constant, a collapsed quarter phase at literal width two, and an +incorrect monomial inverse. The primary checker has six additional ring, +quotient and inverse-polynomial controls. | Obligation | Status | |---|---| @@ -206,7 +226,9 @@ The original retained owners and complements of #4797 are unchanged. This coefficient-ring obstruction gives no universal lower bound for native restoration and excludes no approximate, oblique or width-dependent decoder. The exact source replay and independent finite checks are not human or -proof-kernel acceptance. No selected-frontier or frozen predecessor is changed. +proof-kernel acceptance. A separate read-only agent reviewed the proof and +both implementations and independently ran optimized checks without finding +a blocker. No selected-frontier or frozen predecessor is changed. ## Provenance and overlap diff --git a/research/resonant-recovery-scalars/TASK.json b/research/resonant-recovery-scalars/TASK.json index c3f65bce5a..ef03abbdf0 100644 --- a/research/resonant-recovery-scalars/TASK.json +++ b/research/resonant-recovery-scalars/TASK.json @@ -51,10 +51,10 @@ "bottleneck_link": "Separates the exact Gaussian-dyadic linear decoder contract from rational orthogonal recovery, identifying genuinely required scalar services without assigning their physical runtime zero.", "budget_minutes": 60, "stop_rule": "At most45 minutes for the quantified coefficient-ring theorem and exact/independent finite certificates, with15 minutes reserved for review and committed Git-free replay. Stop if the denominators disappear after the correct even phase quotient or merely restate the source inverse.", - "outcome": "partial", - "evidence": "README proves the finite-support all-even tensor faithfulness and sharp localization theorem. verify.py derives the exact even projector LCD and witness, and separately verifies the actual sufficient decoder polynomial.", + "outcome": "completed", + "evidence": "README proves the finite-support all-even tensor faithfulness and sharp localization theorem. verify.py derives the exact even projector LCD and witness, and separately verifies the actual sufficient decoder polynomial. Independent packed-monomial modular Horner arithmetic certifies the three odd-prime valuations and four semantic controls without importing either mathematical checker.", "author": "JoyboyBrian", - "ai_assistance": "Substantial OpenAI Codex assistance for proof, exact implementation and source review; no independent human or proof-kernel acceptance claimed.", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, exact implementation, source review and a separate read-only agent proof/code review. No independent human or proof-kernel acceptance claimed.", "open_questions": [ { "question": "Can a uniform oblique accessible-coordinate decoder avoid odd scalar services?", diff --git a/research/resonant-recovery-scalars/VERIFY.json b/research/resonant-recovery-scalars/VERIFY.json index af2edf11d5..29624c0523 100644 --- a/research/resonant-recovery-scalars/VERIFY.json +++ b/research/resonant-recovery-scalars/VERIFY.json @@ -28,6 +28,27 @@ ], "timeout_seconds": 45, "checks": "Same explicit exact checks under optimized Python." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent_modular.py" + ], + "timeout_seconds": 45, + "checks": "Independent packed-monomial/right-BFS modular annihilator and exact odd-prime valuations, plus four semantic failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent_modular.py" + ], + "timeout_seconds": 45, + "checks": "Same independently implemented modular checks with assertions disabled." } ] } diff --git a/research/resonant-recovery-scalars/independent_modular.py b/research/resonant-recovery-scalars/independent_modular.py new file mode 100644 index 0000000000..d5058928b7 --- /dev/null +++ b/research/resonant-recovery-scalars/independent_modular.py @@ -0,0 +1,208 @@ +#!/usr/bin/env python3 +"""Independent packed-monomial modular check of the odd denominator witness. + +Does not import the primary checker or execute the predecessor's code. +The exact proof remains in README.md and the primary integer certificate. +""" +import argparse +import ast +from fractions import Fraction +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +INPUT = HERE.parent / 'resonant-all-width-projector' +PINS = {'verify.py': '29554fca57ad1b91469cbd65543882ebdaf8cafa93b8dc2ff37b00baef03e930', + 'TARGET.json': 'e7df852b5c641f326ac67cd35cea8da6cfdd059fa12df1cf6fb758bb4206d684'} +IDENTITY = bytes(list(range(8)) + [0] * 8) +MINUS = bytes(list(range(8)) + [2] * 8) +WITNESS = bytes([0, 1, 3, 2, 4, 5, 7, 6, 0, 0, 1, 3, 0, 0, 3, 1]) +MODULUS = 3 ** 5 * 5 * 7 + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def compose(first, second): + """Packed permutation/phase composition, applying second first.""" + out = bytearray(16) + for column in range(8): + middle = second[column] + out[column] = first[middle] + out[8 + column] = (second[8 + column] + first[8 + middle]) & 3 + return bytes(out) + + +def inverse(word): + out = bytearray(16) + for column in range(8): + row = word[column] + out[row] = column + out[8 + row] = (-word[8 + column]) & 3 + return bytes(out) + + +def inputs(): + raw = {} + for name, pin in PINS.items(): + data = (INPUT / name).read_bytes() + require(hashlib.sha256(data).hexdigest() == pin, 'independent input hash: ' + name) + raw[name] = data + polynomial = None + for node in ast.parse(raw['verify.py']).body: + if isinstance(node, ast.Assign) and any(isinstance(t, ast.Name) and t.id == 'POLY' for t in node.targets): + polynomial = ast.literal_eval(node.value) + require(polynomial is not None and len(polynomial) == 19, 'literal polynomial') + records = json.loads(raw['TARGET.json']) + A = {} + for record in records: + p, phase = record['permutation'], record['phase_i'] + coefficient = Fraction(record['coefficient']) * 16 + require(sorted(p) == list(range(8)) and len(phase) == 8 and all(0 <= x < 4 for x in phase), 'literal monomial') + require(coefficient in (-1, 1), 'literal coefficient') + word = bytes(p + phase) + require(word not in A, 'duplicate target term') + A[word] = int(coefficient) + require(len(A) == 256, 'target support') + return polynomial, A + + +def factors(A): + generators = [MINUS, bytes([j ^ 1 for j in range(8)] + [1] * 8)] + generators += [bytes(list(range(8)) + [2 * ((j >> bit) & 1) for j in range(8)]) for bit in range(3)] + subgroup = {IDENTITY} + for g in generators: + subgroup.update([compose(g, h) for h in tuple(subgroup)]) + require(len(subgroup) == 32, 'output subgroup') + require(all({compose(g, h) for h in subgroup} == subgroup for g in generators), + 'literal subgroup closure') + remaining = set(A) + representatives = [] + while remaining: + word = min(remaining) + orbit = {compose(h, word) for h in subgroup} + require(orbit <= remaining and all(A[h] == A[word] for h in orbit), 'signed left-coset factorization') + representatives.append((word, A[word])) + remaining.difference_update(orbit) + require(len(representatives) == 8, 'eight signed cosets') + r0 = representatives[0][0] + ri = inverse(r0) + b = [(compose(ri, word), sign) for word, sign in representatives] + d = [compose(compose(ri, word), r0) for word in generators] + return b, d + + +def action(b, d): + letters = list(dict.fromkeys([g for g, _ in b] + d + [inverse(g) for g, _ in b])) + # Right-generator enumeration is independent of the source's left BFS. + group = [IDENTITY] + positions = {IDENTITY: 0} + for word in group: + for generator in letters: + next_word = compose(word, generator) + if next_word not in positions: + positions[next_word] = len(group) + group.append(next_word) + require(len(group) <= 21504, 'group bound') + require(len(group) == 21504, 'group cardinality') + tables = {g: [positions[compose(g, word)] for word in group] for g in letters} + n = len(group) + + def sum_translates(vector, weighted): + output = [0] * n + for word, sign in weighted: + table = tables[word] + for index, value in enumerate(vector): + output[table[index]] += sign * value + return [value % MODULUS for value in output] + + def apply_H(vector): + current = sum_translates(vector, b) + for g in reversed(d): + table = tables[g] + changed = current[:] + for index, value in enumerate(current): + changed[table[index]] += value + current = [value % MODULUS for value in changed] + current = sum_translates(current, [(inverse(g), sign) for g, sign in b]) + return [(value * ((MODULUS + 1) // 2)) % MODULUS for value in current] + + return group, positions, apply_H + + +def valuation(number, prime): + require(number != 0, 'valuation of nonzero residue') + count = 0 + while number % prime == 0: + number //= prime + count += 1 + return count + + +def verify(): + polynomial, A = inputs() + b, d = factors(A) + group, positions, apply_H = action(b, d) + q = polynomial[1:] + vector = [0] * len(group) + vector[positions[IDENTITY]] = 1 + for k in range(16, -1, -1): + vector = apply_H(vector) + vector[positions[IDENTITY]] = (vector[positions[IDENTITY]] + q[k] * pow(64, 17-k, MODULUS)) % MODULUS + require(not any(apply_H(vector)), 'independent modular annihilator') + negative = compose(MINUS, WITNESS) + value = (-vector[positions[WITNESS]] - vector[positions[negative]]) % MODULUS + denominator = q[0] * 64 ** 17 + expected_numerator = Fraction(1243, 3870720) * denominator + require(expected_numerator.denominator == 1, 'integer raw witness numerator') + require(value == expected_numerator.numerator % MODULUS, 'independent even witness residue') + valuation_receipt = [] + for prime, exponent in ((3, 5), (5, 1), (7, 1)): + residue = value % prime ** exponent + nv = valuation(residue, prime) + dv = valuation(abs(denominator), prime) + require(nv < exponent and dv - nv == (3 if prime == 3 else 1), 'odd-prime denominator valuation') + valuation_receipt.append({'prime': prime, 'modulus': prime ** exponent, 'raw_numerator_residue': residue, + 'numerator_valuation': nv, 'denominator_valuation': dv, + 'reduced_denominator_valuation': dv-nv}) + controls = [] + require((-vector[positions[WITNESS]]) % MODULUS != value, 'negative representative omission') + controls.append('omit_negative_word') + changed = vector[:] + changed[positions[IDENTITY]] = (changed[positions[IDENTITY]] + pow(64, 17, MODULUS)) % MODULUS + require(any(apply_H(changed)), 'constant polynomial mutation') + controls.append('constant_polynomial_mutation') + quarter = bytes(list(range(8)) + [1] * 8) + require(compose(quarter, quarter) == MINUS and MINUS != IDENTITY, 'quarter-phase square') + # At f=2 the actual central quarter phase acts as -1, not +1. + require((quarter[8] + quarter[8]) % 4 == 2, 'literal width-two central phase') + controls.append('quarter_phase_collapse_at_width_two') + orientation_word = next(g for g in A if inverse(g) != g and g[:8] != IDENTITY[:8]) + require(compose(inverse(orientation_word), orientation_word) == IDENTITY + and compose(orientation_word, orientation_word) != IDENTITY, + 'orientation-sensitive monomial inverse') + controls.append('inverse_orientation') + return {'status': 'PASS_INDEPENDENT_RESONANT_SCALARS', 'source_pins': PINS, + 'group_size': len(group), 'modulus': MODULUS, 'even_witness_raw_residue': value, + 'odd_prime_valuations': valuation_receipt, 'negative_controls': controls, + 'scope': 'Independent finite modular corroboration of the exact source projector coefficient; not a replacement for exact integer or all-even faithfulness proofs.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', action='store_true') + args = parser.parse_args() + result = verify() + path = HERE / 'INDEPENDENT.json' + if args.write: + path.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + require(json.loads(path.read_text()) == result, 'independent receipt') + print(result['status']) + + +if __name__ == '__main__': + main()