From 9360ba7312cf8961e672e9eb26c612719028d39d Mon Sep 17 00:00:00 2001 From: ross Date: Fri, 16 Oct 2026 21:52:11 +1100 Subject: [PATCH] Prove fixed-cut rank-seven helper408 obstruction --- .../helper408-rank7-pairing/.gitattributes | 1 + research/helper408-rank7-pairing/BOUNDARY.md | 255 +++++ .../helper408-rank7-pairing/INDEPENDENT.md | 264 +++++ research/helper408-rank7-pairing/NOTICE.md | 7 + research/helper408-rank7-pairing/README.md | 155 +++ .../helper408-rank7-pairing/SOURCE-PINS.json | 71 ++ research/helper408-rank7-pairing/SOURCES.json | 18 + research/helper408-rank7-pairing/TASK.json | 90 ++ research/helper408-rank7-pairing/VERIFY.json | 39 + .../helper408-rank7-pairing/check_budget.py | 169 ++++ .../check_independent.py | 471 +++++++++ .../evidence/BOUNDARY.json | 925 ++++++++++++++++++ .../evidence/BUDGET.json | 134 +++ .../evidence/INDEPENDENT.json | 744 ++++++++++++++ .../evidence/VALIDATION.json | 41 + .../sources/CONSTRUCTION.md | 86 ++ .../sources/CREDITS.md | 39 + .../helper408-rank7-pairing/sources/PINS.json | 52 + .../sources/SOURCES.json | 18 + .../sources/allocation/FILL.json.gz | Bin 0 -> 1298679 bytes .../sources/allocation/ORDER.json | 1 + .../sources/allocation/PROFILE.json | 1 + .../sources/allocation/PROVIDERS.json | 1 + .../sources/allocation/RESULT.json | 1 + .../sources/allocation/baseline/PROFILE.json | 1 + .../allocation/vendor/TEMPLATE.json.gz | Bin 0 -> 1124331 bytes .../sources/data/PARENT-base.json.gz | Bin 0 -> 70383 bytes .../sources/data/PARENT-extra.json.gz | Bin 0 -> 70381 bytes .../sources/data/TRANSFORM.json | 271 +++++ .../sources/data/WORD-base.json.gz | Bin 0 -> 69992 bytes .../sources/data/WORD-extra.json.gz | Bin 0 -> 69989 bytes .../verify_boundary.py | 411 ++++++++ 32 files changed, 4266 insertions(+) create mode 100644 research/helper408-rank7-pairing/.gitattributes create mode 100644 research/helper408-rank7-pairing/BOUNDARY.md create mode 100644 research/helper408-rank7-pairing/INDEPENDENT.md create mode 100644 research/helper408-rank7-pairing/NOTICE.md create mode 100644 research/helper408-rank7-pairing/README.md create mode 100644 research/helper408-rank7-pairing/SOURCE-PINS.json create mode 100644 research/helper408-rank7-pairing/SOURCES.json create mode 100644 research/helper408-rank7-pairing/TASK.json create mode 100644 research/helper408-rank7-pairing/VERIFY.json create mode 100644 research/helper408-rank7-pairing/check_budget.py create mode 100644 research/helper408-rank7-pairing/check_independent.py create mode 100644 research/helper408-rank7-pairing/evidence/BOUNDARY.json create mode 100644 research/helper408-rank7-pairing/evidence/BUDGET.json create mode 100644 research/helper408-rank7-pairing/evidence/INDEPENDENT.json create mode 100644 research/helper408-rank7-pairing/evidence/VALIDATION.json create mode 100644 research/helper408-rank7-pairing/sources/CONSTRUCTION.md create mode 100644 research/helper408-rank7-pairing/sources/CREDITS.md create mode 100644 research/helper408-rank7-pairing/sources/PINS.json create mode 100644 research/helper408-rank7-pairing/sources/SOURCES.json create mode 100644 research/helper408-rank7-pairing/sources/allocation/FILL.json.gz create mode 100644 research/helper408-rank7-pairing/sources/allocation/ORDER.json create mode 100644 research/helper408-rank7-pairing/sources/allocation/PROFILE.json create mode 100644 research/helper408-rank7-pairing/sources/allocation/PROVIDERS.json create mode 100644 research/helper408-rank7-pairing/sources/allocation/RESULT.json create mode 100644 research/helper408-rank7-pairing/sources/allocation/baseline/PROFILE.json create mode 100644 research/helper408-rank7-pairing/sources/allocation/vendor/TEMPLATE.json.gz create mode 100644 research/helper408-rank7-pairing/sources/data/PARENT-base.json.gz create mode 100644 research/helper408-rank7-pairing/sources/data/PARENT-extra.json.gz create mode 100644 research/helper408-rank7-pairing/sources/data/TRANSFORM.json create mode 100644 research/helper408-rank7-pairing/sources/data/WORD-base.json.gz create mode 100644 research/helper408-rank7-pairing/sources/data/WORD-extra.json.gz create mode 100644 research/helper408-rank7-pairing/verify_boundary.py diff --git a/research/helper408-rank7-pairing/.gitattributes b/research/helper408-rank7-pairing/.gitattributes new file mode 100644 index 0000000000..fa1385d99a --- /dev/null +++ b/research/helper408-rank7-pairing/.gitattributes @@ -0,0 +1 @@ +* -text diff --git a/research/helper408-rank7-pairing/BOUNDARY.md b/research/helper408-rank7-pairing/BOUNDARY.md new file mode 100644 index 0000000000..fd7de6b25b --- /dev/null +++ b/research/helper408-rank7-pairing/BOUNDARY.md @@ -0,0 +1,255 @@ +# A diagonal obstruction to rank-seven helper408 extraction + +For the two pinned PR2894 providers carried by PR2908, helper408 cannot be +isolated and restored at its original rank-seven last frame by the proposed +scalar input/output basis changes. This remains impossible when protected +terminal helpers are generously made available. The decisive certificate is an +11 by 11 diagonal forbidden-input minor with determinant `-1/4`. + +This is a fixed-word, fixed-entrance, fixed-terminal-support obstruction. It +does not exclude a changed middle word, changed source access, additional +intermediate operations, or a different endpoint. There is no new supplier and +no new kappa claim. + +## Exact premises + +The source scientific pins are PR2908 head +`51309592971e3b5be935599eed2a95404dc7781e`, containing the PR2894 providers at +`18d03c447886895ef9abf888398178e0428533ca`. The shared research base is +`475fec190d5ad746bd4690574dca30d6901acdaf`. Source bytes, provenance and their +independent integrity gate are recorded by the surrounding package. + +| Provider | SHA256 of compressed source bytes | +| --- | --- | +| `PARENT-base.json.gz` | `c20a470aec0f3e61833cb41fe190639eb358f58017143d2336c55c80fba265eb` | +| `PARENT-extra.json.gz` | `db34e39876241087b581ed9374c53e9cd393e3e86ef6103bfb54f3077c3d2761` | + +Work over the dyadic ring `Z[1/2]`, enlarged to `Q` for the complete linear +space computation. Every live data/helper input is arbitrary and independent; +no helper is assumed initially zero. A zero entrance *frame* does not mean a +zero value. The non-target coordinates are + +``` +L = {0,...,703} \ (removed union {112,...,223}), |L| = 520. +``` + +`M` is the complete non-target middle operator: `A[prelude_events:]`, followed +chronologically by `B` and all its inserted warps, followed by `restore`, +omitting exactly the target writes. Each warp is its own invertible formal +generator, multiplied on the left. Only adjacent inverse cancellation is +allowed. No source auditor or source `structure.py` is imported. The exact +replay uses 4,583 gates and produces 11,912 nonzero free-word terms. + +Let `P` be the union of `helper_final`, `start_extra`, and initial-correction +source registers. The allowed input coordinates are + +``` +H = {r in L : r >= 224 and r not in P}, |H| = 226. +``` + +Input basis changes `S` are arbitrary invertible scalar changes inside `H`, +extended by the identity elsewhere. In particular, existing 72 cold helper +entrances, nonzero entrance frames, and operator-correction sources stay +protected. The checker also verifies that no prelude warp lender lies in `H`. + +The proposed helper408 entrance/terminal pair is + +``` +(empty, E7), E7 = span_GF(2)(256,128,66,36,22,8,1). +``` + +If a supplier existed, its physical residual would be the paired operator +`T_native(E7) T_native(empty)^-1`. No native factorization or phase identity +for this residual is assumed or certified here. The symbol `T` below denotes +the proposed *scalar output basis change*, not this native residual. + +## Deriving the terminal support + +Replay the entire literal frame chain, including all `A` incidents, target +writes' source incidents, the 24 prelude warps, all 72 `B` warps, and the +`restore` incidents. Scalar incidents must be monotone; a warp checks its +recorded incoming frame and replaces it by its recorded outgoing frame. A +union of all historical frames would be incorrect across these resets. +The replay covers 10,456 scalar register incidents. + +Let `F_r` be the frame after `restore` and before the prescribed final climbs. +Every register available to an appended scalar gate at `E7` must satisfy +`F_r <= E7`. Thus the maximal relaxed non-target support is + +``` +R = (105,307,309,314,369,371,373,378,408,572,573). +``` + +The following are the derived last frames; the list is complete. + +| Registers | Last frame basis | +| --- | --- | +| 105, 408, 572, 573 | `(256,128,66,36,22,8,1)` | +| 307, 309, 314 | `(385,74,44,30)` | +| 369, 371, 373, 378 | `(392,67,37,22)` | + +The nine registers in `R \ {105,408}` are existing cold helpers. Allowing +arbitrary terminal mixing on them relaxes the requirement that those existing +extractions survive. A negative result for this larger `R` therefore also +applies with the original cold-helper protection enforced. Ordinary data +register105 is likewise allowed. Target registers are excluded throughout. + +## Necessary paired identities + +Write the desired isolated helper as `h=408`. If scalar changes `S,T` produce +both an identity column and identity row on that helper, define + +``` +v = S e_h, alpha = e_h^T T, +y = M v, u = alpha M. +``` + +Then `v,u` are scalar supported on `H`, `y,alpha` are scalar supported on `R`, +and `alpha y = u v = 1`. Indeed, the row identity +`e_h^T T M S = e_h^T` already gives +`alpha M = e_h^T S^-1`, which is supported on `H` and nonzero. + +The complete rational spaces checked here are + +``` +V = {v in Q^H : Mv is scalar and supported on R}, +A = {alpha in Q^R : alpha M is scalar and supported on H}. +``` + +They have dimensions zero and zero in both source variants. The forward +system has 608 nonzero coefficient equations and rank226; the dual system has +17 nonzero coefficient equations and rank11. Consequently the full pairing +matrix on their bases is empty and zero. This is exact rational elimination, +not a random or modular rank estimate. + +## Small certificate: every terminal readout vanishes + +The full space computation is corroborating evidence. The following minor +alone proves the obstruction. In the order of `R` above, take the forbidden +input columns + +``` +J = (14,307,309,314,369,371,373,378,41,572,573). +``` + +Every member of `J` is outside `H`: 14 and 41 are data inputs and the others +are protected cold helpers. Exact free-word replay gives + +``` +M[R,J] = diag(-1/2,1,1,1,1,1,1,1,1/2,1,1), +det M[R,J] = -1/4. +``` + +All off-diagonal polynomials are zero, and all diagonal polynomials are the +displayed scalars with no nonempty operator words. Thus, for a readout +`alpha` supported on `R`, the requirement that `alpha M` be supported on `H` +forces + +``` +-alpha_105/2 = 0, alpha_408/2 = 0, +alpha_r = 0 for r = 307,309,314,369,371,373,378,572,573. +``` + +Hence `alpha=0`, contradicting the required unit pairing or merely the +nonzero row identity. The determinant is a unit in `Z[1/2]`; no odd-denominator +normalization is used. The obstruction remains valid over `Q` and for every +representation of the frozen free-operator word on a dyadic module. Because +the minor is already a scalar identity, this conclusion does not depend on +distinct nonempty free words remaining independent after specialization. + +The two source files were independently loaded and replayed. Their complete +non-target middle operators compare equal, with canonical term-list SHA256 +`d1c29a23fbe07da932c44d9e9b1467ab866894faac115d456eae8e42069aec68` under the +encoding in `operator_digest`. Neither equality nor one variant's result is +assumed when checking the other. + +## Positive calibration and invalid controls + +The existing PR2908 rank-eight `E52=(256,128,64,36,20,8,2,1)` certificate is +reconstructed from its 24 input gates and three output gates. The checker +derives `S,T,v,u,alpha,y` and verifies all seven displayed identities: + +``` +S e408 = v, u S = e408^T, M v = y, +alpha M = u, alpha y = 1, T y = e408, +e408^T T = alpha. +``` + +In particular it obtains `y=2 e42` and +`alpha=e408^T+(1/2)e42^T+e105^T`, with unit pairing. Its explicit `v,u` are +included in the checker output. Register42 has last frame `E52`, so it is +unavailable at `E7`. This explains a concrete capability lost by the proposed +smaller endpoint. + +The following changed candidates are each rejected for an actual failed +equation or support requirement in both variants: + +| Changed candidate | Failed obligation | +| --- | --- | +| Change known `v_226` from `1/2` to `1` | `Mv` scalar/support requirement at E52 | +| Change known `alpha_42` from `1/2` to `1` | `alpha M` scalar/support requirement on H | +| Claim the unchanged known E52 pair at E7 | Terminal readout support: register42 is outside R | + +These are algebraic or frame mutants of a valid witness. No checksum failure +is counted as a mathematical negative control. + +## Cost consequences and remaining boundaries + +There is no changed word and therefore no realized local cost change. The +proposed saving fails before target-compensation changes, native lowering, +cleanup regeneration, owner assignment or recursive admission can be +constructed. None of those obligations may be waived by this obstruction. + +For the favorable screen declared before computation, an ideal extraction +would remove helper408's rank-two terminal climb from the PR2894 profile, +change its width9 to width7, and require a 73rd private zero buffer. Relative +to PR2908's actual rank-eight extraction, which already pays that buffer and +has local delta `+3 H1 - 2 H2` from PR2894, the optimistic local child-count +delta would be `-3 H1 + H2` per supplier call. There are 666 calls; every +other local child, all eight center H8 children, every bridge and every owner +residue remain charged. If `k_b` copies of helper408 are present in owner bin +`b`, shrinking each width8 to width7 changes its idle rank from `r_b` to +`r_b+k_b`, not necessarily only by one. The favorable raw moment delta is + +``` +666 * (-3 * 1^p + 2^p) + sum_b ((r_b+k_b)^p - r_b^p), 0 < p < 1, +sum_b k_b = 666. +``` + +This is only the unrealizable favorable budget being screened, with added +terminal climbs, scalar compensation, inverse cleanup, native conversion, +routing, precision and stock changes still owed. The parent package owns the +literal owner-bin verification and full cost ledger. Physical families would +be `66304+408+8+73+2=66795` if no further scratch were needed; this count does +not certify a new supplier. No native phase, chronological owner realization, +all-size recurrence, precision, machine or outer theorem follows here. + +This finite exact computation has a short written linear-algebra implication +for arbitrary dirty inputs and arbitrary allowed scalar basis changes. It is +not a formal-kernel proof and is not a classification of other words or +endpoints. In particular, a source-partner recovery that changes `H`, a +changed middle `M`, or altered incident frames would invalidate one of the +explicit premises and would require its own proof and full invoice. + +## Reproduction and credit + +From the repository root, using only Python's standard library: + +```sh +python3 -I -O -B research/helper408-rank7-pairing/verify_boundary.py +``` + +Expected terminal status: `PASS_SCOPED_RANK7_OBSTRUCTION`. The checker also +prints the complete support sets, dimensions, diagonal certificate, source +digests, positive calibration and the three rejected mutants for each +provider. Its source hashes authenticate the input bytes; its exact checks use +explicit exceptions and remain active with Python optimization enabled. + +The paired boundary construction and E52 calibration are credited to Jeremy +Diviney (PR2908). The input providers and chronological frame conventions are +credited to Jeremy Kothe (PR2894 and PR2833), with the retained Yiyang Lu +(PR2857), Dugongue (PR2863), Marius-Paul Dumitrean (PR2843/2802), Philippe Van +Velzen (PR2853), Tekalign and exact/native lineage credits in the surrounding +package. This new scoped obstruction and independent standard-library checker +were prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. diff --git a/research/helper408-rank7-pairing/INDEPENDENT.md b/research/helper408-rank7-pairing/INDEPENDENT.md new file mode 100644 index 0000000000..ecf922c35a --- /dev/null +++ b/research/helper408-rank7-pairing/INDEPENDENT.md @@ -0,0 +1,264 @@ +# Independent inverse-column and chronological row certificates + +The proposed rank-seven replacement of PR2908's first paired extraction is +impossible with its pinned PR2894 middle word and the declared protected +entrances. Both admissible terminal spaces are zero, independently in the +`base` and `extra` providers. Two small exact restrictions prove this without +depending on the full nullspace calculation. + +This check was derived before reading `verify_boundary.py` or `BOUNDARY.md`. +It imports neither file, nor any predecessor Python module. After obtaining +the result, the primary proof was cross-read: its forward forbidden-input +minor agrees with the independent chronological row calculation below. + +## Fixed domain and actual cut + +The scientific sources are Jeremy Diviney's PR2908 at +`51309592971e3b5be935599eed2a95404dc7781e`, carrying Jeremy Kothe's PR2894 +providers at `18d03c447886895ef9abf888398178e0428533ca`. Each direct replay checks +both SHA256 and Git-blob identities for all five used data files against +`SOURCE-PINS.json`; these two commit identifiers are also fixed in the checker. + +All non-target input values are arbitrary. The scalar coefficient domain is +`Q`, which contains the proposed dyadic domain. Warps are independent invertible +noncommuting operators; only adjacent inverse symbols cancel. The map `M` +contains the 4,583 chronological non-target gates from `A[84:]`, `B` with its +72 numbered warps inserted at their recorded positions, and `restore`. +Targets 112 through 223 are omitted. A target-to-non-target source edge would +invalidate that reduction and is explicitly rejected. + +The eligible input set `H` contains 226 helpers. It excludes all removed +registers, all 72 existing `helper_final` registers, every `start_extra` +register and every source of the initial operator corrections. Input changes +`S` must act inside `H` and be the identity elsewhere. Zero entrance frame +does not mean a zero initial value. + +At the actual cut after `restore`, before final climbs, the complete relaxed +terminal support at + +``` +E7 = span_GF(2)(256,128,66,36,22,8,1) +``` + +is, in this order, + +``` +R = (105,307,309,314,369,371,373,378,408,572,573). +``` + +The last-frame collector includes all incidences of the full `A` word, +including prelude warps and sources of target writes; all `B` gates and warp +resets; and all `restore` gates. Every live register is observed. It also checks +the center frames at the separate target-only cut and all 72 retained cold +helper endpoints. Thus omission of target writes from `M` does not omit their +source incidences from terminal eligibility. The primary checker separately +validates monotonicity at every scalar incidence and both ends of every warp. + +Let + +``` +C = (307,309,314,369,371,373,378,572,573). +``` + +These nine terminal registers are existing cold helpers. The independent +test generously permits them in the terminal support. Preserving them would +only restrict the proposed terminal change `T` further. The data register105 +is also permitted, while targets and removed registers are excluded. + +## The inverse-column restriction is the identity matrix + +For an arbitrary scalar `y` supported on `R`, exact inverse replay gives + +``` +(M^-1 y)_550 = y_408, +(M^-1 y)_551 = y_105, +(M^-1 y)_c = y_c for each c in C. +``` + +These equalities are complete operator-polynomial identities: the displayed +coordinates have no omitted nonempty operator words or other coefficients. +Registers 550 and 551 are protected nonzero-entry `start_extra` helpers, +and every member of `C` is a protected cold helper. All eleven coordinates +are outside `H`. + +Equivalently, in the given order of `R`, set + +``` +Jinv = (551,307,309,314,369,371,373,378,550,572,573). +``` + +Then the exact 11 by 11 restriction is + +``` +(M^-1)[Jinv,R] = I_11. +``` + +Its determinant is one. Therefore `M^-1 y` supported on `H` forces `y=0`. +This already excludes any nonzero extractable column at `E7`. + +## An independent row restriction has determinant -1/4 + +For a scalar covector `alpha` supported on the same `R`, chronological right +multiplication gives + +``` +(alpha M)_14 = -alpha_105/2, +(alpha M)_41 = alpha_408/2, +(alpha M)_c = alpha_c for each c in C. +``` + +Again these are complete operator identities. Data inputs 14 and 41 and +all nine cold inputs are outside `H`. In the order + +``` +Jrow = (14,307,309,314,369,371,373,378,41,572,573) +``` + +the restriction is + +``` +M[R,Jrow] = diag(-1/2,1,1,1,1,1,1,1,1/2,1,1). +``` + +Its determinant is `-1/4`, a unit already over `Z[1/2]`. Hence the scalar +support condition on `alpha M` forces `alpha=0` independently of the column +argument. Because both restrictions are scalar identities, their obstruction +survives every representation of the pinned free-operator word on a dyadic +module; no independence of nonempty words after specialization is needed. + +For clarity about chronology, write `M=G_n ... G_1`. To compute `M^-1 y`, +the checker visits `G_n,...,G_1` and applies each inverse on the left. To +compute `alpha M`, it visits the same reversed chronological list and +multiplies each `G_i` on the right. A shear `d += q s` updates the covector +coordinate `s += q d`; an operator on `d` appends its symbol to the right +of each existing coefficient word. Prepending here would be wrong. + +## Consequence for simultaneous input and terminal changes + +Suppose invertible scalar changes `S` on `H` and `T` on `R` produced both +the helper408 identity row and identity column in `T M S`. Then + +``` +v = S e408, y = T^-1 e408, +alpha = e408^T T, u = e408^T S^-1 +``` + +would satisfy + +``` +M v = y, alpha M = u, alpha y = u v = 1, +v,u supported on H, y,alpha supported on R. +``` + +The inverse-column identity already forces `y=0`, and the row identity +independently forces `alpha=0`; either contradicts the unit pairing. +The full rational calculation confirms dimensions zero and zero, using +11 inverse-column constraints of rank11 and 17 row constraints of rank11. +This covers every allowed rational scalar basis change, hence every allowed +dyadic one. It is not merely a failed candidate search. + +## Existing rank-eight composition and defect-sensitive controls + +The checker reconstructs the existing PR2908 composition from its actual +`WORD-*` providers and `TRANSFORM.json`. Its 24 input gates define `S`, and +its three terminal gates are + +``` +408 += (1/2) * 42 +408 += 105 +42 -= 2 * 408. +``` + +They act at `E8=(256,128,64,36,20,8,2,1)` and give + +``` +y = 2 e42, +alpha = e408^T + (1/2)e42^T + e105^T. +``` + +The replay independently derives `v=S e408` and `u=e408^T S^-1`, then +checks `Mv=y`, `alpha M=u`, `T y=e408`, `u S=e408^T`, and both pairings +equal one. The complete rank-eight terminal spaces have dimensions 7 and 4 +with a nonzero pairing matrix. Terminal register42 has frame `E8` and is +unavailable at `E7`. + +The simultaneous literal recipe is also checked: the new `A` is exactly the +old prelude, followed by the input gates, followed by the old remaining `A`; +new `restore` is old `restore` followed by the terminal gates. `B`, all warps, +prelude length, initial operator corrections, removed helpers and entry data +stay exactly equal. Input gates touch only `H` at frame zero. Terminal gates +touch no existing cold helper, and the old `helper_final` map is preserved +with only the new helper408 endpoint added. + +For every compensation target, the actual new correction map equals `C S`. +The incorrect `C S^-1` map differs and is rejected. This matters because +the correction observes the transformed raw input, rather than undoing `S`. + +Both literal cleanup lists are independently rebuilt by reversing the entire +changed non-target word and inverting every gate. The cold-helper host map is +`r -> r+704`, and all cleanup gates use the complete rank-nine frame. The +parent has 4,583 cleanup gates and 72 private buffers; the existing rank-eight +composition has 4,610 cleanup gates and 73 private buffers. This checks the +literal inverse recipe; the inherited native allocation and initialization of +those buffers are not re-proved here. + +The following controls are required to distinguish actual semantic defects: + +| Changed object | Observed consequence | +| --- | --- | +| Admit register42 into the rank-seven terminal support | A one-dimensional column and row pair appears with nonzero pairing | +| Replace `C S` by `C S^-1` | Actual target compensation differs | +| Omit the inverse of the final terminal gate | `M v = y` fails | +| Use forward chronology for the row pullback | `alpha M = u` fails | +| Add a target112-to-helper408 gate | Non-target reduction explicitly rejects the new dependency | + +The operator implementation also distinguishes the words `(1,2)` and `(2,1)` +and checks left and right adjacent inverse cancellation. All mathematical and +integrity checks use explicit exceptions and remain active under Python `-O`. + +## Scope, costs and next obligations + +There is no new word and no paid saving: the proposed endpoint fails its +necessary algebraic interface before a cost improvement can be realized. +The declared favorable recursive screen, full owner-bin multiplicities, +unchanged centers and bridges, helper stock, and remaining scalar costs are +accounted for in the parent package. The above rank-eight gate and buffer +counts validate the predecessor composition only; they are not a newly +improved profile. + +This is exact finite symbolic replay plus a written implication for arbitrary +dirty input values and all scalar changes within the fixed support class. It +is not a formal-kernel proof, an all-size supplier theorem, or a restriction +on changed middles or alternative endpoints. Native phases, compensation +lowering, physical owner realization, full recursive moments, precision and +outer assembly would all remain necessary for any changed construction. + +An eligible next mechanism must change a premise that the witnesses use: +for example, paid recovery that changes the admissible entrances550/551, +the middle word, or the terminal incidence at register42. Such a change +requires a new combined word and a complete invoice. No such construction +or search is included here. + +## Reproduction, independence and credit + +From the repository root: + +```sh +python3 -I -O -B research/helper408-rank7-pairing/check_independent.py +``` + +The exact stdout JSON ends with status +`PASS_INDEPENDENT_RANK7_PAIRING no_new_kappa`; it includes each provider's +support set, dimensions, two small restrictions, rank-eight bases, source +hashes, cleanup counts and control outcomes. It can be redirected to a +receipt without changing the computation. Only the standard library is used. + +The new contribution is the independently derived inverse-column certificate, +its independent row counterpart and the composition-sensitive calibration. +The paired extraction mechanism, its actual 24+3-gate word, and the rank-eight +positive result belong to Jeremy Diviney (PR2908). The retained provider word +and earlier staged composition belong to Jeremy Kothe (PR2894/2833), with the +Yiyang Lu, Dugongue, Marius-Paul Dumitrean, Philippe Van Velzen, Tekalign and +exact/native lineage credit retained in `NOTICE.md` and the pinned sources. +Prepared for Ross Richardson with substantial OpenAI Codex assistance. +Apache-2.0. diff --git a/research/helper408-rank7-pairing/NOTICE.md b/research/helper408-rank7-pairing/NOTICE.md new file mode 100644 index 0000000000..ec74fb826b --- /dev/null +++ b/research/helper408-rank7-pairing/NOTICE.md @@ -0,0 +1,7 @@ +# Attribution and scope + +Prepared for Ross Richardson with substantial OpenAI Codex GPT-6 Astra assistance, including two separately assigned mathematical specialists. No independent human or formal-kernel review is claimed. Apache-2.0, under the repository LICENSE. + +Jeremy Diviney supplied PR2908 (51309592971e3b5be935599eed2a95404dc7781e), its first paired helper408 extraction, exact source words and actual T74 allocation. Jeremy Kothe supplied PR2894 (18d03c447886895ef9abf888398178e0428533ca), the parent word and preload changes. Yiyang Lu/PR2857, Dugongue/PR2863, Marius-Paul Dumitrean/PR2843/2802, Philippe Van Velzen/PR2853, Tekalign and the retained exact/native authors retain their separate contributions; the copied sources/CREDITS.md records the full lineage. PR2904's fixed-gate screen is a scoped predecessor, not this terminal-basis test. + +The supplied word and allocation data and documents are copied byte-for-byte from PR2908 with SHA-256 and Git blob IDs in SOURCE-PINS.json. No predecessor executable is imported. The new exact checkers and written minor obstruction test a different rank-seven endpoint; they do not recertify PR2908's full native/outer release, establish a new kappa, or admit any multiplication theorem. The rank-eight source is a positive control. diff --git a/research/helper408-rank7-pairing/README.md b/research/helper408-rank7-pairing/README.md new file mode 100644 index 0000000000..fa58d69b43 --- /dev/null +++ b/research/helper408-rank7-pairing/README.md @@ -0,0 +1,155 @@ +# Rank-seven helper408 extraction is impossible at the fixed terminal cut + +For both PR2894 parent providers carried by PR2908, arbitrary allowed scalar +input and output basis changes cannot isolate helper408 at its original +rank-seven last frame. Two independent exact implementations produce small +invertible forbidden-input restrictions. The conclusion covers all rational +scalar changes in the declared support class, hence all dyadic ones. It is a +scoped obstruction, with **no new supplier or kappa**. + +The question comes from the paired extraction mechanism in +[Discussion2612](https://github.com/CrocSwap/integer-mult-bounds/discussions/2612) +and [PR2908](https://github.com/CrocSwap/integer-mult-bounds/pull/2908). That +predecessor succeeds at rank eight. This package tests whether its first +helper408 extraction could instead stop at rank seven; the ongoing second +and subsequent rank-eight extraction work is a separate question. + +## Fixed model and decisive witnesses + +Freeze PR2908 at `51309592971e3b5be935599eed2a95404dc7781e`, carrying PR2894 +at `18d03c447886895ef9abf888398178e0428533ca`. All data and helper values are +arbitrary. The map `M` contains the 4,583 non-target gates after the prelude, +including all 72 middle warps. Input scalar changes act only on the 226 +unprotected zero-frame helpers `H`; zero frame does not mean zero value. +Targets, existing cold entrances, nonzero entrances and initial-correction +sources stay protected. + +The complete relaxed terminal support at +`E7=(256,128,66,36,22,8,1)` is + +``` +R = (105,307,309,314,369,371,373,378,408,572,573). +``` + +This generously includes nine existing cold helpers and data register105. +For the forbidden input coordinates + +``` +J = (14,307,309,314,369,371,373,378,41,572,573), +Jinv = (551,307,309,314,369,371,373,378,550,572,573), +``` + +the exact restrictions are + +``` +M[R,J] = diag(-1/2,1,1,1,1,1,1,1,1/2,1,1), +(M^-1)[Jinv,R] = I_11. +``` + +Both `J` and `Jinv` are outside `H`. A scalar row supported on `R` whose +pullback is supported on `H` must therefore vanish. Independently, a scalar +terminal column on `R` whose inverse image is supported on `H` must vanish. +Either conclusion contradicts the unit pairing needed to obtain both an +identity row and column in `T M S`. The scalar minors are units over +`Z[1/2]` and survive every representation of this frozen operator word. + +[BOUNDARY.md](BOUNDARY.md) derives the full frame eligibility, forward +operator and diagonal minor. [INDEPENDENT.md](INDEPENDENT.md) independently +reconstructs inverse columns and chronological row pullbacks. Both find +zero-dimensional rank-seven spaces in both providers. The complete middle +operators have 11,912 terms and identical canonical SHA256 +`d1c29a23fbe07da932c44d9e9b1467ab866894faac115d456eae8e42069aec68`. + +The known rank-eight pair passes both implementations. The independent +checker also verifies the literal input/terminal composition, `C S` target +compensation, and reverse-inverse cleanup recipe with 73 private buffers. +Admitting the unavailable rank-eight register42 restores a nonzero pair. +Coefficient, support, compensation, chronology, cleanup and forbidden target +dependency controls distinguish actual defects from source hash failures. + +## Favorable budget and why the search stops + +The candidate was motivated by removing the original rank-two end climb and +narrowing helper408. Its necessary boundary condition fails, so none of the +following hypothetical saving is realized. Against the actual PR2908 word: + +| Item | Actual rank eight | Ideal rank seven hypothesis | +| --- | --- | --- | +| Local child histogram | `{1:2407,2:640,3:262,4:128,5:26,8:8}` | `{1:2404,2:641,3:262,4:128,5:26,8:8}` | +| Helper408 width | 8 | 7 | +| Private cleanup buffers | 73 | 73 | +| Physical families | 66,795 | 66,795 if no further scratch is needed | + +`check_budget.py` reconstructs the complete actual and hypothetical profiles +from all 271,728 roles in the pinned 666-call T74 fill. It verifies capacity, +non-overlap, complete role coverage, original compact prefixes and the full +published profile. Let `k_b` be the number of helper408 roles sharing owner +bin `b`, and `r_b` its actual idle rank. Compacting within that bin after +shrinking those widths leaves idle rank `r_b+k_b`, not just `r_b+1`. +For `0= 0, "available rank-two climb") + + order = read("allocation/ORDER.json") + replicas = 74 + calls = 9 * replicas + need(len(order) == calls and set(map(tuple, order)) == + {(s, r) for s in range(9) for r in range(replicas)}, "complete calls") + template = read("allocation/vendor/TEMPLATE.json.gz") + need(template["m"] == 73, "supplier dimension") + caps = {} + for child in template["idle_children"]: + c, rank = child["child"], child["rank"] + need(c not in caps or caps[c] == rank, "consistent capacity") + caps[c] = rank + fill = read("allocation/FILL.json.gz") + need(fill["columns"] == ["time", "helper", "owner_replica", "child", "port", "offset"], "fill schema") + seen = set() + masks = defaultdict(int) + shrinks = Counter() + for t, h, owner, child, port, offset in fill["rows"]: + need(0 <= t < calls and 0 <= h < len(helpers), "role bounds") + need((t, h) not in seen, "duplicate role") + seen.add((t, h)) + need(0 <= owner < replicas and child in caps and 0 <= port < 112, "owner bounds") + width = widths[h] + need(0 <= offset and offset + width <= caps[child], "capacity") + key = (owner, child, port) + mask = ((1 << width) - 1) << offset + need(not masks[key] & mask, "overlapping intervals") + masks[key] |= mask + if h == helper_index: + shrinks[key] += 1 + need(len(seen) == calls * len(helpers), "complete role coverage") + need(sum(shrinks.values()) == calls, "one helper408 per call") + + current_idle, ideal_idle, affected = Counter(), Counter(), Counter() + for owner in range(replicas): + for child, cap in caps.items(): + for port in range(112): + key = (owner, child, port) + occupied = masks[key] + used = occupied.bit_count() + need(occupied == (1 << used) - 1, "compact original prefix") + r, k = cap - used, shrinks[key] + need(0 <= used - k <= cap, "hypothetical reduced capacity") + if r: + current_idle[r] += 1 + if r + k: + ideal_idle[r + k] += 1 + if k: + affected[(r, k)] += 1 + current = current_idle.copy() + ideal = ideal_idle.copy() + for r, n in current_local.items(): + current[r] += calls * n + for r, n in ideal_local.items(): + ideal[r] += calls * n + need(current == profile(read("allocation/PROFILE.json")), "complete current profile") + need(mass(current) == mass(ideal) == 65088 * replicas, "complete rank mass") + need(current_local[8] == ideal_local[8] == 8, "all eight centre children retained") + stock = 896 * replicas + 408 + 8 + 73 + 2 + need(stock == 66795, "charged private stock") + + controls = [] + def reject(name, predicate): + try: + predicate() + except ValueError: + controls.append(name) + else: + raise ValueError("control accepted: " + name) + unpaid_idle = current.copy() + unpaid_idle[1] -= 3 * calls + unpaid_idle[2] += calls + reject("omit_new_idle_ranks", lambda: need(mass(unpaid_idle) == mass(current), "rank mass")) + reject("omit_extra_zero_buffer", lambda: need(896 * replicas + 408 + 8 + 72 + 2 == stock, "private stock")) + reject("omit_one_helper408_role", lambda: need(sum(shrinks.values()) - 1 == calls, "role count")) + reject("reuse_rank8_local_profile", lambda: need(mass(current_local) + sum(widths) == + mass(ideal_local) + sum(widths) - 1, "changed local and width balance")) + result = { + "status": "PASS_HYPOTHETICAL_RANK7_BUDGET_NO_SUPPLIER", + "source_commit": pins["source_commit"], "calls": calls, + "roles": len(seen), "helper408_index": helper_index, + "current_local": dict(sorted(current_local.items())), + "ideal_local": dict(sorted(ideal_local.items())), + "current_full_profile": dict(sorted(current.items())), + "ideal_full_profile": dict(sorted(ideal.items())), + "affected_bins_by_old_idle_and_number_of_shrinks": [ + {"old_idle": r, "helper408_roles": k, "bins": n} + for (r, k), n in sorted(affected.items())], + "complete_rank_mass": mass(current), "private_buffers": 73, + "physical_families": stock, "controls": controls, + "comparison": "Delta(p)=666*(-3+2^p)+sum_b((r_b+k_b)^p-r_b^p)<0 for 0