From 6d81d47e6d107e3c52b4583526d31e102b219bdc Mon Sep 17 00:00:00 2001 From: thu-nmrc Date: Sun, 25 Oct 2026 01:37:15 +0800 Subject: [PATCH 1/3] Resolve physical native history spans and bound fixed Z ABI images --- .../physical-zqy-scalar-span/ABI-CLOSURE.json | 32 + .../INDEPENDENT-WIDTH1.json | 957 ++++++++++++++++++ .../INTERNAL-REVIEW.md | 43 + research/physical-zqy-scalar-span/PROOF.md | 225 ++++ research/physical-zqy-scalar-span/README.md | 95 ++ research/physical-zqy-scalar-span/RESULT.json | 81 ++ .../physical-zqy-scalar-span/SOURCES.json | 55 + research/physical-zqy-scalar-span/TASK.json | 96 ++ .../physical-zqy-scalar-span/VALIDATION.md | 49 + research/physical-zqy-scalar-span/VERIFY.json | 90 ++ .../physical-zqy-scalar-span/abi_closure.py | 180 ++++ research/physical-zqy-scalar-span/finite.py | 105 ++ .../independent_width1.py | 171 ++++ research/physical-zqy-scalar-span/monomial.py | 59 ++ research/physical-zqy-scalar-span/native.py | 116 +++ .../physical-zqy-scalar-span/phase_audit.py | 153 +++ research/physical-zqy-scalar-span/rational.py | 17 + research/physical-zqy-scalar-span/verify.py | 81 ++ 18 files changed, 2605 insertions(+) create mode 100644 research/physical-zqy-scalar-span/ABI-CLOSURE.json create mode 100644 research/physical-zqy-scalar-span/INDEPENDENT-WIDTH1.json create mode 100644 research/physical-zqy-scalar-span/INTERNAL-REVIEW.md create mode 100644 research/physical-zqy-scalar-span/PROOF.md create mode 100644 research/physical-zqy-scalar-span/README.md create mode 100644 research/physical-zqy-scalar-span/RESULT.json create mode 100644 research/physical-zqy-scalar-span/SOURCES.json create mode 100644 research/physical-zqy-scalar-span/TASK.json create mode 100644 research/physical-zqy-scalar-span/VALIDATION.md create mode 100644 research/physical-zqy-scalar-span/VERIFY.json create mode 100644 research/physical-zqy-scalar-span/abi_closure.py create mode 100644 research/physical-zqy-scalar-span/finite.py create mode 100644 research/physical-zqy-scalar-span/independent_width1.py create mode 100644 research/physical-zqy-scalar-span/monomial.py create mode 100644 research/physical-zqy-scalar-span/native.py create mode 100644 research/physical-zqy-scalar-span/phase_audit.py create mode 100644 research/physical-zqy-scalar-span/rational.py create mode 100644 research/physical-zqy-scalar-span/verify.py diff --git a/research/physical-zqy-scalar-span/ABI-CLOSURE.json b/research/physical-zqy-scalar-span/ABI-CLOSURE.json new file mode 100644 index 0000000000..c09edf4735 --- /dev/null +++ b/research/physical-zqy-scalar-span/ABI-CLOSURE.json @@ -0,0 +1,32 @@ +{ + "base_exact_non_Y_projection_rank_from_primary": 546, + "base_exact_rank_from_primary": 546, + "base_operator_count": 59, + "base_operator_set_sha256": "34ad3a3f37a53afd59e0d295d6dffa446819539b9ac46556ef51134eb888d831", + "base_rank_obligation": "The registered primary verify.py must pass; this command authenticates/replays the source and consumes its exact 546/546 certificate, rather than rerunning the large exact elimination.", + "coefficient_scope": "arbitrary complex scalar coefficients, allowed to depend on width", + "conclusion": "For every f>=59707 the declared finite left-image span has no nonzero pure-Y vector. Thus it cannot supply the nonzero eight-mode b=ZQY by an exact all-width identity within this fixed family.", + "distinct_left_maps": 1012, + "distinct_left_products": 59708, + "input_sha256": { + "normalizers": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da", + "provider_interface": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65" + }, + "left_map_set_sha256": "e83c2c7f31983321d0f1908d1c1aeb3a9ba1f63cc17106b6089e3cf833c33ccb", + "left_product_set_sha256": "ac702db8dfcf74b29c17686c0899ad1f2b805c50d23ef5e0cee013c57c65e24e", + "left_support_collision_count": 0, + "mode_normalizers": 8, + "new_kappa": false, + "physical_to_logical_left_transport": "F9^-1 T F9 = T, including absolute phase; all seeds centralize the full nine-axis Gaussian and so do their products.", + "port_normalizers": 112, + "product_exact_zero_anchor_checks": 59708, + "provider_full_frame_versions": 4891, + "raw_left_family_size": 1017, + "schema": "physical-zqy-fixed-abi-left-images/v1", + "scope": "Provider-backward whole history; independently chosen left images T in {I,Kp_i,Km_a,Km_a^-1 Kp_i}. No unrestricted products of these generators, no arbitrary monomial left closure, no changed producer or extra correlated data; no small-width nonmembership claim.", + "seed_exact_F9_signed_kernel_address_checks": 61440, + "seed_normalizer_inverse_additions": 0, + "status": "PASS_FIXED_Z_ABI_LEFT_IMAGES_EVENTUAL_WIDTH_NO_NEW_KAPPA", + "target_or_paid_profile_change": false, + "tensor_independence_degree_bound": 59707 +} diff --git a/research/physical-zqy-scalar-span/INDEPENDENT-WIDTH1.json b/research/physical-zqy-scalar-span/INDEPENDENT-WIDTH1.json new file mode 100644 index 0000000000..6a7b601301 --- /dev/null +++ b/research/physical-zqy-scalar-span/INDEPENDENT-WIDTH1.json @@ -0,0 +1,957 @@ +{ + "arithmetic": "Exact Fraction arithmetic; no finite-field rank or nonmembership shortcut. A checked coordinate phase gauge proves the Q(i) physical-operator rank using rational row elimination.", + "checks": [ + { + "all_scalar_coefficients_after_operator_quotient_real_rational": true, + "exact_non_Y_projection_rank_over_Q_i": 546, + "exact_pure_Y_any_physical_operator_dimension": 0, + "exact_rank_V_over_Q_i": 546, + "full_frame_versions": 4891, + "max_basis_denominator_bits": 5, + "max_basis_numerator_bits": 6, + "name": "provider-backward", + "positive_pure_Y_identity_injection": { + "pure_Y_dimension_after_injection": 1, + "rank_increase": 1 + }, + "quotient_coordinates": 1092, + "seconds": 46.47324045805726 + }, + { + "all_scalar_coefficients_after_operator_quotient_real_rational": true, + "exact_non_Y_projection_rank_over_Q_i": 554, + "exact_pure_Y_any_physical_operator_dimension": 0, + "exact_rank_V_over_Q_i": 554, + "full_frame_versions": 5019, + "max_basis_denominator_bits": 6, + "max_basis_numerator_bits": 6, + "name": "source-backward", + "positive_pure_Y_identity_injection": { + "pure_Y_dimension_after_injection": 1, + "rank_increase": 1 + }, + "quotient_coordinates": 1092, + "seconds": 32.12903791607823 + }, + { + "all_scalar_coefficients_after_operator_quotient_real_rational": true, + "exact_non_Y_projection_rank_over_Q_i": 554, + "exact_pure_Y_any_physical_operator_dimension": 0, + "exact_rank_V_over_Q_i": 554, + "full_frame_versions": 4968, + "max_basis_denominator_bits": 6, + "max_basis_numerator_bits": 6, + "name": "source-forward", + "positive_pure_Y_identity_injection": { + "pure_Y_dimension_after_injection": 1, + "rank_increase": 1 + }, + "quotient_coordinates": 723, + "seconds": 24.572202416951768 + } + ], + "implementation_sha256": { + "monomial.py": "87cdb1688b841891eccefdcaebe67b97a6c86b7af676bbbb667d1d5ee5d45d3e", + "native.py": "1bad1ffe747c3977d1a6bc1cfa9faa4127e38cbf49d7fcf4ae8060fbc7f67d4e" + }, + "independent_script_sha256": "08ec7f1897ab4292f037842288e3fcf239c2c6f412d0f10bf54615b2b5620345", + "operators": { + "basis_denominator_bits": 2, + "basis_numerator_bits": 2, + "coordinate_phase_gauge": "Every fixed physical matrix coordinate has one shared phase parity, making all 215 columns rational after invertible coordinate scaling. Rational rank is unchanged under scalar extension Q -> Q(i) -> C.", + "distinct_physical_matrix_coordinates": 38232, + "exact_kernel_dimension": 1, + "exact_pivot_coordinates": [ + [ + 0, + 0 + ], + [ + 16, + 16 + ], + [ + 16, + 64 + ], + [ + 8, + 8 + ], + [ + 4, + 4 + ], + [ + 32, + 48 + ], + [ + 8, + 15 + ], + [ + 8, + 16 + ], + [ + 8, + 64 + ], + [ + 16, + 74 + ], + [ + 32, + 86 + ], + [ + 8, + 27 + ], + [ + 8, + 40 + ], + [ + 32, + 32 + ], + [ + 16, + 43 + ], + [ + 32, + 62 + ], + [ + 16, + 27 + ], + [ + 8, + 10 + ], + [ + 2, + 2 + ], + [ + 8, + 385 + ], + [ + 16, + 44 + ], + [ + 8, + 12 + ], + [ + 1, + 1 + ], + [ + 2, + 4 + ], + [ + 16, + 154 + ], + [ + 8, + 32 + ], + [ + 16, + 31 + ], + [ + 8, + 128 + ], + [ + 8, + 387 + ], + [ + 16, + 128 + ], + [ + 64, + 32 + ], + [ + 8, + 54 + ], + [ + 128, + 128 + ], + [ + 16, + 57 + ], + [ + 16, + 84 + ], + [ + 32, + 143 + ], + [ + 64, + 98 + ], + [ + 16, + 293 + ], + [ + 16, + 121 + ], + [ + 16, + 392 + ], + [ + 16, + 50 + ], + [ + 32, + 138 + ], + [ + 32, + 64 + ], + [ + 16, + 83 + ], + [ + 16, + 415 + ], + [ + 16, + 39 + ], + [ + 16, + 23 + ], + [ + 64, + 64 + ], + [ + 64, + 67 + ], + [ + 128, + 135 + ], + [ + 64, + 70 + ], + [ + 64, + 89 + ], + [ + 8, + 6 + ], + [ + 8, + 5 + ], + [ + 8, + 31 + ], + [ + 8, + 30 + ], + [ + 16, + 24 + ], + [ + 16, + 8 + ], + [ + 16, + 266 + ], + [ + 16, + 35 + ], + [ + 16, + 398 + ], + [ + 16, + 427 + ], + [ + 4, + 8 + ], + [ + 16, + 40 + ], + [ + 4, + 15 + ], + [ + 16, + 46 + ], + [ + 8, + 55 + ], + [ + 8, + 26 + ], + [ + 16, + 73 + ], + [ + 12, + 20 + ], + [ + 24, + 11 + ], + [ + 32, + 107 + ], + [ + 32, + 27 + ], + [ + 8, + 50 + ], + [ + 16, + 33 + ], + [ + 2, + 8 + ], + [ + 2, + 39 + ], + [ + 4, + 28 + ], + [ + 4, + 12 + ], + [ + 4, + 46 + ], + [ + 2, + 31 + ], + [ + 2, + 30 + ], + [ + 5, + 9 + ], + [ + 4, + 31 + ], + [ + 8, + 28 + ], + [ + 20, + 36 + ], + [ + 16, + 389 + ], + [ + 32, + 128 + ], + [ + 32, + 40 + ], + [ + 32, + 153 + ], + [ + 8, + 197 + ], + [ + 8, + 465 + ], + [ + 8, + 468 + ], + [ + 8, + 439 + ], + [ + 8, + 222 + ], + [ + 8, + 281 + ], + [ + 8, + 482 + ], + [ + 8, + 291 + ], + [ + 32, + 188 + ], + [ + 32, + 394 + ], + [ + 32, + 464 + ], + [ + 32, + 23 + ], + [ + 2, + 27 + ], + [ + 4, + 10 + ], + [ + 5, + 8 + ], + [ + 16, + 140 + ], + [ + 16, + 30 + ], + [ + 16, + 274 + ], + [ + 32, + 77 + ], + [ + 128, + 197 + ], + [ + 32, + 483 + ], + [ + 64, + 80 + ], + [ + 128, + 66 + ], + [ + 32, + 189 + ], + [ + 8, + 504 + ], + [ + 16, + 451 + ], + [ + 128, + 160 + ], + [ + 36, + 132 + ], + [ + 128, + 99 + ], + [ + 12, + 36 + ], + [ + 24, + 53 + ], + [ + 128, + 198 + ], + [ + 24, + 136 + ], + [ + 128, + 129 + ], + [ + 128, + 65 + ], + [ + 24, + 43 + ], + [ + 16, + 404 + ], + [ + 32, + 456 + ], + [ + 128, + 105 + ], + [ + 16, + 32 + ], + [ + 32, + 29 + ], + [ + 64, + 160 + ], + [ + 16, + 155 + ], + [ + 32, + 30 + ], + [ + 32, + 51 + ], + [ + 64, + 163 + ], + [ + 16, + 397 + ], + [ + 24, + 20 + ], + [ + 64, + 170 + ], + [ + 72, + 172 + ], + [ + 128, + 153 + ], + [ + 64, + 143 + ], + [ + 128, + 111 + ], + [ + 160, + 47 + ], + [ + 128, + 39 + ], + [ + 48, + 28 + ], + [ + 128, + 80 + ], + [ + 128, + 68 + ], + [ + 32, + 492 + ], + [ + 128, + 195 + ], + [ + 160, + 61 + ], + [ + 48, + 123 + ], + [ + 80, + 210 + ], + [ + 48, + 507 + ], + [ + 18, + 130 + ], + [ + 64, + 106 + ], + [ + 192, + 192 + ], + [ + 40, + 23 + ], + [ + 9, + 17 + ], + [ + 32, + 72 + ], + [ + 24, + 22 + ], + [ + 48, + 63 + ], + [ + 32, + 46 + ], + [ + 48, + 268 + ], + [ + 128, + 149 + ], + [ + 32, + 85 + ], + [ + 64, + 387 + ], + [ + 64, + 130 + ], + [ + 16, + 79 + ], + [ + 4, + 47 + ], + [ + 32, + 47 + ], + [ + 32, + 144 + ], + [ + 24, + 19 + ], + [ + 32, + 139 + ], + [ + 24, + 144 + ], + [ + 32, + 142 + ], + [ + 128, + 166 + ], + [ + 96, + 187 + ], + [ + 64, + 129 + ], + [ + 24, + 72 + ], + [ + 2, + 132 + ], + [ + 18, + 10 + ], + [ + 64, + 141 + ], + [ + 20, + 24 + ], + [ + 5, + 44 + ], + [ + 34, + 74 + ], + [ + 4, + 2 + ], + [ + 20, + 12 + ], + [ + 32, + 43 + ], + [ + 32, + 75 + ], + [ + 24, + 34 + ], + [ + 20, + 43 + ], + [ + 36, + 79 + ], + [ + 160, + 108 + ], + [ + 128, + 79 + ], + [ + 16, + 28 + ], + [ + 40, + 167 + ], + [ + 32, + 135 + ], + [ + 24, + 52 + ], + [ + 32, + 79 + ], + [ + 32, + 98 + ], + [ + 32, + 26 + ], + [ + 32, + 81 + ], + [ + 36, + 68 + ], + [ + 96, + 303 + ], + [ + 160, + 401 + ], + [ + 96, + 368 + ], + [ + 32, + 392 + ], + [ + 20, + 394 + ], + [ + 17, + 9 + ], + [ + 66, + 162 + ], + [ + 32, + 55 + ], + [ + 32, + 54 + ], + [ + 36, + 99 + ] + ], + "exact_rank_over_C": 214, + "exact_rank_over_Q_i": 214, + "kernel_relation": { + "156": "-1", + "157": "1", + "49": "-1", + "51": "1" + }, + "operator_count": 215, + "phase_exponent_counts": { + "0": 33824, + "1": 27136, + "2": 21984, + "3": 27136 + }, + "wrong_phase_control": { + "exact_mutated_rank_over_Q_i": 215, + "exact_relation_rejected": true, + "input_column": 1, + "nonzero_residual_coordinates": 1, + "operator": 157, + "permutation_preserved": true, + "phase_increment_mod4": 1, + "rational_gauge_rejected": true, + "unit_coordinate_outside_original_span": true, + "zero_column_phase_anchor_preserved": true + } + }, + "scope": "Width-one scalar span of all retained full-frame versions under the source replay. All actual signed-monomial matrix relations are quotiented exactly. No closure under arbitrary free left transports, modified native history, supplied correlated observations, all-width implementation, or new kappa is asserted.", + "seconds": 105.72680175001733, + "source_sha256": { + "provider": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc", + "source": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + }, + "status": "PASS_INDEPENDENT_EXACT_WIDTH1_PHYSICAL_QUOTIENT" +} diff --git a/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md b/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md new file mode 100644 index 0000000000..c576e1e55b --- /dev/null +++ b/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md @@ -0,0 +1,43 @@ +# Internal corroboration and its limits + +Separate OpenAI Codex agents checked the source-specific phase algebra and +tensor argument. This is internal AI-assisted review, not independent human +acceptance or a proof-kernel result. + +- `phase_audit.py` uses the pinned signed Clifford evaluator and its absolute + phase anchor, rather than the primary direct Gram-phase column formula. + All 147,456 native variants and 36,864 product columns agree, including raw + backward conjugation. Its phase controls remain active under `-O`. +- `independent_width1.py` separately implements exact Fraction elimination + with a checked coordinate phase gauge. It recovers physical rank 214 and + the four-term relation, then computes the actual quotient ranks 546/546, + 554/554 and 554/554 without modular inference. A phase error at input + column one preserves the permutation and zero-address anchor while raising + physical operator rank from 214 to 215. The optional author's normal replay + passed in 90.663 seconds after adapting imports; the final whitespace-normalized + source replay passed in 105.727 seconds. The + self-contained receipt is `INDEPENDENT-WIDTH1.json`. +- A separate Gaussian-integer Gram implementation reproduced width-two rank + 215 and determinant 298401053 modulo 1000000009, in normal and optimized + modes. The registered primary checker regenerates this same certificate. +- A separate literal-normalizer implementation checked all 31,457,280 seed + Gaussian-kernel entries, and independently reproduced the 1,012/59/59,708 + ABI image/product counts and set hashes. Static review found the required + physical/logical commutation and finite-family tensor argument valid. The + portable registered `abi_closure.py` regenerates the published certificate. + +The registered commands, their source pins and the written proofs are the +public reproduction path. The last two internal audits are corroboration, +not additional standalone registered entry points. Source-generation scripts +were not changed to obtain these results. + +Optional exact width-one corroboration: + +```sh +python3 -I -B research/physical-zqy-scalar-span/independent_width1.py +``` + +It writes nothing by default and prints +`PASS_INDEPENDENT_EXACT_WIDTH1_PHYSICAL_QUOTIENT`. Its explicit `--write` +option regenerates the separate receipt. The registered rank-sandwich proof +already suffices; this slower exact calculation is not required for CI. diff --git a/research/physical-zqy-scalar-span/PROOF.md b/research/physical-zqy-scalar-span/PROOF.md new file mode 100644 index 0000000000..db69d4d2b7 --- /dev/null +++ b/research/physical-zqy-scalar-span/PROOF.md @@ -0,0 +1,225 @@ +# Physical scalar-span separation at every positive tensor width + +THU New Media Research Center (@thu-nmrc), with substantial OpenAI Codex +assistance. Apache-2.0. Event and history semantics follow Mark/Matarener's +[#5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427); native words +and phase conventions retain the source authors listed in README.md. + +## 1. Precisely the interface being tested + +Fix the literal inputs in SOURCES.json: Cao Yifan's final #4610 forward and +backward words, and Dillon's #5402 backward coupled-provider word. All 632 +original input fields are independent. Owned entry fields are also independent +until the literal word clears them. No new helper relation is imposed. + +For each word, collect every nonzero field version immediately after an event +at which that field occupies the unique full nine-axis frame. Grant retention +of every such version over the entire execution, even past the intended exit. +The grant ignores its ordinary storage cost and chronology, making an +exclusion stronger within this grammar. Different versions may be combined +with arbitrary complex scalars, possibly depending on tensor width f. + +Write Y for original fields L112 through L223. A pure-Y observation is any +linear field expression depending only on these 112 original fields. Its +coefficients need not be identity operators. The target b=Z Q Y in the +#5415/#5419 interface is relevant because it is a nonzero pure-Y observation +when its current Y=Dy is referred back to this call's input. The statement +below concerns direct scalar combinations of retained full-frame versions. + +**Theorem.** At every integer f>=1, for each of the three frozen words, the +complex scalar span of the granted versions contains no nonzero pure-Y +observation. This includes width-dependent complex scalar coefficients. + +**Boundary.** Versions are not independently preprocessed by arbitrary free +left monomial maps before combination. Such a module closure, partial-frame +versions, changed words, new paid queries, supplied observations, different +providers and caller-level changes remain outside the theorem. In particular, +this does not prove that every endogenous ZQY observer is impossible. + +## 2. Literal phase algebra + +For a nine-bit invertible binary map G, the retained native convention is + + K_G |x> = i^{q_G(Gx)} |Gx>, + Q_G = I + G^{-T} G^{-1}, + +where q_G has diagonal coefficients (Q_G)jj in Z/4 and off-diagonal +coefficients 2(Q_G)ij. `monomial.native` evaluates all 512 signed columns. +Composition, inverse and complex conjugation retain these columns literally. +For a backward warp the operator is the inverse transpose of the forward +operator, hence its complex conjugate, not a permutation with discarded phase. +The separately implemented phase audit compares 147,456 native signed columns +and 36,864 product columns with the retained Clifford evaluator. + +Every native map and every product used here sends |0> to |0> with coefficient +one. Thus projective aliases in this set cannot hide a nontrivial global phase. +The 72 native labels contain 58 distinct signed operators. Across the three +replays, including inverse/conjugate products, there are exactly 215 operators +A0,...,A214, with A0=I. Each is lifted as the SAME one-column operator on all +f columns. Independent per-column controls are not silently granted. + +A literal logical row is + + sum_{input r, operator j} c[r,j] A_j^{tensor f} input_r. + +Scalar ADD/COPY/CLEAR and scale events act exactly on these rows. Paid climbs +change only the frame. Warps left-multiply by the actual signed operator. +All recorded versions occupy a common invertible physical full-frame map; +removing that common map preserves linear dependence and the input-support +property. Forward and raw backward frames are treated in their respective +conventions. The source frames and event order are checked during replay. + +## 3. Exact group-coordinate projection ranks + +Temporarily regard the 215 distinct signed operators as formal coordinates. +Let V be the version span and let pi delete all Y coordinates, retaining X, +all original helpers and all owned entry coordinates. Exact Fraction +elimination gives: + +| Frozen word | Full-frame versions | dim V | dim pi(V) | +|---|---:|---:|---:| +| #5402 backward | 4,891 | 546 | 546 | +| #4610 backward | 5,019 | 554 | 554 | +| #4610 forward | 4,968 | 554 | 554 | + +These are exact rational ranks, not floating tolerances. Rank is unchanged by +extension to C. Since the two ranks agree, pi is injective on V. Appending the +original pure-Y identity row increases each rank by one, so the checker can +detect a supplied observation. Actual operator identities must still be +handled; distinct one-column operators are not necessarily linearly independent. + +## 4. Width one: a real physical relation, with a separate rank argument + +The 215 actual one-column matrices have rank exactly 214. There is an exact +four-term relation in the deterministic replay enumeration: + + A157 + A51 - A156 - A49 = 0. + +The verifier checks this equality at every matrix coordinate. A changed +absolute phase breaks it. A rank-214 minor modulo p=998244353 under +`i -> 911660635` proves a rank LOWER bound over Q(i). The exact displayed +relation gives the matching upper bound, so the remaining 214 matrices after +eliminating A157 form a C-basis. + +Substitute A157=A156+A49-A51 in every version. In this physical quotient, +modular elimination of the non-Y projection gives lower bounds 546,554,554. +The exact ranks in section 3 give upper bounds of the same sizes for the +entire quotient version spaces. Projection rank cannot exceed the rank of +the space. Therefore the actual width-one projection is injective in all +three cases. This excludes nonzero pure-Y observations at f=1. + +No conclusion is obtained merely from modular nonmembership. A rational +solution can have a denominator divisible by the test prime; that shortcut +would be invalid. Here modular computations certify nonzero minors only, +and exact rational upper bounds complete the argument. An additional, +separately implemented exact rational physical-quotient audit corroborates +these ranks without modular inference. + +## 5. Width two and all larger widths + +For the actual signed columns, form the Hermitian Hilbert-Schmidt Gram +matrix + + H_ij = Tr(A_i^* A_j), + G_ij = H_ij^2. + +The square is literal, not an absolute-value square: G is the Gram matrix of +A_i tensor A_i. Entries are Gaussian integers. Modulo p=1000000009 with +`i -> 569522298`, the 215-by-215 matrix has full rank and determinant +298401053. Thus its Gaussian-integer determinant is nonzero, and the 215 +literal tensor squares are C-linearly independent. This finite certificate +uses no large tensor matrices or numerical singular-value threshold. + +For f>2, apply the linear functional ell(T)=<0|T|0> to each of the final f-2 +operator tensor factors. Every A_j has ell(A_j)=1. A putative relation among +A_j^{tensor f}, with any width-dependent coefficients, would therefore give +the same relation among A_j^{tensor 2}. Independence at width two makes all +coefficients zero. Hence these 215 operator lifts are independent at every +f>=2. Section 3 is consequently the actual physical rank computation at +all such widths. Together with section 4, this proves the theorem. + +## 6. Consequence and remaining construction work + +This resolves the actual-phase scalar-span question left open by #5427's +formal-word native test, including its width-one check. It does not copy +that predecessor's caller-level or paid-response-reuse conclusions into a +stronger grammar. It does not change a paid or productive histogram, install +a supplier, improve kappa or audit the multiplication framework. + +A constructive continuation must change an explicit premise. The smallest +nearby one is to allow the concrete Z-ABI monomial maps on separately retained +versions, then prove a phase-correct pure-Y witness at the actual current-Y +cut. Another is a changed native schedule that saves pure Ry before Dx is +mixed in. Such constructions must retain all independent input directions, +owned returns, lifetime and the complete observer/termination bill. + +## 7. A separate concrete Z-ABI left-image theorem + +The constructive continuation also tests a larger, explicitly finite family +on the #5402 backward history. Let Kp_i be its 112 physical port normalizers +and Km_a its eight physical mode normalizers. In addition to no preprocessing, +grant each retained version any ONE left image from + + T = { I, Kp_i, Km_a, Km_a^{-1} Kp_i }. + +There are 1,017 listed entries and 1,012 distinct signed maps; seed inverses +already occur among the seeds. This is a bank of allowed left images, not +closure under arbitrary products of its generators. Each version may receive +its own allowed image before scalar combination. Each selected one-column +map is lifted identically on all f columns; per-column choices are outside +this finite family. + +The source ABI has + + Z = diag(Km_a^{-1}) M^T diag(Kp_i) / 2, + W = diag(Kp_i^{-1}) M diag(Km_a) / 2, + M^T M = 56 I8, ZW = 14 I8. + +Thus its termwise composite maps Km_a^{-1}Kp_i are included. The target b is +nonzero for independent native-return Y=Dy. A later caller Y contaminated by +X is not silently identified with this pure-original-Y target. + +`abi_closure.py` authenticates the two additional pinned JSON inputs and +checks the normalizers literally, with phases. Each seed is a real signed +orthogonal linear permutation K|x>=i^{phi(x)}|Gx> satisfying + + phi(x) - wt(x) + wt(Gx) = 0 mod 4. + +The full-frame kernel is R[y,x]=alpha*(-i)^{wt(x xor y)}. Orthogonality and +the displayed signed-weight relation give KR=RK, including phase. Hence +physical preprocessing and logical left multiplication agree: +R^{-1}KR=K. The same holds for the raw backward common frame and seed +products. These normalizers are not admitted as free merely from a frame tag. +The separate checker verifies 61,440 seed/address conditions. + +Only 59 of the 215 signed operators occur in the backward provider's full-frame +versions. The literal products T A, over the 1,012 maps T and these 59 operators +A, are all 59,708 distinct maps. All have zero-state coefficient one, so they +are pairwise nonproportional. No left-image support collision occurs. + +Consequently the translated spaces T V form a direct sum in formal product +coordinates. Their non-Y projections form the same direct sum: left multiplication +does not change the original input owner. The exact base 546/546 projection +certificate therefore makes the entire finite left-image projection injective. + +For completeness, a classical separating-functional argument supplies a +rigorous width bound without a huge Gram computation. For each pair of +nonproportional vectors v_i,v_j choose a linear functional ell_ij with +ell_ij(v_j)=0 and ell_ij(v_i)!=0. The tensor product over j!=i is a functional +on tensor degree N-1 that vanishes on all v_j^{tensor(N-1)} except v_i. +Thus N pairwise projectively distinct matrices have independent tensor powers +at degree N-1. The common zero-state anchor extends independence to every +larger degree, as in section 5. Apply this with N=59,708. + +**Fixed-ABI theorem.** At every f>=59,707, the span of the granted 1,012 left +images of every retained backward-provider full-frame version contains no +nonzero pure-Y observation. Arbitrary width-dependent complex scalar +coefficients are allowed. In particular, this fixed family cannot supply b +by an identity valid at all widths, or throughout a consecutive infinite tail. + +No small-width nonmembership claim is made for this enlarged family. Further +products, arbitrary monomial left maps, new paid observations, changed native +words and different input/return contracts remain outside the result. The +checker consumes the primary exact rank certificate; it is not a substitute +for replaying that certificate. This extension changes neither paid jobs nor +productive targets and supplies no new kappa. diff --git a/research/physical-zqy-scalar-span/README.md b/research/physical-zqy-scalar-span/README.md new file mode 100644 index 0000000000..a1d90de9b0 --- /dev/null +++ b/research/physical-zqy-scalar-span/README.md @@ -0,0 +1,95 @@ +# Actual-phase native history scalar spans + +This package resolves the physical scalar-span question left open by +[Mark/Matarener's #5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427). +At **every positive tensor width**, no nonzero pure-Y observation is a scalar +combination of all retained full-frame versions of the frozen #5402 backward +word or either orientation of the final #4610 word. All original inputs remain +independent. The complete history is granted, including versions after an exit. + +The new point is the actual operator algebra. The 215 signed operators have +one genuine four-term linear relation at width one. After including that +relation the observation still does not exist. A full-rank tensor-square Gram +certificate and the shared zero-state anchor cover every larger width. Exact +rational projection ranks and nonzero modular minors play separate roles; +modular nonmembership alone is not used as a rational exclusion. + +**This is a restricted negative theorem, with no new kappa.** It does not close +the history under independently chosen free left monomial maps, including the +concrete Z-ABI transports. It does not exclude changed native schedules, +partial-frame histories, new paid queries or an endogenous observer in those +larger models. The independent inputs, observation version and these limits +are part of the claim. See [PROOF.md](PROOF.md). + +## Reproduce + +Python 3.12, standard library only, read-only default: + +```sh +python3 -B scripts/research_package.py --package research/physical-zqy-scalar-span +``` + +Expected mathematical marker: + +```text +PASS_ALL_WIDTH_PHYSICAL_NATIVE_SCALAR_SPAN_NO_NEW_KAPPA +``` + +The registered checks recompute the finite ABI left-image certificate, all +source-bound row ranks, the one-column operator relation/rank and the tensor-square Gram certificate, in normal and +optimized modes. The separate phase audit compares actual columns against the +retained exact Clifford implementation. `--write` explicitly regenerates the +local result; ordinary replay compares it without writing. Mathematical/runtime +checks are recorded in VALIDATION.md; publication byte/export transport results +are recorded in the PR. [INTERNAL-REVIEW.md](INTERNAL-REVIEW.md) separates internal +corroboration from external acceptance. No full native admission, selected cold +replay, compiler/outer, precision/tape, Lean or Docker run is claimed. + +## Concrete Z-ABI left-image extension + +A separate bounded continuation grants each backward-provider version one +left image from `{I, Kp_i, Km_a, Km_a^-1 Kp_i}`. The 1,012 distinct physical +maps and 59 actual history operators give 59,708 pairwise nonproportional +products, with exact F9 commutation and phase checks. The resulting span has +no nonzero pure-Y observation for **every f>=59,707**. Thus this fixed bank +cannot implement an all-width observer. This does not assert small-width +nonmembership or closure under arbitrary further products. The proof and +[ABI-CLOSURE.json](ABI-CLOSURE.json) state this as a separate theorem. + +## Open next questions + +1. Modify the native word to retain pure Ry before Dx is mixed in. Price every + new observer job, storage slot and eventual termination. A supplied-observer + invoice is not its construction. +2. Supply a genuinely new, versioned nonfree observation from another paid + caller event, keeping disjoint mode ownership and every original input. + Reconstruct one actual current-Y exit before extending the caller. +3. Test a different producer or partial-frame interface with its own exact + arbitrary-input operator and complete bill. These theorems provide no + price lower bound for that changed construction. + +## Provenance and credit + +Prepared by THU New Media Research Center (@thu-nmrc) with substantial OpenAI +Codex assistance from a lead and separate algebra/phase reviewers. These agents +are not independent human reviewers or a proof kernel. Apache-2.0. + +- [Mark/Matarener, #5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427), + head `389578f2d3ef075495ce76f08100ac50e18f7d40`: formal-word question, + input/ownership/event/version semantics and the explicit physical follow-up. + `native.py` adapts those semantics with actual signed operator composition. +- [Dillon Amburgey/dillona, #5402](https://github.com/CrocSwap/integer-mult-bounds/pull/5402): + unrestricted coupled provider and all original mode inputs. +- [Cao Yifan/intqwq, #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610): + final native word and phase evidence. Cinna Davis/1337isnot1337, zxv, + Dugongue, Jacob Alan Sussman and retained source authors supply its native, + query, frame, tensor, compiler and analytic lineage. +- [zxv, #5415](https://github.com/CrocSwap/integer-mult-bounds/pull/5415) and + [#5419](https://github.com/CrocSwap/integer-mult-bounds/pull/5419): current-Y + observation contract, physical normalizers and consumer/cost obligations. +- [Ali Romman, #5377](https://github.com/CrocSwap/integer-mult-bounds/pull/5377): + retained native row conventions. Chris R/Clear1nsight's provider and caller + reviews remain separate from this scoped result. + +Frozen upstream packages, scientific receipts and selected-frontier files are +unchanged. Exact canonical input blobs and hashes are in SOURCES.json. diff --git a/research/physical-zqy-scalar-span/RESULT.json b/research/physical-zqy-scalar-span/RESULT.json new file mode 100644 index 0000000000..30b25b223d --- /dev/null +++ b/research/physical-zqy-scalar-span/RESULT.json @@ -0,0 +1,81 @@ +{ + "cases": [ + { + "exact_group_non_Y_projection_rank": 546, + "exact_group_rank": 546, + "full_frame_versions": 4891, + "group_coordinate_count": 1090, + "max_denominator_bits": 5, + "max_numerator_bits": 6, + "name": "provider-backward", + "positive_injection_rank": 547, + "width_one_modular_rank_bounds": { + "positive_control_rank": 547, + "rank_lower_V": 546, + "rank_lower_non_Y_projection": 546 + } + }, + { + "exact_group_non_Y_projection_rank": 554, + "exact_group_rank": 554, + "full_frame_versions": 5019, + "group_coordinate_count": 1090, + "max_denominator_bits": 6, + "max_numerator_bits": 6, + "name": "source-backward", + "positive_injection_rank": 555, + "width_one_modular_rank_bounds": { + "positive_control_rank": 555, + "rank_lower_V": 554, + "rank_lower_non_Y_projection": 554 + } + }, + { + "exact_group_non_Y_projection_rank": 554, + "exact_group_rank": 554, + "full_frame_versions": 4968, + "group_coordinate_count": 723, + "max_denominator_bits": 6, + "max_numerator_bits": 6, + "name": "source-forward", + "positive_injection_rank": 555, + "width_one_modular_rank_bounds": { + "positive_control_rank": 555, + "rank_lower_V": 554, + "rank_lower_non_Y_projection": 554 + } + } + ], + "controls": [ + "injected pure-y identity raises rank in every case", + "wrong absolute phase breaks exact four-term relation" + ], + "new_kappa": false, + "operator_certificate": { + "exact_relation": { + "49": -1, + "51": 1, + "156": -1, + "157": 1 + }, + "operators": 215, + "rank_lower_prime": 998244353, + "sqrt_minus_one": 911660635, + "width_one_exact_rank": 214, + "wrong_phase_control": true + }, + "productive_or_paid_profile_change": false, + "schema": "physical-zqy-scalar-span/v1", + "scope": "Scalar linear combinations of all full-frame versions of these frozen native words; excludes arbitrary independently chosen free left maps and changed words.", + "source_payload_sha256": "cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd", + "status": "PASS_ALL_WIDTH_PHYSICAL_NATIVE_SCALAR_SPAN_NO_NEW_KAPPA", + "tensor_square_gram": { + "all_zero_anchors_one": true, + "determinant_mod_prime": 298401053, + "prime": 1000000009, + "rank": 215, + "sqrt_minus_one": 569522298, + "width": 2 + }, + "widths": "all positive integers; coefficients may depend on width and be complex" +} diff --git a/research/physical-zqy-scalar-span/SOURCES.json b/research/physical-zqy-scalar-span/SOURCES.json new file mode 100644 index 0000000000..d0d899c492 --- /dev/null +++ b/research/physical-zqy-scalar-span/SOURCES.json @@ -0,0 +1,55 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "usage": "input", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e" + }, + { + "path": "research/native-rank8-helper-provider/WORD.json.gz", + "usage": "input", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc", + "git_blob": "f3111b47e89496da8ca0ee45b2e4b258c0634d8e" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446" + }, + { + "path": "research/coded-native-caller/NORMALIZERS.json", + "usage": "input", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f" + }, + { + "path": "research/native-rank8-helper-provider/PROVIDER.json", + "usage": "input", + "sha256": "676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65", + "git_blob": "0afd30ed01202eb6ce62462dcf8bc9164f3b0455" + } + ], + "predecessor_source": { + "pr": 5427, + "commit": "389578f2d3ef075495ce76f08100ac50e18f7d40", + "path": "research/zqy-observation-not-retained/verify.py", + "sha256": "40fd198b79490c5897feb45cd8b6fbe9cf3f8f5c9e0215efb2b9973c8e92106a", + "usage": "attribution and adapted event/version semantics; not a runtime input" + } +} diff --git a/research/physical-zqy-scalar-span/TASK.json b/research/physical-zqy-scalar-span/TASK.json new file mode 100644 index 0000000000..a62de3f881 --- /dev/null +++ b/research/physical-zqy-scalar-span/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. 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", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Resolve actual-phase scalar-span separation at every positive tensor width, and exclude the concrete1012-map Z-ABI left-image family at every f>=59707, for the frozen native histories.", + "scope_change_reason": "The named physical follow-up was unexecuted. Actual operators have a width-one relation and need an all-width argument beyond formal words. A separate bounded constructive continuation tested the actual ABI monomial left images and found disjoint operator supports; the resulting finite-family theorem is stated separately.", + "bottleneck_link": "The#5415/#5419 consumer needs current ZQY; this rejects one zero-new-query grammar while leaving monomial preprocessing and changed native producers open.", + "budget_minutes": 60, + "stop_rule": "Finish both scoped physical separation statements and registered checks; stop this frozen scalar/finite-ABI family. Changed native producers or unrestricted products require a new hypothesis and budget.", + "outcome": "negative-result", + "evidence": "PROOF.md, RESULT.json, literal phase audit, exact rational projection ranks and a Gaussian-integer Gram minor. ABI-CLOSURE.json authenticates1012 left maps and59708 pairwise nonproportional products; a separating-functionals proof supplies its width threshold.", + "author": "THU New Media Research Center (@thu-nmrc)", + "ai_assistance": "Substantial OpenAI Codex assistance by lead and separate algebra/phase agents; no independent human or kernel review.", + "open_questions": [ + { + "question": "Can a changed native word retain pure Ry before Dx mixing at a profitable complete price?", + "why_it_matters": "Both frozen scalar and the specified finite Z-ABI image bank are excluded; a changed producer can supply new information.", + "first_step": "Emit one all-input prefix, its current-Y observation, every owned return and complete observer/termination bill.", + "blocked_by": "No profitable changed physical producer is known in this package." + }, + { + "question": "Can another real paid caller event supply a correlated current-version observation with disjoint mode ownership?", + "why_it_matters": "New nonfree history leaves the frozen-history hypotheses and could eliminate actual recursive calls.", + "first_step": "Specify one exact event/cut with all original inputs, observation owners and later consumers, then replay the complete exit.", + "blocked_by": "No source-bound witness, lifetime proof and full bill are established here." + } + ] +} diff --git a/research/physical-zqy-scalar-span/VALIDATION.md b/research/physical-zqy-scalar-span/VALIDATION.md new file mode 100644 index 0000000000..5bb776d062 --- /dev/null +++ b/research/physical-zqy-scalar-span/VALIDATION.md @@ -0,0 +1,49 @@ +# Validation scope + +Python 3.12.14, standard library only, macOS arm64. No dependency install, +Lean, Docker, selected cold replay or unrelated historical suite was run. + +## Mathematical checks + +- Exact source-bound native rows, all full-frame history versions and rational + ranks: 4,891 /546, 5,019 /554 and 4,968 /554. Non-Y projection ranks match. +- The actual width-one operator rank is 214, with the exact four-term relation + and a separate nonzero Gaussian-integer minor. Physical quotient projection + lower bounds match exact rational upper bounds; no modular nonmembership + shortcut is used. +- Width-two 215-by-215 Gram determinant is 298401053 modulo 1000000009. + Every literal operator has zero-state coefficient one. The written + contraction proof covers every larger width. +- Independent Clifford phase audit: 147,456 native columns, 36,864 product + columns; wrong-phase and backward-direction controls. +- Fixed Z-ABI bank: 1,012 distinct left maps, 59 provider operators, 59,708 + pairwise distinct products and exact zero anchors. Exact signed F9 kernel + checks authenticate physical/logical left multiplication. The written + separating-functional proof has the explicit guard f>=59,707. +- Additional exact width-one Fraction audit passes without modular rank + inference; its portable optional script and separate receipt are included. + It ran in 90.663 seconds after import adaptation and 105.727 seconds after + final whitespace normalization. Internal audit is distinct + from external scientific acceptance; see INTERNAL-REVIEW.md. + +All six registered normal/optimized commands PASS. The primary normal and +optimized mathematical runs took 134.403 and 157.388 seconds respectively. +Phase and fixed-ABI replays also PASS in both modes. Publication byte/export +transport checks are recorded separately in the pull request after commit. Individual commands use explicit +exceptions; mathematical checks are not disabled by `-O`. The retained +Clifford engine has its own assertion-based internals, while the audit's +literal column comparisons and negative controls remain explicit. + +Development record: the first registered attempt rejected the result's JSON +key representation after completing its mathematical checks. Integer relation +indices are now serialized as strings. The revised result compares identically; +this repair changes no rank, source operator or scientific conclusion. + +## Limits + +No runtime measurement here is a physical fixed-tape benchmark. The frozen +source words and inherited Clifford realization are reused, not readmitted as +a new complete native supplier. No new paid or productive profile, exponent, +precision/tape/stock/compiler funding or multiplication theorem is claimed. +The finite ABI theorem is not arbitrary monomial group/module closure and +makes no enlarged-family small-width exclusion. diff --git a/research/physical-zqy-scalar-span/VERIFY.json b/research/physical-zqy-scalar-span/VERIFY.json new file mode 100644 index 0000000000..99d2287eb4 --- /dev/null +++ b/research/physical-zqy-scalar-span/VERIFY.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "research/native-rank8-helper-provider/WORD.json.gz", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "research/coded-native-caller/NORMALIZERS.json", + "research/native-rank8-helper-provider/PROVIDER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact rational history ranks, width-one physical quotient rank sandwich, absolute-phase control and tensor-square all-width certificate." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Exact rational history ranks, width-one physical quotient rank sandwich, absolute-phase control and tensor-square all-width certificate." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/phase_audit.py" + ], + "timeout_seconds": 90, + "checks": "Independent retained Clifford/tableau/absolute-phase comparison of147456 native columns and36864 product columns, with phase/orientation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/phase_audit.py" + ], + "timeout_seconds": 90, + "checks": "Independent retained Clifford/tableau/absolute-phase comparison of147456 native columns and36864 product columns, with phase/orientation controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/abi_closure.py" + ], + "timeout_seconds": 90, + "checks": "Checks fixed1012 physical Z-ABI left maps, exact F9 commutation,59708 distinct signed products and zero anchors; consumes the freshly replayed primary exact546/546 rank certificate. Eventual-width proof is in PROOF.md." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/abi_closure.py" + ], + "timeout_seconds": 90, + "checks": "Checks fixed1012 physical Z-ABI left maps, exact F9 commutation,59708 distinct signed products and zero anchors; consumes the freshly replayed primary exact546/546 rank certificate. Eventual-width proof is in PROOF.md." + } + ] +} diff --git a/research/physical-zqy-scalar-span/abi_closure.py b/research/physical-zqy-scalar-span/abi_closure.py new file mode 100644 index 0000000000..c61aafeb13 --- /dev/null +++ b/research/physical-zqy-scalar-span/abi_closure.py @@ -0,0 +1,180 @@ +#!/usr/bin/env python3 +"""Fixed physical Z-ABI left-image audit; default replay is read-only. + +Predecessors: physical K normalizers/C by the #4933 lineage; the actual +coupled provider and its mode boundaries by Dillon's #5402; Z/W observer ABI +by #5415/#5419; native event/version semantics by Mark (Matarener), #5427. +This finite composed-normalizer audit was prepared for THU New Media Research +Center (@thu-nmrc) with substantial OpenAI Codex assistance. Apache-2.0. + +This is a bounded family of independently chosen left images, not closure +under arbitrary products of its generators or an arbitrary-free-control +lower bound. The primary registered verify.py proves the base exact rank. +""" +from pathlib import Path +from array import array +from hashlib import sha256 +import argparse,json,sys,struct +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import native as N +import monomial as M + +INPUTS={ + 'normalizers':('research/coded-native-caller/NORMALIZERS.json', + 'ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da'), + 'provider_interface':('research/native-rank8-helper-provider/PROVIDER.json', + '676de7551d3364598f4a7e29ae97cae0e4364348786bbe70435b84294ba7dd65')} + + +def read(name): + rel,digest=INPUTS[name];raw=(N.ROOT/rel).read_bytes() + N.need(sha256(raw).hexdigest()==digest,'fixed ABI input bytes '+rel) + return json.loads(raw) + + +def row_map(rows,x): + return sum(((rows[j]&x).bit_count()%2)<>j&1) + phase+=2*sum(((rows[j]>>k)&1) for j in range(9)for k in range(j+1,9) + if (x>>j&1)and(x>>k&1)) + return phase%4 + + +def literal(word): + """Literal chronological P/D/X/phase monomial, including absolute phase.""" + values=list(M.decode(M.IDENTITY)) + for event in word: + kind=event[0] + if kind=='P': + N.need(len(event[1])==9,'nine-axis P') + values=[4*row_map(event[1],v//4)+v%4 for v in values] + elif kind=='D': + N.need(len(event[1])==len(event[2])==9,'nine-axis D') + values=[4*(v//4)+(v%4+quadratic(event[1],event[2],v//4))%4 for v in values] + elif kind=='X':values=[4*((v//4)^event[1])+v%4 for v in values] + elif kind=='phase':values=[4*(v//4)+(v%4+event[1])%4 for v in values] + else:raise ValueError('non-monomial ABI event '+repr(kind)) + N.need(sorted(v//4 for v in values)==list(range(512)),'literal monomial permutation') + return array('H',values).tobytes() + + +def exact_R_centralizer(operator): + """Check sufficient exact signed-linear full-Gaussian kernel identities. + +K|x>=i^phase(x)|Gx>. Orthogonal G and a real linear sign, together with +phase(x)-wt(x)+wt(Gx)=0 mod4, imply KR=RK for +R[y,x]=alpha*(-i)^wt(x+y). The scalar alpha is retained on both sides. +""" + values=M.decode(operator) + N.need(values[0]==0,'ABI zero-address absolute phase') + columns=[values[1<>j&1)%4 + N.need(phase==v%4,'linear ABI sign at every address') + N.need((phase-x.bit_count()+(v//4).bit_count())%4==0, + 'exact full-Gaussian signed kernel commutation') + return 512 + + +def digest_operators(operators): + return sha256(b''.join(sorted(struct.pack('<512H',*M.decode(op)) for op in operators))).hexdigest() + + +def calculate(): + normalizers=read('normalizers');interface=read('provider_interface') + ports=[literal(row['K_word']) for row in normalizers['ports']] + mode_rows=interface['mode_boundaries'] + modes=[literal(row['input_K']['literal_word']) for row in mode_rows] + N.need(len(ports)==112 and len(modes)==8,'112-port/eight-mode ABI') + N.need([row['mode']for row in mode_rows]==list(range(8)),'ordered mode basis') + N.need([row['owner']for row in mode_rows]==interface['mode_owners'],'physical mode ownership') + mode_columns=normalizers['mode_columns'] + N.need(len(mode_columns)==8 and all(len(c)==112 for c in mode_columns),'source mode matrix shape') + N.need(all(x in (-1,0,1)for c in mode_columns for x in c),'source mode entries') + N.need(sum(x!=0 for c in mode_columns for x in c)==448,'mode support count') + for a in range(8): + for b in range(8): + N.need(sum(x*y for x,y in zip(mode_columns[a],mode_columns[b]))==56*int(a==b), + 'physical Z/W mode Gram identity') + anchor_checks=sum(exact_R_centralizer(x)for x in ports+modes) + N.need(all(M.inverse(x)==x for x in ports+modes),'seed normalizer inverses already present') + + source=N.read('source');provider=N.read('provider');canon=source['canonical'];N.initialize(canon) + versions,rows,frames,full=N.native_replay(canon,provider['word'],True) + N.need(len(versions)==4891,'complete provider full-frame history') + used_indices=sorted({op for row in versions for role,op in row}) + base_operators=[N.operators[i]for i in used_indices] + N.need(len(base_operators)==59 and len(set(base_operators))==59,'59 literal base operators') + N.need(all(M.decode(op)[0]==0 for op in base_operators),'base zero anchors') + # This check consumes the primary registered exact certificate. It does not + # substitute a modular rank test for that exact base injectivity proof. + primary=json.loads((HERE/'RESULT.json').read_text()) + base=next(row for row in primary['cases']if row['name']=='provider-backward') + N.need(base['full_frame_versions']==4891 and + base['exact_group_rank']==base['exact_group_non_Y_projection_rank']==546, + 'primary exact base-span injectivity certificate') + + raw=[('I',M.IDENTITY)] + raw += [('Kp_'+str(i),x)for i,x in enumerate(ports)] + raw += [('Km_'+str(a),x)for a,x in enumerate(modes)] + raw += [('Km_'+str(a)+'^-1_Kp_'+str(i),M.multiply(M.inverse(km),kp)) + for a,km in enumerate(modes)for i,kp in enumerate(ports)] + N.need(len(raw)==1017,'declared finite ABI family before deduplication') + seen=set();family=[] + for name,operator in raw: + if operator not in seen:seen.add(operator);family.append((name,operator)) + N.need(len(family)==1012,'1012 distinct concrete ABI left maps') + N.need(all(M.decode(op)[0]==0 for name,op in family),'left-map absolute zero anchors') + products=set();zero_anchors=0 + for name,left in family: + for right in base_operators: + product=M.multiply(left,right) + N.need(product not in products,'left-image operator-support collision') + products.add(product) + N.need(product[:2]==b'\0\0','product zero anchor and absolute phase') + zero_anchors+=1 + N.need(len(products)==1012*59==59708,'complete distinct left-image support') + # At tensor degree n-1, products of separating linear forms give one dual + # functional per projective point. The common zero anchor lifts to all + # larger degrees. This is a symbolic theorem, not a huge numerical Gram. + threshold=len(products)-1 + return { + 'schema':'physical-zqy-fixed-abi-left-images/v1', + 'status':'PASS_FIXED_Z_ABI_LEFT_IMAGES_EVENTUAL_WIDTH_NO_NEW_KAPPA', + 'input_sha256':{name:digest for name,(rel,digest)in INPUTS.items()}, + 'provider_full_frame_versions':len(versions), + 'base_exact_rank_from_primary':546,'base_exact_non_Y_projection_rank_from_primary':546, + 'base_operator_count':len(base_operators),'base_operator_set_sha256':digest_operators(base_operators), + 'port_normalizers':112,'mode_normalizers':8,'seed_normalizer_inverse_additions':0, + 'seed_exact_F9_signed_kernel_address_checks':anchor_checks, + 'physical_to_logical_left_transport':'F9^-1 T F9 = T, including absolute phase; all seeds centralize the full nine-axis Gaussian and so do their products.', + 'raw_left_family_size':len(raw),'distinct_left_maps':len(family), + 'left_map_set_sha256':digest_operators(seen), + 'distinct_left_products':len(products),'left_support_collision_count':0, + 'left_product_set_sha256':digest_operators(products), + 'product_exact_zero_anchor_checks':zero_anchors, + 'tensor_independence_degree_bound':threshold, + 'coefficient_scope':'arbitrary complex scalar coefficients, allowed to depend on width', + 'conclusion':'For every f>=59707 the declared finite left-image span has no nonzero pure-Y vector. Thus it cannot supply the nonzero eight-mode b=ZQY by an exact all-width identity within this fixed family.', + 'scope':'Provider-backward whole history; independently chosen left images T in {I,Kp_i,Km_a,Km_a^-1 Kp_i}. No unrestricted products of these generators, no arbitrary monomial left closure, no changed producer or extra correlated data; no small-width nonmembership claim.', + 'target_or_paid_profile_change':False,'new_kappa':False, + 'base_rank_obligation':'The registered primary verify.py must pass; this command authenticates/replays the source and consumes its exact 546/546 certificate, rather than rerunning the large exact elimination.'} + + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--write',action='store_true');args=parser.parse_args() + result=calculate();encoded=json.dumps(result,indent=2,sort_keys=True)+'\n' + if args.write:(HERE/'ABI-CLOSURE.json').write_text(encoded) + else:N.need(json.loads((HERE/'ABI-CLOSURE.json').read_text())==result,'fixed ABI receipt differs') + print(json.dumps(result,sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/physical-zqy-scalar-span/finite.py b/research/physical-zqy-scalar-span/finite.py new file mode 100644 index 0000000000..39751c2422 --- /dev/null +++ b/research/physical-zqy-scalar-span/finite.py @@ -0,0 +1,105 @@ +"""Finite Gaussian-integer column certificates; no modular nonmembership shortcut. + +A nonzero modular minor is used only as a rank LOWER bound. Rational span +UPPER bounds and an exact operator relation are supplied separately. +Apache-2.0; substantial OpenAI Codex assistance. +""" +from fractions import Fraction as F +import monomial as M + +PRIME=998244353 +IMAG=911660635 + +def need(ok,why): + if not ok:raise ValueError(why) + +class Span: + def __init__(self):self.piv={} + def add(self,v): + v=dict(v) + while v: + k=min(v) + if k not in self.piv: + q=pow(v[k],PRIME-2,PRIME);self.piv[k]={j:x*q%PRIME for j,x in v.items()};return True + q=v[k] + for j,x in self.piv[k].items(): + z=(v.get(j,0)-q*x)%PRIME + if z:v[j]=z + else:v.pop(j,None) + return False + +RELATION={157:1,51:1,156:-1,49:-1} +SUBSTITUTION={157:{156:1,49:1,51:-1}} + +def relation_zero(operators,relation): + out={} + for j,q in relation.items(): + for x,v in enumerate(M.decode(operators[j])): + a,b=((q,0),(0,q),(-q,0),(0,-q))[v%4];k=x,v//4 + c,d=out.get(k,(0,0));c+=a;d+=b + if c or d:out[k]=c,d + else:out.pop(k,None) + return not out + +def operator_rank(operators): + need(IMAG*IMAG%PRIME==PRIME-1,'Gaussian prime embedding') + need(len(operators)==len(set(operators))==215,'literal operator inventory') + need(relation_zero(operators,RELATION),'exact four-term physical relation') + bad=list(operators);values=M.decode(bad[157]);values[0]^=1;bad[157]=values.tobytes() + need(not relation_zero(bad,RELATION),'wrong absolute phase must break relation') + s=Span() + for op in operators:s.add({x*512+a//4:pow(IMAG,a%4,PRIME) for x,a in enumerate(M.decode(op))}) + need(len(s.piv)==214,'width-one independent 214-minor') + return {'operators':215,'width_one_exact_rank':214,'rank_lower_prime':PRIME,'sqrt_minus_one':IMAG,'exact_relation':{str(k):v for k,v in RELATION.items()},'wrong_phase_control':True} + +def physical_projection_rank(versions): + index={};classes={};vspan=Span();projection=Span() + for row in versions: + v={} + for (role,op),q in row.items(): + q=q.numerator*pow(q.denominator,PRIME-2,PRIME)%PRIME + for j,a in SUBSTITUTION.get(op,{op:1}).items(): + key=role,j;k=index.setdefault(key,len(index));classes[k]=(role[0]=='L' and 112<=role[1]<224);z=(v.get(k,0)+q*a)%PRIME + if z:v[k]=z + else:v.pop(k,None) + vspan.add(v) + projection.add({k:q for k,q in v.items() if not classes[k]}) + # Coordinate injection is an actual pure-y operator, with the identity map. + k=index.setdefault((('L',112),0),len(index));before=len(vspan.piv) + need(vspan.add({k:1}),'physical pure-y positive control') + return {'rank_lower_V':before,'rank_lower_non_Y_projection':len(projection.piv),'positive_control_rank':len(vspan.piv)} + +def matrix_rank_det(rows,prime): + a=[r[:] for r in rows];n=len(a);r=0;det=1 + for c in range(n): + pivot=next((k for k in range(r,n) if a[k][c]),None) + if pivot is None:continue + if pivot!=r:a[pivot],a[r]=a[r],a[pivot];det=-det + z=a[r][c];det=det*z%prime;q=pow(z,prime-2,prime);a[r]=[x*q%prime for x in a[r]] + for k in range(r+1,n): + z=a[k][c] + if z:a[k]=[(x-z*y)%prime for x,y in zip(a[k],a[r])] + r+=1 + return r,det%prime if r==n else 0 + +def tensor_square(operators): + prime=1000000009;imag=569522298 + need(imag*imag%prime==prime-1,'second Gaussian prime embedding') + ops=[M.decode(x) for x in operators];need(all(x[0]==0 for x in ops),'zero-vector phase anchor for every map') + gram=[] + for a in ops: + row=[] + for b in ops: + re=im=0 + for x,y in zip(a,b): + if x//4!=y//4:continue + ph=(y-x)%4 + if ph==0:re+=1 + elif ph==1:im+=1 + elif ph==2:re-=1 + else:im-=1 + row.append(pow((re+imag*im)%prime,2,prime)) + gram.append(row) + rank,det=matrix_rank_det(gram,prime) + need(rank==215 and det==298401053,'tensor-square nonzero Gaussian-integer Gram determinant') + return {'width':2,'rank':rank,'prime':prime,'sqrt_minus_one':imag,'determinant_mod_prime':det,'all_zero_anchors_one':True} diff --git a/research/physical-zqy-scalar-span/independent_width1.py b/research/physical-zqy-scalar-span/independent_width1.py new file mode 100644 index 0000000000..242998a7f3 --- /dev/null +++ b/research/physical-zqy-scalar-span/independent_width1.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Independent exact Q(i) physical width-one quotient and version-span audit. + +THU New Media Research Center; substantial OpenAI Codex assistance. Apache-2.0. +No finite-field rank or nonmembership routine is called. Distinct physical +operator matrices are expanded in their literal signed columns. A checked +coordinate phase gauge makes the operator matrix rational, so exact rational +row elimination proves its rank over Q(i), and hence over C. The single real +kernel relation is then used for exact version-span elimination. +""" +from pathlib import Path +from hashlib import sha256 +from fractions import Fraction as F +from collections import Counter +import argparse,json,sys,time +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import native as source +source.source=source.read("source") +source.provider=source.read("provider") +source.canon=source.source["canonical"] +source.initialize(source.canon) +source.actual_replay=source.native_replay +import monomial as mon + +def need(ok,message): + if not ok:raise ValueError(message) + +class RationalEchelon: + """Independent sparse fraction row elimination; ordered leading pivots.""" + def __init__(self,track=False): + self.rows={};self.certificates={};self.track=track;self.max_numerator_bits=0;self.max_denominator_bits=0 + def reduce(self,row,certificate=None): + row={k:F(v) for k,v in row.items() if v};certificate=dict(certificate or {}) + while row: + pivot=min(row) + if pivot not in self.rows:return row,certificate + multiple=row[pivot] + for k,value in self.rows[pivot].items(): + z=row.get(k,F(0))-multiple*value + if z:row[k]=z + else:row.pop(k,None) + if self.track: + for k,value in self.certificates[pivot].items(): + z=certificate.get(k,F(0))-multiple*value + if z:certificate[k]=z + else:certificate.pop(k,None) + return row,certificate + def insert(self,row,label=None): + v,c=self.reduce(row,{label:F(1)} if self.track else None) + if not v:return False,c + pivot=min(v);den=v[pivot];v={k:x/den for k,x in v.items()} + self.rows[pivot]=v + if self.track:self.certificates[pivot]={k:x/den for k,x in c.items()} + self.max_numerator_bits=max(self.max_numerator_bits,max(abs(x.numerator).bit_length() for x in v.values())) + self.max_denominator_bits=max(self.max_denominator_bits,max(x.denominator.bit_length() for x in v.values())) + return True,c + def copy(self): + out=RationalEchelon(self.track);out.rows={p:r.copy() for p,r in self.rows.items()};out.certificates={p:r.copy() for p,r in self.certificates.items()} + out.max_numerator_bits=self.max_numerator_bits;out.max_denominator_bits=self.max_denominator_bits;return out + + +def materialize(): + cases=[] + for name,program,backward in [('provider-backward',source.provider['word'],True),('source-backward',source.source['programs']['backward'],True),('source-forward',source.source['programs']['forward'],False)]: + rows,*_=source.actual_replay(source.canon,program,backward) + cases.append((name,rows));print('REPLAY',name,len(rows),len(source.operators),flush=True) + need(len(source.operators)==215,'Frozen replay must generate 215 actual operators') + return cases + + +def physical_operator_rank(): + tables=[tuple(mon.decode(x)) for x in source.operators] + # For each literal matrix coordinate all nonzero entries must be a real + # multiple of one fixed Gaussian phase. Dividing that coordinate by i^p + # is an invertible complex coordinate change; it is a proof device, never + # a claimed physical instruction or an owner-code tensorization. + gauge={};counts=Counter() + for table in tables: + need(len(table)==512 and len({x//4 for x in table})==512,'Literal monomial bijection') + for col,value in enumerate(table): + row,phase=divmod(value,4);key=512*col+row;parity=phase%2;counts[phase]+=1 + if key not in gauge:gauge[key]=parity + need(gauge[key]==parity,'Common coordinate phase gauge must be consistent') + span=RationalEchelon(track=True);relations=[] + for n,table in enumerate(tables): + vector={} + for col,value in enumerate(table): + row,phase=divmod(value,4);key=512*col+row;difference=(phase-gauge[key])%4 + need(difference in (0,2),'Exact rational coordinate after gauge') + vector[key]=F(1 if difference==0 else -1) + independent,certificate=span.insert(vector,n) + if not independent: + need(certificate,'Nontrivial exact kernel certificate');relations.append(certificate) + if n%50==0:print('EXACT_OPERATOR',n,len(span.rows),flush=True) + need(len(span.rows)==214 and len(relations)==1,'Exact Q(i) operator rank214, kernel dimension1') + expected={157:F(1),51:F(1),156:F(-1),49:F(-1)} + certificate=relations[0];last=max(certificate);normal={k:v/certificate[last] for k,v in certificate.items()} + need(normal==expected,'Independently recovered exact four-term real relation') + # Verify it again on un-gauged Gaussian-integer entries, without elimination. + def residual(relation,mutation=None): + out={} + for n,c in relation.items(): + for col,value in enumerate(tables[n]): + row,phase=divmod(value,4) + if mutation is not None and n==mutation[0] and col==mutation[1]:phase=(phase+mutation[2])%4 + a,b=[(c,F(0)),(F(0),c),(-c,F(0)),(F(0),-c)][phase];key=512*col+row;u,v=out.get(key,(F(0),F(0)));u+=a;v+=b + if u or v:out[key]=u,v + else:out.pop(key,None) + return out + need(not residual(normal),'Exact relation on original complex physical entries') + mutation=(157,1,1);wrong=residual(normal,mutation) + need(wrong,'Wrong complex phase at one nonzero column must break relation') + # This control preserves the permutation and the zero-address phase anchor. + # It must fail the checked rational-gauge shortcut as well. + row,phase=divmod(tables[157][1],4);coordinate=512+row + need(gauge[coordinate]!=(phase+1)%2,'Wrong phase destroys checked common gauge') + # The phase mutation changes the gauged operator by a nonzero complex + # multiple of this unit coordinate. Prove that coordinate is outside the + # old rational span, hence outside its Q(i) extension. The mutated family + # has rank 215: this is a rank-sensitive phase control, not only a checksum. + unit_remainder,_=span.reduce({coordinate:F(1)}) + need(unit_remainder,'Wrong-phase mutation must increase the exact physical rank') + relation_encoded={str(k):str(v) for k,v in sorted(normal.items())} + operator_data={'operator_count':215,'exact_rank_over_Q_i':214,'exact_rank_over_C':214,'exact_kernel_dimension':1,'kernel_relation':relation_encoded,'coordinate_phase_gauge':'Every fixed physical matrix coordinate has one shared phase parity, making all 215 columns rational after invertible coordinate scaling. Rational rank is unchanged under scalar extension Q -> Q(i) -> C.','distinct_physical_matrix_coordinates':len(gauge),'phase_exponent_counts':dict(sorted(counts.items())),'exact_pivot_coordinates':[[k//512,k%512] for k in span.rows],'basis_numerator_bits':span.max_numerator_bits,'basis_denominator_bits':span.max_denominator_bits,'wrong_phase_control':{'operator':157,'input_column':1,'phase_increment_mod4':1,'permutation_preserved':True,'zero_column_phase_anchor_preserved':True,'exact_relation_rejected':True,'rational_gauge_rejected':True,'exact_mutated_rank_over_Q_i':215,'unit_coordinate_outside_original_span':True,'nonzero_residual_coordinates':len(wrong)}} + return normal,operator_data + + +def quotient_row(row,relation,index): + pivot=max(relation);coefficient=relation[pivot];substitution={j:-c/coefficient for j,c in relation.items() if j!=pivot};out={} + for (role,op),c in row.items(): + terms=substitution if op==pivot else {op:F(1)} + for j,d in terms.items(): + key=(role,j);index.setdefault(key,len(index));z=out.get(key,F(0))+c*d + if z:out[key]=z + else:out.pop(key,None) + return {index[k]:v for k,v in out.items()} + + +def version_rank(name,versions,relation): + started=time.monotonic();index={};V=RationalEchelon();N=RationalEchelon() + for n,row in enumerate(versions): + vector=quotient_row(row,relation,index) + reverse={v:k for k,v in index.items()} + non_y={k:c for k,c in vector.items() if not (reverse[k][0][0]=='L' and 112<=reverse[k][0][1]<224)} + V.insert(vector);N.insert(non_y) + if n%1000==0:print('EXACT_QUOTIENT',name,n,len(V.rows),len(N.rows),round(time.monotonic()-started,3),flush=True) + rank_V,rank_N=len(V.rows),len(N.rows) + expected=546 if name=='provider-backward' else 554 + need(rank_V==rank_N==expected,'Exact physical quotient has no pure-Y direction') + # Add one arbitrary original Y input. It has zero non-Y projection and + # cannot already lie in V when rank(V)=rank(non-Y projection). + y_key=(('L',112),0);j=index.setdefault(y_key,len(index));injected=V.copy();changed,_=injected.insert({j:F(1)}) + need(changed and len(injected.rows)==rank_V+1,'Positive pure-Y injection increases exact rank') + need(len(injected.rows)-rank_N==1,'Injected quotient intersection dimension is exactly one') + return {'name':name,'full_frame_versions':len(versions),'quotient_coordinates':len(index),'exact_rank_V_over_Q_i':rank_V,'exact_non_Y_projection_rank_over_Q_i':rank_N,'exact_pure_Y_any_physical_operator_dimension':rank_V-rank_N,'all_scalar_coefficients_after_operator_quotient_real_rational':True,'positive_pure_Y_identity_injection':{'rank_increase':1,'pure_Y_dimension_after_injection':1},'max_basis_numerator_bits':max(V.max_numerator_bits,N.max_numerator_bits),'max_basis_denominator_bits':max(V.max_denominator_bits,N.max_denominator_bits),'seconds':time.monotonic()-started} + + +def main(write=False): + started=time.monotonic();cases=materialize();relation,operators=physical_operator_rank();checks=[] + for name,versions in cases: + row=version_rank(name,versions,relation);checks.append(row);print('CHECK',json.dumps(row,sort_keys=True),flush=True) + pins={name:sha256((source.ROOT/rel).read_bytes()).hexdigest() for name,(rel,expected) in source.INPUTS.items()} + result={'status':'PASS_INDEPENDENT_EXACT_WIDTH1_PHYSICAL_QUOTIENT','arithmetic':'Exact Fraction arithmetic; no finite-field rank or nonmembership shortcut. A checked coordinate phase gauge proves the Q(i) physical-operator rank using rational row elimination.','operators':operators,'checks':checks,'source_sha256':pins,'implementation_sha256':{x:sha256((HERE/x).read_bytes()).hexdigest() for x in ('native.py','monomial.py')},'seconds':time.monotonic()-started,'scope':'Width-one scalar span of all retained full-frame versions under the source replay. All actual signed-monomial matrix relations are quotiented exactly. No closure under arbitrary free left transports, modified native history, supplied correlated observations, all-width implementation, or new kappa is asserted.'} + result['independent_script_sha256']=sha256(Path(__file__).read_bytes()).hexdigest() + if write:(HERE/'INDEPENDENT-WIDTH1.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + print('PASS_INDEPENDENT_EXACT_WIDTH1_PHYSICAL_QUOTIENT',round(result['seconds'],3),flush=True) + return result +if __name__=='__main__': + ap=argparse.ArgumentParser();ap.add_argument('--write',action='store_true');args=ap.parse_args();main(args.write) diff --git a/research/physical-zqy-scalar-span/monomial.py b/research/physical-zqy-scalar-span/monomial.py new file mode 100644 index 0000000000..1a44838084 --- /dev/null +++ b/research/physical-zqy-scalar-span/monomial.py @@ -0,0 +1,59 @@ +"""Exact monomial column algebra; source K_G convention from native phase audit.""" +from functools import lru_cache +from array import array +N=512 +IDENTITY=array('H',(4*x for x in range(N))).tobytes() + +def decode(value): + a=array('H');a.frombytes(value);return a + +def linear(columns,x): + answer=0 + for j,c in enumerate(columns): + if x>>j&1:answer^=c + return answer + +def inverse_columns(columns): + pivots={} + for j,value in enumerate(columns): + coefficient=1<>pivot&1:value^=pivots[pivot][0];coefficient^=pivots[pivot][1] + if not value:raise ValueError('singular native map') + pivots[value.bit_length()-1]=value,coefficient + result=[] + for j in range(9): + value,coefficient=1<>pivot&1:value^=pivots[pivot][0];coefficient^=pivots[pivot][1] + if value:raise ValueError('inverse construction') + result.append(coefficient) + return result + +def native(columns): + # K_G|x>=i^q(Gx)|Gx>, Q=I+G^-T G^-1. Same retained PR2226 phase convention. + inv=inverse_columns(columns) + tr=[sum(((inv[j]>>i)&1)<>j&1)*(y>>j&1) for j in range(9)) + phase+=2*sum((quadratic[j]>>i&1)*(y>>i&1)*(y>>j&1) for i in range(9) for j in range(i+1,9)) + result.append(4*y+phase%4) + return array('H',result).tobytes() + +@lru_cache(None) +def multiply(left,right): + l,r=decode(left),decode(right) + return array('H',(4*(l[v//4]//4)+(l[v//4]%4+v%4)%4 for v in r)).tobytes() + +@lru_cache(None) +def conjugate(op): + return array('H',(4*(v//4)+(-v%4) for v in decode(op))).tobytes() + +@lru_cache(None) +def inverse(op): + a=decode(op);result=[0]*N + for x,v in enumerate(a):result[v//4]=4*x+(-v%4) + return array('H',result).tobytes() diff --git a/research/physical-zqy-scalar-span/native.py b/research/physical-zqy-scalar-span/native.py new file mode 100644 index 0000000000..0784aa84b7 --- /dev/null +++ b/research/physical-zqy-scalar-span/native.py @@ -0,0 +1,116 @@ +"""Actual signed-native row interpreter. + +Event/ownership/version semantics adapted from Mark (Matarener), #5427, +389578f2d3ef075495ce76f08100ac50e18f7d40. Native words by Dillon, +Cao Yifan and the retained Cinna Davis/zxv lineage. The actual monomial +canonicalization and all-width certificate are new. Apache-2.0; substantial +OpenAI Codex assistance for THU New Media Research Center (@thu-nmrc). +""" +from fractions import Fraction as Fr +from pathlib import Path +from hashlib import sha256 +import gzip,json +import monomial as M +ROOT=Path(__file__).resolve().parents[2] +INPUTS={ + 'source':('research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz','7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05'), + 'provider':('research/native-rank8-helper-provider/WORD.json.gz','7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc')} +def need(ok,message): + if not ok:raise ValueError(message) +def read(name): + path,digest=INPUTS[name];raw=(ROOT/path).read_bytes();need(sha256(raw).hexdigest()==digest,'source bytes '+path) + return json.loads(gzip.decompress(raw)) +operators=[M.IDENTITY];lookup={M.IDENTITY:0};products={};base={};back={} +def intern(op): + if op not in lookup:lookup[op]=len(operators);operators.append(op) + return lookup[op] +def initialize(canon): + need(len(operators)==1,'one initialization') + base.update({w['op']:intern(M.native(w['G_columns'])) for w in canon['warps']}) + base.update({-k:intern(M.inverse(operators[v])) for k,v in list(base.items())}) + back.update({k:intern(M.conjugate(operators[v])) for k,v in base.items()}) +def left_row(row,op,backward): + left=(back if backward else base)[op];out={} + for (role,right),q in row.items(): + pair=left,right + if pair not in products:products[pair]=intern(M.multiply(operators[left],operators[right])) + key=role,products[pair];z=out.get(key,0)+q + if z:out[key]=z + else:out.pop(key,None) + return out + +def span_set(basis): + out = {0} + for v in basis: + out |= {x ^ v for x in tuple(out)} + need(len(out) == 1 << len(basis), 'independent frame basis') + return out + +def native_replay(canon, program, backward): + """Exact rows (convention of research/kappa-owned-relation-20261023/native.py). + Returns the list of distinct full-frame versions, final rows and final frames.""" + spaces = [span_set(b) for b in canon['frames']] + full = {i for i, s in enumerate(spaces) if len(s) == 512} + need(len(full) == 1, 'one full frame') + rows = {('L', i): {(('L', i), 0): Fr(1)} for i in range(632)} + frames = {('L', i): canon['start'][i] for i in range(632)} + + def get(r): + if r not in rows: + rows[r] = {(r, 0): Fr(1)} + frames[r] = None + return rows[r] + + seen, versions = set(), [] + for e in program: + k, touched = e[0], None + if k == 'scalar': + g, frame = e[1], e[2] + dst = tuple(g[1]); get(dst); touched = dst + if g[0] == 'clear': + rows[dst] = {}; frames[dst] = frame + elif g[0] == 'copy': + src = tuple(g[2]); need(frames[src] == frame, 'copy frame') + rows[dst] = dict(get(src)); frames[dst] = frame + elif g[0] == 'add': + src = tuple(g[2]); need(frames[src] == frame == frames[dst], 'same-frame ADD') + q = Fr(g[3], g[4]); r = rows[dst] + for key, v in get(src).items(): + nv = r.get(key, 0) + q * v + if nv: + r[key] = nv + else: + r.pop(key, None) + elif g[0] == 'scale': + q = Fr(g[2], g[3]); rows[dst] = {a: q * v for a, v in rows[dst].items()} + else: + raise AssertionError('unknown scalar ' + repr(g[0])) + elif k == 'warp': + _, role, op, old, new = e + dst = tuple(role); get(dst); touched = dst + need(frames[dst] == old, 'warp input frame') + rows[dst] = left_row(rows[dst], op, backward) + frames[dst] = new + elif k == 'climb': + dst = ('L', e[2]); need(frames[dst] == e[3], 'climb input frame') + frames[dst] = e[4]; touched = dst + elif k == 'center': + dst = ('C', e[1]); get(dst); frames[dst] = e[3]; touched = dst + elif k == 'zero_retag': + dst = ('L', e[1]); need(frames[dst] == e[2] and not rows[dst], 'zero retag on a zero row') + frames[dst] = e[3]; touched = dst + else: + need(k in ('phase', 'adapter'), 'unknown event ' + repr(k)) + if touched is not None and frames[touched] in full and rows[touched]: + key = frozenset(rows[touched].items()) + if key not in seen: + seen.add(key); versions.append(dict(rows[touched])) + return versions, rows, frames, full + +def role_class(key): + r = key[0] + if r[0] == 'L' and r[1] < 112: + return 'x' + if r[0] == 'L' and r[1] < 224: + return 'y' + return 'h' diff --git a/research/physical-zqy-scalar-span/phase_audit.py b/research/physical-zqy-scalar-span/phase_audit.py new file mode 100644 index 0000000000..692ec5813d --- /dev/null +++ b/research/physical-zqy-scalar-span/phase_audit.py @@ -0,0 +1,153 @@ +#!/usr/bin/env python3 +"""Independent absolute-phase audit of all actual native monomial variants. + +Native K_G conventions retain PR2226 and Cao Yifan/intqwq's PR4610 source. +The signed Clifford tableau/compiler and its absolute-phase anchor retain the +PR531/T74 native lineage. The conjugate backward convention retains Dugongue, +Cinna Davis and the source phase audit. The observer question retains zxv's +PR5419 and Mark/Matarener's PR5427. This checker corroborates the independently +implemented direct-Gram monomial tables; it does not prove an observer exists. + +Prepared for THU New Media Research Center (@thu-nmrc), with substantial +OpenAI Codex assistance. Apache-2.0. Default operation writes no files. +""" +from pathlib import Path +from hashlib import sha256 +import importlib.util +import gzip +import json +import sys +sys.dont_write_bytecode = True + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ENGINE = ('research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py', + '2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962') +SOURCE = ('research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz', + '7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05') + + +def need(ok, reason): + if not ok: + raise ValueError(reason) + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def run(): + for relative, expected in (ENGINE, SOURCE): + need(sha256((ROOT/relative).read_bytes()).hexdigest() == expected, + 'phase-audit source bytes changed: '+relative) + ce = load('physical_zqy_frozen_clifford_phase_audit', ROOT/ENGINE[0]) + candidate = load('physical_zqy_direct_gram_phase_audit', HERE/'monomial.py') + canon = json.loads(gzip.decompress((ROOT/SOURCE[0]).read_bytes()))['canonical'] + need(len(canon['warps']) == 72 and + {entry['op'] for entry in canon['warps']} == set(range(1, 73)), + 'all 72 pinned native operators') + + def reference(columns): + # Retained phase-audit Kop convention, using frozen Clifford primitives. + # Op.then is chronological: first perm(G), then diag(I+G^-T G^-1). + rows = ce.transpose(tuple(columns), 9) + inverse_rows = ce.inv(rows, 9) + inverse_columns = ce.transpose(inverse_rows, 9) + quadratic = tuple((1 << i) ^ sum(ce.parity(u & v) << j + for j, v in enumerate(inverse_columns)) + for i, u in enumerate(inverse_columns)) + return ce.perm(9, rows).then(ce.diag(9, quadratic)) + + def conjugate(operator): + # Entrywise conjugation, preserving chronological circuit order. + # K_G and its adjoint use only P/D here; the explicit gate cases also + # retain the source convention for ordinary affine/phase gates. + out = ce.ident(operator.n) + for gate in operator.circuit: + kind = gate[0] + if kind == 'P': + part = ce.perm(operator.n, gate[1]) + elif kind == 'D': + part = ce.diag(operator.n, gate[1], tuple(-x % 4 for x in gate[2])) + elif kind == 'X': + part = ce.xgate(operator.n, gate[1]) + elif kind == 'C': + part = ce.cgate(operator.n, gate[1], -gate[2]) + else: + need(kind == 'phase', 'recognized frozen Clifford primitive') + part = ce.Op(operator.n, ce.identity(operator.n), [('phase', -gate[1] % 4)]) + out = out.then(part) + return out + + def checked_columns(operator): + # The frozen compiler derives a monomial from the signed tableau. + # An exact Gaussian-integer zero column fixes the remaining phase. + need(ce.rank([x for x, z, p in operator.tab[9:]]) == 0, 'reference monomial') + compiled, recipe = ce.monomial(operator) + need(compiled.tab == operator.tab and + compiled.zero_state() == operator.zero_state(), + 'frozen signed tableau and absolute phase') + result = [] + for address in range(512): + out = ce.mv(tuple(recipe['matrix_rows']), address) ^ recipe['offset'] + exponent = (ce.qvalue(tuple(recipe['quadratic_rows']), + tuple(recipe['linear_Z4']), address, 9) + recipe['phase']) % 4 + result.append(4*out+exponent) + return result + + actual, refs = {}, {} + individual_columns = backward_differences = 0 + for entry in canon['warps']: + op = entry['op'] + forward_ref = reference(entry['G_columns']) + forward_table = candidate.native(entry['G_columns']) + for sign in (1, -1): + ref = forward_ref if sign == 1 else forward_ref.adjoint() + table = forward_table if sign == 1 else candidate.inverse(forward_table) + for backward in (False, True): + tested = candidate.conjugate(table) if backward else table + expected = conjugate(ref) if backward else ref + need(list(candidate.decode(tested)) == checked_columns(expected), + 'frozen Clifford mismatch for op/sign/backward '+str((op, sign, backward))) + need(candidate.decode(tested)[0] == 0, 'zero-address phase gauge') + actual[op, sign, backward], refs[op, sign, backward] = tested, expected + individual_columns += 512 + backward_differences += int(candidate.conjugate(table) != table) + need(individual_columns == 147456, 'complete individual-column census') + need(backward_differences == 140, 'conjugate-direction discriminating control') + phase_control = refs[1, 1, False].then( + ce.Op(9, ce.identity(9), [('phase', 1)])) + need(phase_control.tab == refs[1, 1, False].tab and + phase_control.zero_state() != refs[1, 1, False].zero_state(), + 'a tableau-invisible global phase must change the absolute anchor') + + # Check multiplication order against frozen Op.then, including complex + # phases and inverse signs, independently of the candidate inverse law. + product_columns = 0 + for op in range(1, 73): + left = (op, -1 if op % 2 else 1, bool(op % 3)) + right = (1 + op % 72, 1 if op % 2 else -1, bool(op % 5)) + table = candidate.multiply(actual[left], actual[right]) + expected = refs[right].then(refs[left]) + need(list(candidate.decode(table)) == checked_columns(expected), 'ordered product mismatch') + product_columns += 512 + need(product_columns == 36864, 'complete ordered-product column census') + return dict(status='PASS_INDEPENDENT_FROZEN_CLIFFORD_NATIVE_MAP_AUDIT', + native_operators=72, signs=2, directions=2, + exact_individual_columns=individual_columns, + exact_ordered_product_columns=product_columns, + backward_sign_cases_differing_from_forward=backward_differences, + tableau_invisible_phase_control=True, + every_reference_fixes_zero_with_zero_phase=True, + frozen_engine_sha256=ENGINE[1], source_word_sha256=SOURCE[1], + evaluator='frozen signed Clifford tableau, monomial compiler, exact Gaussian-integer phase anchor', + no_formal_membership_rerun=True, observation_existence_proved=False, + runtime_file_writes=0) + + +if __name__ == '__main__': + print(json.dumps(run(), sort_keys=True)) diff --git a/research/physical-zqy-scalar-span/rational.py b/research/physical-zqy-scalar-span/rational.py new file mode 100644 index 0000000000..52d912c471 --- /dev/null +++ b/research/physical-zqy-scalar-span/rational.py @@ -0,0 +1,17 @@ +"""Exact rational echelon rank; assertions are not used as checks.""" +from fractions import Fraction as F +class ExactSpan: + def __init__(self):self.piv={};self.max_num=0;self.max_den=0 + def add(self,v): + v=dict(v) + while v: + k=min(v) + if k not in self.piv: + q=v[k];v={j:x/q for j,x in v.items()};self.piv[k]=v + self.max_num=max(self.max_num,max(abs(x.numerator).bit_length() for x in v.values()));self.max_den=max(self.max_den,max(x.denominator.bit_length() for x in v.values()));return True + q=v[k] + for j,x in self.piv[k].items(): + z=v.get(j,F(0))-q*x + if z:v[j]=z + else:v.pop(j,None) + return False diff --git a/research/physical-zqy-scalar-span/verify.py b/research/physical-zqy-scalar-span/verify.py new file mode 100644 index 0000000000..4711ba0f4c --- /dev/null +++ b/research/physical-zqy-scalar-span/verify.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Source-bound, all-width physical scalar-span audit. Default replay is read-only. + +THU New Media Research Center (@thu-nmrc); substantial OpenAI Codex assistance. +Apache-2.0. See PROOF.md for the quantified theorem and its restricted grammar. +""" +from pathlib import Path +from fractions import Fraction as F +from hashlib import sha256 +import argparse,json,sys,time +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import native as N +import monomial as M +from rational import ExactSpan +import finite as C + + +def authenticate(): + pins=json.loads((HERE/'SOURCES.json').read_text()) + for row in pins['files']: + if row['usage']!='input':continue + raw=(N.ROOT/row['path']).read_bytes() + N.need(sha256(raw).hexdigest()==row['sha256'],'input hash '+row['path']) + return pins + + +def scalar_ranks(name,versions): + index={};V=ExactSpan();projection=ExactSpan() + for row in versions: + v={index.setdefault(k,len(index)):q for k,q in row.items()} + non_y={index[k]:q for k,q in row.items() if N.role_class(k)!='y'} + V.add(v);projection.add(non_y) + rank=len(V.piv) + injected=index.setdefault((('L',112),0),len(index)) + N.need(V.add({injected:F(1)}),'positive pure-y injection') + N.need(rank==len(projection.piv),'all-width group-coordinate projection injective') + return {'name':name,'full_frame_versions':len(versions),'group_coordinate_count':len(index), + 'exact_group_rank':rank,'exact_group_non_Y_projection_rank':len(projection.piv), + 'positive_injection_rank':len(V.piv),'max_numerator_bits':V.max_num,'max_denominator_bits':V.max_den} + + +def calculate(): + authenticate();source=N.read('source');provider=N.read('provider');canon=source['canonical'];N.initialize(canon) + case_input=[('provider-backward',provider['word'],True,4891,546), + ('source-backward',source['programs']['backward'],True,5019,554), + ('source-forward',source['programs']['forward'],False,4968,554)] + cases=[];retained=[] + for name,program,backward,count,rank in case_input: + versions,rows,frames,full=N.native_replay(canon,program,backward) + N.need(len(versions)==count,'complete frozen full-frame version count '+name) + result=scalar_ranks(name,versions);N.need(result['exact_group_rank']==rank,'exact frozen span rank '+name) + cases.append(result);retained.append(versions) + print('PASS_EXACT_GROUP_SPAN',name,count,rank,flush=True) + # No phase is silently converted into an ordinary scalar. All products retain literal columns. + N.need(len(N.operators)==215 and all(M.decode(op)[0]==0 for op in N.operators),'complete zero-anchored signed operator set') + one=C.operator_rank(N.operators) + for result,versions in zip(cases,retained): + physical=C.physical_projection_rank(versions) + N.need(physical['rank_lower_non_Y_projection']==result['exact_group_rank'],'width-one projection lower bound equals exact upper bound') + N.need(physical['rank_lower_V']==result['exact_group_rank'],'width-one complete rank agrees') + N.need(physical['positive_control_rank']==result['exact_group_rank']+1,'width-one positive control') + result['width_one_modular_rank_bounds']=physical + two=C.tensor_square(N.operators) + return {'schema':'physical-zqy-scalar-span/v1', + 'status':'PASS_ALL_WIDTH_PHYSICAL_NATIVE_SCALAR_SPAN_NO_NEW_KAPPA', + 'source_payload_sha256':sha256(__import__('gzip').decompress((N.ROOT/N.INPUTS['source'][0]).read_bytes())).hexdigest(), + 'cases':cases,'operator_certificate':one,'tensor_square_gram':two, + 'widths':'all positive integers; coefficients may depend on width and be complex', + 'scope':'Scalar linear combinations of all full-frame versions of these frozen native words; excludes arbitrary independently chosen free left maps and changed words.', + 'productive_or_paid_profile_change':False,'new_kappa':False, + 'controls':['injected pure-y identity raises rank in every case','wrong absolute phase breaks exact four-term relation']} + + +def main(): + parser=argparse.ArgumentParser();parser.add_argument('--write',action='store_true');args=parser.parse_args() + start=time.monotonic();result=calculate();encoded=json.dumps(result,indent=2,sort_keys=True)+'\n' + if args.write:(HERE/'RESULT.json').write_text(encoded) + else:N.need(json.loads((HERE/'RESULT.json').read_text())==result,'committed result differs from fresh computation') + print(result['status'], 'seconds',round(time.monotonic()-start,3),flush=True) +if __name__=='__main__':main() From 7895420fa5713aaabd035954ba215d0c721c8022 Mon Sep 17 00:00:00 2001 From: thu-nmrc Date: Sun, 25 Oct 2026 04:34:49 +0800 Subject: [PATCH 2/3] Prove explicit all-width input kernels for complete native histories --- .../FORMAL-KERNEL.json | 34 + .../INDEPENDENT-KERNEL-AUDIT.json | 83 + .../INTERNAL-REVIEW.md | 37 +- .../physical-zqy-scalar-span/KERNEL-PROOF.md | 63 + .../KERNEL-RESULT.json | 85 + research/physical-zqy-scalar-span/KERNEL.json | 1763 +++++++++++++++++ research/physical-zqy-scalar-span/README.md | 45 +- research/physical-zqy-scalar-span/TASK.json | 14 +- .../physical-zqy-scalar-span/VALIDATION.md | 113 +- research/physical-zqy-scalar-span/VERIFY.json | 53 +- .../physical-zqy-scalar-span/formal_kernel.py | 98 + .../independent_kernel.py | 184 ++ .../physical-zqy-scalar-span/verify_kernel.py | 217 ++ 13 files changed, 2693 insertions(+), 96 deletions(-) create mode 100644 research/physical-zqy-scalar-span/FORMAL-KERNEL.json create mode 100644 research/physical-zqy-scalar-span/INDEPENDENT-KERNEL-AUDIT.json create mode 100644 research/physical-zqy-scalar-span/KERNEL-PROOF.md create mode 100644 research/physical-zqy-scalar-span/KERNEL-RESULT.json create mode 100644 research/physical-zqy-scalar-span/KERNEL.json create mode 100644 research/physical-zqy-scalar-span/formal_kernel.py create mode 100644 research/physical-zqy-scalar-span/independent_kernel.py create mode 100644 research/physical-zqy-scalar-span/verify_kernel.py diff --git a/research/physical-zqy-scalar-span/FORMAL-KERNEL.json b/research/physical-zqy-scalar-span/FORMAL-KERNEL.json new file mode 100644 index 0000000000..bf78257ec0 --- /dev/null +++ b/research/physical-zqy-scalar-span/FORMAL-KERNEL.json @@ -0,0 +1,34 @@ +{ + "actual_operator_identifications_used": false, + "cases": { + "provider_backward": { + "exact_formal_HK_zero": true, + "full_frame_histories": 4891, + "history_formal_terms": 119521, + "kernel_formula": "[I_112;I_112;0_408x112]", + "maximum_surviving_word_length": 1 + }, + "source_backward": { + "exact_formal_HK_zero": true, + "full_frame_histories": 5019, + "history_formal_terms": 80007, + "kernel_formula": "[I_112;I_112;0_408x112]", + "maximum_surviving_word_length": 1 + }, + "source_forward": { + "exact_formal_HK_zero": true, + "full_frame_histories": 4968, + "history_formal_terms": 94439, + "kernel_formula": "[0_112x112;I_112;0_408x112]", + "maximum_surviving_word_length": 1 + } + }, + "distinct_native_generator_names": 72, + "matrix_sum_relations_used": false, + "phase_or_group_normalization_used": false, + "reductions": "Only adjacent signed inverse cancellation on free words.", + "schema": "native-full-history-freeword-kernel/v1", + "scope": "Formal corroboration of the three frozen full-frame observation families, considered separately. Scalar identities over these formal words survive any consistent assignment of invertible operators, hence every tensor width. Ownership and legal native physical semantics remain inherited from the actual source.", + "source_native_sha256": "1bad1ffe747c3977d1a6bc1cfa9faa4127e38cbf49d7fcf4ae8060fbc7f67d4e", + "status": "PASS_FORMAL_FREEWORD_RIGHT_KERNEL_THREE_CASES" +} diff --git a/research/physical-zqy-scalar-span/INDEPENDENT-KERNEL-AUDIT.json b/research/physical-zqy-scalar-span/INDEPENDENT-KERNEL-AUDIT.json new file mode 100644 index 0000000000..7a60d6ef43 --- /dev/null +++ b/research/physical-zqy-scalar-span/INDEPENDENT-KERNEL-AUDIT.json @@ -0,0 +1,83 @@ +{ + "K_Y_identity_columns": 112, + "actual_group_annihilation_checks": 4891, + "actual_observation_operator_count": 59, + "actual_observation_operator_set_sha256": "34ad3a3f37a53afd59e0d295d6dffa446819539b9ac46556ef51134eb888d831", + "all_width_reason": "Each exact signed group identity lifts by operator composition to every tensor width. H_j K=0 retains scalar owner coefficients outside tensor powers and does not use physical width-one linear relations.", + "augmentation_nonY_rank": 474, + "controls": { + "Y_variation_without_nonY_compensation": { + "coefficient": "1/2", + "event": { + "event": 15380, + "frame": 1, + "role": [ + "L", + 299 + ] + }, + "first_nonzero_group_column": [ + 0, + 17 + ], + "history": 79, + "residual_terms": 4 + }, + "supplied_original_Y0_identity_observation": { + "identity_operator_coefficient": "1", + "non_annihilated_Y_column": 0 + }, + "wrong_Y_row": { + "coefficient": "1/2", + "event": { + "event": 15875, + "frame": 1, + "role": [ + "L", + 0 + ] + }, + "first_nonzero_group_column": [ + 0, + 0 + ], + "history": 269, + "residual_terms": 1 + }, + "wrong_nonY_compensation": { + "coefficient": "1/2", + "event": { + "event": 15875, + "frame": 1, + "role": [ + "L", + 0 + ] + }, + "first_nonzero_group_column": [ + 0, + 0 + ], + "history": 269, + "residual_terms": 1 + } + }, + "full_frame_histories": 4891, + "kernel_sha256": "250947ff109dcb1e72f9a379e40d82aed099f2925894537719bf719525a916ca", + "kernel_shape": "K=[I112;I112;0_408], and zero on all nine owned inputs", + "limits": "Only the unchanged frozen native full-frame snapshots. Separate reads of partial-frame/main Y, modified paid contacts/history or new supplied correlated observations are outside this theorem. Fixing helper or owned values alone does not evade this particular kernel, because it changes only X and Y. No paid lower bound, new caller or new kappa is asserted.", + "method": "Own Fraction elimination of augmentation proposes scalar K; decisive independent verification is H_j K=0 in every actual group coefficient of every original replay row. No decomposition certificate, search import, modular calculation or width-one matrix-sum relation is used. The candidate is derived without reading saved kernel rows, then compared with KERNEL.json.", + "nonzero_nonY_compensating_original_roles": 112, + "original_K_nonzero_entries": 224, + "original_history_group_terms": 119515, + "original_independent_roles": 632, + "owned_entry_roles": 9, + "paired_X_Y_group_terms_checked": 11262, + "physical_chart_guard": "Logical source variables are converted to physical independent inputs by their invertible birth frames. All snapshots share the one full inverse-transpose Gaussian Phi. Right birth factors and common Phi preserve annihilation and the hidden-Y fiber; owned chart/precision execution remains inherited.", + "seconds": 3.311939083971083, + "source_owned_compensation_is_zero": true, + "source_payload_sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05", + "source_word_sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc", + "status": "PASS_INDEPENDENT_ORIGINAL_GROUP_HISTORY_HIDDEN_Y_KERNEL", + "theorem": "At every width, every original Y variation can be compensated by the same logical X variation, with all helpers and owned entries fixed, leaving every admitted full-frame history unchanged. Therefore no nonzero pure-Y linear observation lies in their module even under arbitrary address-End left coefficients; no deterministic postprocessing of only those snapshots can recover a nonconstant function of Y." +} diff --git a/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md b/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md index c576e1e55b..3537c9ea94 100644 --- a/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md +++ b/research/physical-zqy-scalar-span/INTERNAL-REVIEW.md @@ -4,6 +4,27 @@ Separate OpenAI Codex agents checked the source-specific phase algebra and tensor argument. This is internal AI-assisted review, not independent human acceptance or a proof-kernel result. +The kernel extension adds a separate native/frame/group implementation in +`independent_kernel.py`. It derives the provider kernel without importing the +primary interpreter, monomial evaluator or discovery eliminator, then checks +the resulting kernel against the original operator-valued histories. Scalar +augmentation is used for discovery, not as a substitute for that final check. +`INDEPENDENT-KERNEL-AUDIT.json` records the result. Normal and optimized runs +pass. The free-word corroboration uses the primary event interpreter with an +alternate algebra and is explicitly not an independent parser. + +A separate read-only scope review found the input-fiber argument, raw-backward +R inverse, physical birth-frame conversion, fixed helper/owned values and the +eight partial-cache boundary consistent. That review also replayed the three +kernel scripts normally and with optimization. This is an internal AI-assisted +review, not external scientific acceptance. In the backward case, inability to +identify Y does not mean independence of Y when X is held fixed: the channel +can depend on X-Y. + +The older scalar and finite-image corroboration below concerns the initial +publication. Its rank/ABI checks are optional direct entry points after the +kernel extension, rather than current registered proof dependencies. + - `phase_audit.py` uses the pinned signed Clifford evaluator and its absolute phase anchor, rather than the primary direct Gram-phase column formula. All 147,456 native variants and 36,864 product columns agree, including raw @@ -19,17 +40,17 @@ acceptance or a proof-kernel result. self-contained receipt is `INDEPENDENT-WIDTH1.json`. - A separate Gaussian-integer Gram implementation reproduced width-two rank 215 and determinant 298401053 modulo 1000000009, in normal and optimized - modes. The registered primary checker regenerates this same certificate. + modes. The optional primary `verify.py` regenerates this certificate. - A separate literal-normalizer implementation checked all 31,457,280 seed Gaussian-kernel entries, and independently reproduced the 1,012/59/59,708 ABI image/product counts and set hashes. Static review found the required physical/logical commutation and finite-family tensor argument valid. The - portable registered `abi_closure.py` regenerates the published certificate. + portable optional `abi_closure.py` regenerates the published certificate. -The registered commands, their source pins and the written proofs are the -public reproduction path. The last two internal audits are corroboration, -not additional standalone registered entry points. Source-generation scripts -were not changed to obtain these results. +The current registered commands, source pins and KERNEL-PROOF.md are the +kernel reproduction path. The older internal Gram and normalizer audits are +corroboration, not additional standalone registered entry points. +Source-generation scripts were not changed to obtain these results. Optional exact width-one corroboration: @@ -39,5 +60,5 @@ python3 -I -B research/physical-zqy-scalar-span/independent_width1.py It writes nothing by default and prints `PASS_INDEPENDENT_EXACT_WIDTH1_PHYSICAL_QUOTIENT`. Its explicit `--write` -option regenerates the separate receipt. The registered rank-sandwich proof -already suffices; this slower exact calculation is not required for CI. +option regenerates the separate receipt. This older exact calculation is not +required by the kernel proof or current CI suite. diff --git a/research/physical-zqy-scalar-span/KERNEL-PROOF.md b/research/physical-zqy-scalar-span/KERNEL-PROOF.md new file mode 100644 index 0000000000..3bf3445bd7 --- /dev/null +++ b/research/physical-zqy-scalar-span/KERNEL-PROOF.md @@ -0,0 +1,63 @@ +# An explicit kernel of every retained full-frame native history + +The new source-specific fact is simple: every raw-backward retained full-frame value is unchanged when the original logical X and Y inputs are shifted by the same arbitrary vector, with all helpers fixed. For the raw-forward word, shifting Y alone is invisible. These identities hold coefficient by coefficient in the native operator algebra. They remove the need for a monomial-independence assumption in this observation question. + +## Exact statement + +Use the frozen words and the source-bound event/frame semantics in native.py and SOURCES.json. The 632 persistent original roles are 112 X, 112 Y and 408 independent helpers. Retain every nonzero full-nine-dimensional-frame value throughout the entire word, even after an intended exit. Repeated identical values may be deduplicated. The source has no full-frame persistent input at entry. Zero values add no information. + +Write H_f for this complete retained channel at any positive digit width f. The sparse scalar kernel certificate is + + backward: K v = (v, v, 0), + forward: K v = (0, v, 0), + H_f K = 0, K_Y = I_112. + +For #5402 raw backward the channel contains 4,891 distinct nonzero values. The final #4610 raw-backward and raw-forward channels contain 5,019 and 4,968. The direct checker verifies the identity separately for each of them. KERNEL.json explicitly stores all 632 rows of the backward kernel; the forward version changes its X block to zero. Helpers and owned inputs are not identified with Y or surrendered: their change is zero. + +It follows that every change of arbitrary Y can be accompanied by a change of X that leaves every retained value unchanged. In particular: + +* No arbitrary address-linear combination of the retained values can equal a nonzero function only of the original Y. The left operators may be computationally expensive and need not be native monomials. +* Any postprocessor whose data consist only of this full-frame channel cannot exactly determine a nonconstant function of arbitrary Y. The ambiguity is between two valid independent-input instances with identical observations. Original helper values can also be supplied: they are the same in those instances. + +The source question's b=ZQY_return, with the specified native return Y_return=Dy, is a nonzero pure-original-Y map. Nonzeroness follows from ZW=14I and invertibility of D,Q. The theorem therefore excludes recovering that target from the frozen channel alone. A later caller Y already mixed with X has a different meaning. + +## Direct certificate and all-width proof + +A logical history row has the form + + H_j = sum_(input s, native word g) a_(j,s,g) g x_s, + +with rational scalar coefficients and literal native operators. The direct verifier freshly replays each frozen source and checks + + a_(j,X_i,g) + a_(j,Y_i,g) = 0 (backward), + a_(j,Y_i,g) = 0 (forward) + +for every history, original index i and literal operator g. These are exactly H_j K=0. Thus a backward channel factors through X-Y and the helper inputs; a forward channel factors through X and the helper inputs. K_Y=I prevents the vacuous zero-kernel argument. + +The actual-operator checker cancels coefficients of identical signed native monomials before numerical matrix evaluation. A separate formal checker repeats all three row identities using 72 free generator names and only adjacent inverse cancellation; it makes no actual-operator identification. Thus the kernel identities also survive any consistent invertible assignment of those letters, with forward and backward observation families interpreted separately. It does not use the width-one four-term linear relation, modular nonmembership, a tensor Gram rank, or an inverse of an operator polynomial. Absolute phases remain part of the literal operators, rather than being absorbed into exterior owner coefficients. + +A composition or inverse identity between literal one-column native operators remains valid under their columnwise f-fold tensor lift, with spectator axes fixed. Extending this multiplicative assignment linearly, while keeping the rational owner coefficients unchanged, evaluates the same coefficientwise zero at every positive f. The owner kernel K is a scalar matrix between fields; it is not tensor-powered. Independence of different lifted operators is unnecessary. + +For arbitrary left address operators A_j, multiplying the row identities gives + + (sum_j A_j H_j) K = 0. + +If that sum were a nonzero Y-only linear map T, its product with K would instead be T because K_Y=I, a contradiction. For nonlinear postprocessing, compare an input z with z+Kv. Their whole channels coincide while their Y values differ by arbitrary v. This proves exact nonidentifiability without an approximation or precision lower bound. + +## Physical coordinates and exact boundary + +The source rows use logical native input coordinates. Every physical original input differs by its own invertible birth-frame factor on the right, and a logical complete frame has one common full-frame factor on the left. In raw backward this common factor is R inverse with the retained conjugated native letters. It must not be silently replaced by the forward R. + +Applying the individual birth-frame maps to the kernel's input components gives the corresponding physical input displacement. Those maps do not mix original-field labels or X/Y/helper roles, and the Y displacement remains arbitrary. The full-frame left factor maps a zero logical history difference to zero. This conversion proves the physical ambiguity; it does not claim that preparing the compensating physical inputs is free or scalar-only. + +The #5402 WORD is the raw native body. Its eight output caches are still partial-frame data until the provider boundary exchanges and clears them. They are not zero at the WORD endpoint and are not included as full-frame observations. The theorem does not describe the whole machine state as Y-blind. Lower-frame current Y, original X, partial cache reads, extra paid transformations, a changed word, or a relation restricting X and Y can supply different information and are outside this channel. Fixing the helpers or owned inputs alone does not remove this particular kernel, because their displacement is zero. A provider-boundary extension must explicitly check which new values are supplied; the native-body certificate does not replace that check. + +The result concerns exact recovery on arbitrary source inputs. A finite-precision approximation lower bound, a profitable new supplier and the complete multiplication theorem require separate arguments. No new kappa or scientific acceptance is claimed by replay success. + +## Verification and discovery + +Run verify_kernel.py, formal_kernel.py and independent_kernel.py in normal and optimized Python. The direct checker checks all three channels, the 224 nonzero backward kernel entries, all 632 original rows and four failure controls: a vacuous zero kernel, a missing X compensator, a corrupted signed history coefficient, and an added original/lower-frame Y side observation. + +Discovery first found a 474-row operator-module container for #5402, with non-Y unit upper triangle in discovery order. All 1,438 container terms turned out scalar, giving the simple kernel above. A separately written implementation checked the full container factorization and independently regenerated the scalar kernel from augmented histories, then verified it against the original operator-valued rows. The large discovery decomposition is not a runtime or proof dependency of the small direct certificate. Triangular elimination and kernel nonidentifiability are standard linear algebra; the source-specific complete-channel identities and their physical interpretation are the contribution. + +Prepared by THU New Media Research Center (@thu-nmrc), with substantial OpenAI Codex multi-agent assistance. Retain Mark/Matarener's #5427 event/version semantics, Dillon's #5402 provider, Cao Yifan's #4610 word, the Cinna Davis/Dugongue/zxv/Chris R native, phase, controller and compiler lineages, and their Apache-2.0 notices. diff --git a/research/physical-zqy-scalar-span/KERNEL-RESULT.json b/research/physical-zqy-scalar-span/KERNEL-RESULT.json new file mode 100644 index 0000000000..f57f4accbc --- /dev/null +++ b/research/physical-zqy-scalar-span/KERNEL-RESULT.json @@ -0,0 +1,85 @@ +{ + "all_width_lift": "Every coefficient of HK cancels between identical actual signed monomial operators, before numerical evaluation. Literal products and phase identities lift to every positive tensor width, with exterior scalar rational coefficients unchanged.", + "cases": { + "provider_backward": { + "direction": "raw backward", + "exact_HK_zero": true, + "full_frame_histories": 4891, + "history_exact_terms": 119515, + "history_terms_with_nonzero_kernel_row": 11262, + "kernel_formula": "K_X=I_112, K_Y=I_112, K_helpers=0_408x112", + "literal_decoded_operator_columns_sha256": "763bff3cc998dd17fcfc0bb0723f0b7a0be98e8ff5fdd27e18258d3b7afbd0d9", + "literal_group_operators": 215 + }, + "source_backward": { + "direction": "raw backward", + "exact_HK_zero": true, + "full_frame_histories": 5019, + "history_exact_terms": 80001, + "history_terms_with_nonzero_kernel_row": 11304, + "kernel_formula": "K_X=I_112, K_Y=I_112, K_helpers=0_408x112", + "literal_decoded_operator_columns_sha256": "763bff3cc998dd17fcfc0bb0723f0b7a0be98e8ff5fdd27e18258d3b7afbd0d9", + "literal_group_operators": 215 + }, + "source_forward": { + "direction": "forward", + "exact_HK_zero": true, + "full_frame_histories": 4968, + "history_exact_terms": 94137, + "history_terms_with_nonzero_kernel_row": 0, + "kernel_formula": "K_X=0_112x112, K_Y=I_112, K_helpers=0_408x112", + "literal_decoded_operator_columns_sha256": "763bff3cc998dd17fcfc0bb0723f0b7a0be98e8ff5fdd27e18258d3b7afbd0d9", + "literal_group_operators": 215 + } + }, + "direction": "raw backward", + "free_Y_columns": 112, + "full_frame_histories": 4891, + "history_exact_terms": 119515, + "history_terms_with_nonzero_kernel_row": 11262, + "information_consequence": "For every logical original Y displacement v, displace logical original X by the same v in either backward case, or leave X unchanged in the source-forward case; leave all 408 independent helper inputs fixed. Every full-frame history is identical. Thus a decoder receiving only that complete history cannot determine a nonconstant Y-only function, even with arbitrary nonlinear postprocessing.", + "kernel_formula": "K_X=I_112, K_Y=I_112, K_helpers=0_408x112", + "kernel_nonzero_rows": 224, + "kernel_scalar_terms": 224, + "kernel_sha256": "ad403cdd98975ae9a8033afff5a86f96d055e44c5be19c1f171387cf26cd3b81", + "literal_decoded_operator_columns_sha256": "763bff3cc998dd17fcfc0bb0723f0b7a0be98e8ff5fdd27e18258d3b7afbd0d9", + "literal_group_operators": 215, + "module_factorization_required_at_runtime": false, + "negative_controls": { + "deleted_X0_compensator": { + "failing_histories": 14, + "first_failing_history": 269, + "rejected": true + }, + "one_signed_X_history_coefficient": { + "history": 79, + "rejected": true, + "residual_literal_terms": 1 + }, + "original_Y_side_observation": { + "rejected": true, + "residual_literal_terms": 1 + }, + "zero_kernel_passes_HK_but_fails_Y_identity": true + }, + "new_observation_or_kappa": false, + "original_input_rows": 632, + "physical_coordinates": "Logical original-input coordinates are used. Each physical independent input differs by an invertible birth-chart right factor. Conjugating the input displacement by those factors preserves HK=0 and arbitrary variation of physical Y; this is not a claim that the physical input embedding is scalar-only or free.", + "polynomial_operator_inverses_used": false, + "schema": "native-full-history-direct-scalar-kernel/v1", + "scope": "Only the frozen #5402 raw-backward provider and original source-backward/source-forward full-frame observation families, each considered separately. The decoder is not also given lower-frame values, original inputs, new paid observations, or a changed producer. Source native, phase and compiler premises are inherited.", + "source_inputs": { + "provider": { + "path": "research/native-rank8-helper-provider/WORD.json.gz", + "sha256": "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc" + }, + "source": { + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05" + } + }, + "source_monomial_sha256": "87cdb1688b841891eccefdcaebe67b97a6c86b7af676bbbb667d1d5ee5d45d3e", + "source_native_sha256": "1bad1ffe747c3977d1a6bc1cfa9faa4127e38cbf49d7fcf4ae8060fbc7f67d4e", + "status": "PASS_EXACT_ALL_WIDTH_FULL_HISTORY_Y_BLINDNESS", + "width_one_matrix_sum_relations_used": false +} diff --git a/research/physical-zqy-scalar-span/KERNEL.json b/research/physical-zqy-scalar-span/KERNEL.json new file mode 100644 index 0000000000..cd699656f9 --- /dev/null +++ b/research/physical-zqy-scalar-span/KERNEL.json @@ -0,0 +1,1763 @@ +{ + "coordinate_convention": "Logical independent native input roles. Physical birth-chart maps are invertible right factors; the corresponding physical input deformation conjugates these scalar rows by those birth maps.", + "free_Y_columns": 112, + "original_input_roles": 632, + "provenance_module_certificate_sha256": "fa4cb2d6a9d8e04d056f5e1b9494909772611cc78438ed5ec9ab36b62642bd03", + "rows": [ + [ + [ + 0, + "1" + ] + ], + [ + [ + 1, + "1" + ] + ], + [ + [ + 2, + "1" + ] + ], + [ + [ + 3, + "1" + ] + ], + [ + [ + 4, + "1" + ] + ], + [ + [ + 5, + "1" + ] + ], + [ + [ + 6, + "1" + ] + ], + [ + [ + 7, + "1" + ] + ], + [ + [ + 8, + "1" + ] + ], + [ + [ + 9, + "1" + ] + ], + [ + [ + 10, + "1" + ] + ], + [ + [ + 11, + "1" + ] + ], + [ + [ + 12, + "1" + ] + ], + [ + [ + 13, + "1" + ] + ], + [ + [ + 14, + "1" + ] + ], + [ + [ + 15, + "1" + ] + ], + [ + [ + 16, + "1" + ] + ], + [ + [ + 17, + "1" + ] + ], + [ + [ + 18, + "1" + ] + ], + [ + [ + 19, + "1" + ] + ], + [ + [ + 20, + "1" + ] + ], + [ + [ + 21, + "1" + ] + ], + [ + [ + 22, + "1" + ] + ], + [ + [ + 23, + "1" + ] + ], + [ + [ + 24, + "1" + ] + ], + [ + [ + 25, + "1" + ] + ], + [ + [ + 26, + "1" + ] + ], + [ + [ + 27, + "1" + ] + ], + [ + [ + 28, + "1" + ] + ], + [ + [ + 29, + "1" + ] + ], + [ + [ + 30, + "1" + ] + ], + [ + [ + 31, + "1" + ] + ], + [ + [ + 32, + "1" + ] + ], + [ + [ + 33, + "1" + ] + ], + [ + [ + 34, + "1" + ] + ], + [ + [ + 35, + "1" + ] + ], + [ + [ + 36, + "1" + ] + ], + [ + [ + 37, + "1" + ] + ], + [ + [ + 38, + "1" + ] + ], + [ + [ + 39, + "1" + ] + ], + [ + [ + 40, + "1" + ] + ], + [ + [ + 41, + "1" + ] + ], + [ + [ + 42, + "1" + ] + ], + [ + [ + 43, + "1" + ] + ], + [ + [ + 44, + "1" + ] + ], + [ + [ + 45, + "1" + ] + ], + [ + [ + 46, + "1" + ] + ], + [ + [ + 47, + "1" + ] + ], + [ + [ + 48, + "1" + ] + ], + [ + [ + 49, + "1" + ] + ], + [ + [ + 50, + "1" + ] + ], + [ + [ + 51, + "1" + ] + ], + [ + [ + 52, + "1" + ] + ], + [ + [ + 53, + "1" + ] + ], + [ + [ + 54, + "1" + ] + ], + [ + [ + 55, + "1" + ] + ], + [ + [ + 56, + "1" + ] + ], + [ + [ + 57, + "1" + ] + ], + [ + [ + 58, + "1" + ] + ], + [ + [ + 59, + "1" + ] + ], + [ + [ + 60, + "1" + ] + ], + [ + [ + 61, + "1" + ] + ], + [ + [ + 62, + "1" + ] + ], + [ + [ + 63, + "1" + ] + ], + [ + [ + 64, + "1" + ] + ], + [ + [ + 65, + "1" + ] + ], + [ + [ + 66, + "1" + ] + ], + [ + [ + 67, + "1" + ] + ], + [ + [ + 68, + "1" + ] + ], + [ + [ + 69, + "1" + ] + ], + [ + [ + 70, + "1" + ] + ], + [ + [ + 71, + "1" + ] + ], + [ + [ + 72, + "1" + ] + ], + [ + [ + 73, + "1" + ] + ], + [ + [ + 74, + "1" + ] + ], + [ + [ + 75, + "1" + ] + ], + [ + [ + 76, + "1" + ] + ], + [ + [ + 77, + "1" + ] + ], + [ + [ + 78, + "1" + ] + ], + [ + [ + 79, + "1" + ] + ], + [ + [ + 80, + "1" + ] + ], + [ + [ + 81, + "1" + ] + ], + [ + [ + 82, + "1" + ] + ], + [ + [ + 83, + "1" + ] + ], + [ + [ + 84, + "1" + ] + ], + [ + [ + 85, + "1" + ] + ], + [ + [ + 86, + "1" + ] + ], + [ + [ + 87, + "1" + ] + ], + [ + [ + 88, + "1" + ] + ], + [ + [ + 89, + "1" + ] + ], + [ + [ + 90, + "1" + ] + ], + [ + [ + 91, + "1" + ] + ], + [ + [ + 92, + "1" + ] + ], + [ + [ + 93, + "1" + ] + ], + [ + [ + 94, + "1" + ] + ], + [ + [ + 95, + "1" + ] + ], + [ + [ + 96, + "1" + ] + ], + [ + [ + 97, + "1" + ] + ], + [ + [ + 98, + "1" + ] + ], + [ + [ + 99, + "1" + ] + ], + [ + [ + 100, + "1" + ] + ], + [ + [ + 101, + "1" + ] + ], + [ + [ + 102, + "1" + ] + ], + [ + [ + 103, + "1" + ] + ], + [ + [ + 104, + "1" + ] + ], + [ + [ + 105, + "1" + ] + ], + [ + [ + 106, + "1" + ] + ], + [ + [ + 107, + "1" + ] + ], + [ + [ + 108, + "1" + ] + ], + [ + [ + 109, + "1" + ] + ], + [ + [ + 110, + "1" + ] + ], + [ + [ + 111, + "1" + ] + ], + [ + [ + 0, + "1" + ] + ], + [ + [ + 1, + "1" + ] + ], + [ + [ + 2, + "1" + ] + ], + [ + [ + 3, + "1" + ] + ], + [ + [ + 4, + "1" + ] + ], + [ + [ + 5, + "1" + ] + ], + [ + [ + 6, + "1" + ] + ], + [ + [ + 7, + "1" + ] + ], + [ + [ + 8, + "1" + ] + ], + [ + [ + 9, + "1" + ] + ], + [ + [ + 10, + "1" + ] + ], + [ + [ + 11, + "1" + ] + ], + [ + [ + 12, + "1" + ] + ], + [ + [ + 13, + "1" + ] + ], + [ + [ + 14, + "1" + ] + ], + [ + [ + 15, + "1" + ] + ], + [ + [ + 16, + "1" + ] + ], + [ + [ + 17, + "1" + ] + ], + [ + [ + 18, + "1" + ] + ], + [ + [ + 19, + "1" + ] + ], + [ + [ + 20, + "1" + ] + ], + [ + [ + 21, + "1" + ] + ], + [ + [ + 22, + "1" + ] + ], + [ + [ + 23, + "1" + ] + ], + [ + [ + 24, + "1" + ] + ], + [ + [ + 25, + "1" + ] + ], + [ + [ + 26, + "1" + ] + ], + [ + [ + 27, + "1" + ] + ], + [ + [ + 28, + "1" + ] + ], + [ + [ + 29, + "1" + ] + ], + [ + [ + 30, + "1" + ] + ], + [ + [ + 31, + "1" + ] + ], + [ + [ + 32, + "1" + ] + ], + [ + [ + 33, + "1" + ] + ], + [ + [ + 34, + "1" + ] + ], + [ + [ + 35, + "1" + ] + ], + [ + [ + 36, + "1" + ] + ], + [ + [ + 37, + "1" + ] + ], + [ + [ + 38, + "1" + ] + ], + [ + [ + 39, + "1" + ] + ], + [ + [ + 40, + "1" + ] + ], + [ + [ + 41, + "1" + ] + ], + [ + [ + 42, + "1" + ] + ], + [ + [ + 43, + "1" + ] + ], + [ + [ + 44, + "1" + ] + ], + [ + [ + 45, + "1" + ] + ], + [ + [ + 46, + "1" + ] + ], + [ + [ + 47, + "1" + ] + ], + [ + [ + 48, + "1" + ] + ], + [ + [ + 49, + "1" + ] + ], + [ + [ + 50, + "1" + ] + ], + [ + [ + 51, + "1" + ] + ], + [ + [ + 52, + "1" + ] + ], + [ + [ + 53, + "1" + ] + ], + [ + [ + 54, + "1" + ] + ], + [ + [ + 55, + "1" + ] + ], + [ + [ + 56, + "1" + ] + ], + [ + [ + 57, + "1" + ] + ], + [ + [ + 58, + "1" + ] + ], + [ + [ + 59, + "1" + ] + ], + [ + [ + 60, + "1" + ] + ], + [ + [ + 61, + "1" + ] + ], + [ + [ + 62, + "1" + ] + ], + [ + [ + 63, + "1" + ] + ], + [ + [ + 64, + "1" + ] + ], + [ + [ + 65, + "1" + ] + ], + [ + [ + 66, + "1" + ] + ], + [ + [ + 67, + "1" + ] + ], + [ + [ + 68, + "1" + ] + ], + [ + [ + 69, + "1" + ] + ], + [ + [ + 70, + "1" + ] + ], + [ + [ + 71, + "1" + ] + ], + [ + [ + 72, + "1" + ] + ], + [ + [ + 73, + "1" + ] + ], + [ + [ + 74, + "1" + ] + ], + [ + [ + 75, + "1" + ] + ], + [ + [ + 76, + "1" + ] + ], + [ + [ + 77, + "1" + ] + ], + [ + [ + 78, + "1" + ] + ], + [ + [ + 79, + "1" + ] + ], + [ + [ + 80, + "1" + ] + ], + [ + [ + 81, + "1" + ] + ], + [ + [ + 82, + "1" + ] + ], + [ + [ + 83, + "1" + ] + ], + [ + [ + 84, + "1" + ] + ], + [ + [ + 85, + "1" + ] + ], + [ + [ + 86, + "1" + ] + ], + [ + [ + 87, + "1" + ] + ], + [ + [ + 88, + "1" + ] + ], + [ + [ + 89, + "1" + ] + ], + [ + [ + 90, + "1" + ] + ], + [ + [ + 91, + "1" + ] + ], + [ + [ + 92, + "1" + ] + ], + [ + [ + 93, + "1" + ] + ], + [ + [ + 94, + "1" + ] + ], + [ + [ + 95, + "1" + ] + ], + [ + [ + 96, + "1" + ] + ], + [ + [ + 97, + "1" + ] + ], + [ + [ + 98, + "1" + ] + ], + [ + [ + 99, + "1" + ] + ], + [ + [ + 100, + "1" + ] + ], + [ + [ + 101, + "1" + ] + ], + [ + [ + 102, + "1" + ] + ], + [ + [ + 103, + "1" + ] + ], + [ + [ + 104, + "1" + ] + ], + [ + [ + 105, + "1" + ] + ], + [ + [ + 106, + "1" + ] + ], + [ + [ + 107, + "1" + ] + ], + [ + [ + 108, + "1" + ] + ], + [ + [ + 109, + "1" + ] + ], + [ + [ + 110, + "1" + ] + ], + [ + [ + 111, + "1" + ] + ], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [], + [] + ], + "schema": "native-full-history-Y-kernel/v1", + "source_monomial_sha256": "87cdb1688b841891eccefdcaebe67b97a6c86b7af676bbbb667d1d5ee5d45d3e", + "source_native_sha256": "1bad1ffe747c3977d1a6bc1cfa9faa4127e38cbf49d7fcf4ae8060fbc7f67d4e" +} diff --git a/research/physical-zqy-scalar-span/README.md b/research/physical-zqy-scalar-span/README.md index a1d90de9b0..5b46d6a339 100644 --- a/research/physical-zqy-scalar-span/README.md +++ b/research/physical-zqy-scalar-span/README.md @@ -1,24 +1,28 @@ -# Actual-phase native history scalar spans +# An explicit full-frame native-history kernel -This package resolves the physical scalar-span question left open by +## Stronger complete-channel kernel + +[KERNEL-PROOF.md](KERNEL-PROOF.md) gives a short all-width information barrier for the exact full-frame-only channels. Every raw-backward history is invariant under logical `(X,Y,H) -> (X+v,Y+v,H)`; the forward histories are invariant under `Y -> Y+v`. The small [kernel certificate](KERNEL.json) and [fresh direct replay](KERNEL-RESULT.json) therefore exclude arbitrary postprocessing of these retained values, including unrestricted left operators. Helpers remain fixed. The statement does not include partial-frame values, original X, new paid observations or changed input relations. + +This stronger proof needs no independence of monomial matrices. The earlier scalar-span and finite-image results below remain separately replayable evidence, with their original restricted statements. No new kappa is claimed. + +## Earlier scalar-span certificate + +The earlier certificate resolves the physical scalar-span question left open by [Mark/Matarener's #5427](https://github.com/CrocSwap/integer-mult-bounds/pull/5427). At **every positive tensor width**, no nonzero pure-Y observation is a scalar combination of all retained full-frame versions of the frozen #5402 backward word or either orientation of the final #4610 word. All original inputs remain independent. The complete history is granted, including versions after an exit. -The new point is the actual operator algebra. The 215 signed operators have +That certificate tests the actual operator algebra. The 215 signed operators have one genuine four-term linear relation at width one. After including that relation the observation still does not exist. A full-rank tensor-square Gram certificate and the shared zero-state anchor cover every larger width. Exact rational projection ranks and nonzero modular minors play separate roles; modular nonmembership alone is not used as a rational exclusion. -**This is a restricted negative theorem, with no new kappa.** It does not close -the history under independently chosen free left monomial maps, including the -concrete Z-ABI transports. It does not exclude changed native schedules, -partial-frame histories, new paid queries or an endogenous observer in those -larger models. The independent inputs, observation version and these limits +**The scalar certificate alone is a restricted negative theorem.** The new input kernel above closes arbitrary postprocessing of the same full-frame channel. Changed native schedules, partial-frame histories and new paid observations supply different data and remain outside the channel. The independent inputs, observation version and these limits are part of the claim. See [PROOF.md](PROOF.md). ## Reproduce @@ -29,31 +33,26 @@ Python 3.12, standard library only, read-only default: python3 -B scripts/research_package.py --package research/physical-zqy-scalar-span ``` -Expected mathematical marker: +The registered checks verify the direct all-width input kernel, repeat it over formal free words, independently regenerate the provider kernel with a separate native/group/frame implementation, and compare exact physical phases against the retained Clifford implementation. All run in normal and optimized modes. The ordinary command compares frozen receipts without writing; `--write` explicitly authors outputs. + +The initial scalar-rank/Gram and fixed-image certificates are retained unchanged from publication head `6d81d47e6d107e3c52b4583526d31e102b219bdc`. They are no longer dependencies of the stronger kernel proof or default registered replay. They remain optional direct checks: -```text -PASS_ALL_WIDTH_PHYSICAL_NATIVE_SCALAR_SPAN_NO_NEW_KAPPA +```sh +python3 -B research/physical-zqy-scalar-span/verify.py +python3 -B research/physical-zqy-scalar-span/abi_closure.py ``` -The registered checks recompute the finite ABI left-image certificate, all -source-bound row ranks, the one-column operator relation/rank and the tensor-square Gram certificate, in normal and -optimized modes. The separate phase audit compares actual columns against the -retained exact Clifford implementation. `--write` explicitly regenerates the -local result; ordinary replay compares it without writing. Mathematical/runtime -checks are recorded in VALIDATION.md; publication byte/export transport results -are recorded in the PR. [INTERNAL-REVIEW.md](INTERNAL-REVIEW.md) separates internal -corroboration from external acceptance. No full native admission, selected cold -replay, compiler/outer, precision/tape, Lean or Docker run is claimed. +Mathematical/runtime checks are recorded in VALIDATION.md; exact publication byte/export results are recorded in the PR. [INTERNAL-REVIEW.md](INTERNAL-REVIEW.md) distinguishes AI corroboration from external acceptance. No selected cold replay, fresh complete native admission, compiler/outer, precision/tape, Lean or Docker run is claimed. -## Concrete Z-ABI left-image extension +## Earlier concrete Z-ABI certificate -A separate bounded continuation grants each backward-provider version one +The earlier bounded continuation grants each backward-provider version one left image from `{I, Kp_i, Km_a, Km_a^-1 Kp_i}`. The 1,012 distinct physical maps and 59 actual history operators give 59,708 pairwise nonproportional products, with exact F9 commutation and phase checks. The resulting span has no nonzero pure-Y observation for **every f>=59,707**. Thus this fixed bank cannot implement an all-width observer. This does not assert small-width -nonmembership or closure under arbitrary further products. The proof and +nonmembership or closure under arbitrary further products on its own. The new kernel separately excludes this whole channel at every positive width. The proof and [ABI-CLOSURE.json](ABI-CLOSURE.json) state this as a separate theorem. ## Open next questions diff --git a/research/physical-zqy-scalar-span/TASK.json b/research/physical-zqy-scalar-span/TASK.json index a62de3f881..1c80a261d2 100644 --- a/research/physical-zqy-scalar-span/TASK.json +++ b/research/physical-zqy-scalar-span/TASK.json @@ -70,25 +70,25 @@ ] }, "scope_status": "changed", - "actual_scope": "Resolve actual-phase scalar-span separation at every positive tensor width, and exclude the concrete1012-map Z-ABI left-image family at every f>=59707, for the frozen native histories.", - "scope_change_reason": "The named physical follow-up was unexecuted. Actual operators have a width-one relation and need an all-width argument beyond formal words. A separate bounded constructive continuation tested the actual ABI monomial left images and found disjoint operator supports; the resulting finite-family theorem is stated separately.", - "bottleneck_link": "The#5415/#5419 consumer needs current ZQY; this rejects one zero-new-query grammar while leaving monomial preprocessing and changed native producers open.", + "actual_scope": "An explicit all-width input kernel for every retained full-frame value in the frozen #5402 raw-backward and final #4610 raw-backward/forward native words, excluding arbitrary postprocessing receiving only those channels. Earlier scalar/fixed-image certificates remain independent restricted results.", + "scope_change_reason": "After testing changed paid contacts, a new native-left module model exposed a simple complete input kernel. The fresh row identity HK=0 supersedes any independence-based restriction on postprocessing of the same full-frame channel. It does not exclude partial information or changed producers.", + "bottleneck_link": "The full-frame-only channel hides every original Y direction, even under arbitrary postprocessing. A construction must supply additional partial-frame information, change an input relation or producer, and pay its complete bill.", "budget_minutes": 60, - "stop_rule": "Finish both scoped physical separation statements and registered checks; stop this frozen scalar/finite-ABI family. Changed native producers or unrestricted products require a new hypothesis and budget.", + "stop_rule": "Verify the explicit kernel and independent source/physical interpretation, then stop expanding this frozen full-frame-only channel. New work must identify different information and a fully priced consumer.", "outcome": "negative-result", - "evidence": "PROOF.md, RESULT.json, literal phase audit, exact rational projection ranks and a Gaussian-integer Gram minor. ABI-CLOSURE.json authenticates1012 left maps and59708 pairwise nonproportional products; a separating-functionals proof supplies its width threshold.", + "evidence": "KERNEL.json, KERNEL-RESULT.json, KERNEL-PROOF.md, independent kernel audit. Older PROOF.md/RESULT.json/ABI-CLOSURE.json retain scalar and finite-family certificates.", "author": "THU New Media Research Center (@thu-nmrc)", "ai_assistance": "Substantial OpenAI Codex assistance by lead and separate algebra/phase agents; no independent human or kernel review.", "open_questions": [ { "question": "Can a changed native word retain pure Ry before Dx mixing at a profitable complete price?", - "why_it_matters": "Both frozen scalar and the specified finite Z-ABI image bank are excluded; a changed producer can supply new information.", + "why_it_matters": "The frozen full-frame-only channel cannot identify original Y: its backward values can depend on X-Y, with X independently arbitrary. A changed resource must add information, not just more postprocessing of the same values.", "first_step": "Emit one all-input prefix, its current-Y observation, every owned return and complete observer/termination bill.", "blocked_by": "No profitable changed physical producer is known in this package." }, { "question": "Can another real paid caller event supply a correlated current-version observation with disjoint mode ownership?", - "why_it_matters": "New nonfree history leaves the frozen-history hypotheses and could eliminate actual recursive calls.", + "why_it_matters": "The frozen full-frame-only channel cannot identify original Y: its backward values can depend on X-Y, with X independently arbitrary. A changed resource must add information, not just more postprocessing of the same values.", "first_step": "Specify one exact event/cut with all original inputs, observation owners and later consumers, then replay the complete exit.", "blocked_by": "No source-bound witness, lifetime proof and full bill are established here." } diff --git a/research/physical-zqy-scalar-span/VALIDATION.md b/research/physical-zqy-scalar-span/VALIDATION.md index 5bb776d062..810cb59e6a 100644 --- a/research/physical-zqy-scalar-span/VALIDATION.md +++ b/research/physical-zqy-scalar-span/VALIDATION.md @@ -1,49 +1,74 @@ # Validation scope -Python 3.12.14, standard library only, macOS arm64. No dependency install, -Lean, Docker, selected cold replay or unrelated historical suite was run. - -## Mathematical checks - -- Exact source-bound native rows, all full-frame history versions and rational - ranks: 4,891 /546, 5,019 /554 and 4,968 /554. Non-Y projection ranks match. -- The actual width-one operator rank is 214, with the exact four-term relation - and a separate nonzero Gaussian-integer minor. Physical quotient projection - lower bounds match exact rational upper bounds; no modular nonmembership - shortcut is used. -- Width-two 215-by-215 Gram determinant is 298401053 modulo 1000000009. - Every literal operator has zero-state coefficient one. The written - contraction proof covers every larger width. -- Independent Clifford phase audit: 147,456 native columns, 36,864 product - columns; wrong-phase and backward-direction controls. -- Fixed Z-ABI bank: 1,012 distinct left maps, 59 provider operators, 59,708 - pairwise distinct products and exact zero anchors. Exact signed F9 kernel - checks authenticate physical/logical left multiplication. The written - separating-functional proof has the explicit guard f>=59,707. -- Additional exact width-one Fraction audit passes without modular rank - inference; its portable optional script and separate receipt are included. - It ran in 90.663 seconds after import adaptation and 105.727 seconds after - final whitespace normalization. Internal audit is distinct - from external scientific acceptance; see INTERNAL-REVIEW.md. - -All six registered normal/optimized commands PASS. The primary normal and -optimized mathematical runs took 134.403 and 157.388 seconds respectively. -Phase and fixed-ABI replays also PASS in both modes. Publication byte/export -transport checks are recorded separately in the pull request after commit. Individual commands use explicit -exceptions; mathematical checks are not disabled by `-O`. The retained -Clifford engine has its own assertion-based internals, while the audit's -literal column comparisons and negative controls remain explicit. - -Development record: the first registered attempt rejected the result's JSON -key representation after completing its mathematical checks. Integer relation -indices are now serialized as strings. The revised result compares identically; -this repair changes no rank, source operator or scientific conclusion. +Python 3.12.14, standard library only, macOS arm64. The current registered +suite consists of eight commands. All eight pass on the kernel extension. +Default replay compares frozen receipts and writes no package files. + +## Current kernel checks + +- `verify_kernel.py` freshly replays the actual signed native histories in + all three frozen words: 4,891 provider-backward, 5,019 source-backward and + 4,968 source-forward distinct nonzero full-frame values. It checks the + explicit input kernel against every operator coefficient and verifies + `K_Y=I`. Four failure controls reject a vacuous kernel, missing X + compensation, one corrupted coefficient and added original-Y information. +- `independent_kernel.py` imports neither `native.py`, `monomial.py` nor the + discovery code. Its separate native/group/frame implementation regenerates + all 4,891 provider histories, derives the 224-entry kernel using exact + Fraction elimination of scalar augmentations, then checks the kernel + against every original operator-valued row. The final check, rather than + the augmentation alone, certifies the claimed identity. +- `formal_kernel.py` repeats all three identities over 72 free generator + names, cancelling only adjacent inverses. It uses the primary event/frame + interpreter with a different word algebra; it is corroboration rather than + an independently implemented parser. No matrix independence or width-one + matrix-sum relation is required. +- `phase_audit.py` compares 147,456 native columns and 36,864 product columns + with the retained exact Clifford evaluator, including absolute-phase and + backward-direction controls. + +All four scripts pass in normal and optimized Python, with `-I -W error -B`. +Checks use explicit exceptions and remain active under `-O`. The retained +Clifford engine also contains its own assertion-based internals; literal +column comparisons and the audit's failure controls remain explicit. + +The small kernel and source-bound row identities are the proof dependencies. +The 13 MB discovery module factorization is neither shipped nor required. +See KERNEL-PROOF.md for the all-width and physical-coordinate argument. +These are internal AI-assisted checks, not external human acceptance or a +proof-kernel result. Exact committed-byte, export, read-only replay and hosted +CI receipts are recorded at the publication commit in the pull request. + +## Historical scalar and finite-image checks + +The initial publication at `6d81d47e6d107e3c52b4583526d31e102b219bdc` +passed its then-registered six commands, its committed-byte/export checks, +a read-only Git-free replay and hosted CI. Those commands ran `verify.py`, +`phase_audit.py` and `abi_closure.py`, each normally and with optimization. +Their scalar/Gram/ABI scripts and frozen results remain byte-identical to +that commit, but the rank and ABI checks are no longer in the default suite +or dependencies of the stronger kernel theorem. + +That historical result includes exact projection ranks 546/546, 554/554 and +554/554; physical width-one operator rank 214 with a four-term relation; +the width-two 215-by-215 Gram determinant 298401053 modulo 1000000009; and +1,012 left maps producing 59,708 distinct products with the explicit +finite-family guard `f>=59,707`. The optional independent Fraction width-one +audit remains available via `independent_width1.py`. Its final source replay +passed in 105.727 seconds. See PROOF.md and INTERNAL-REVIEW.md for these older +restricted statements; they are not new kernel-extension replay claims. ## Limits -No runtime measurement here is a physical fixed-tape benchmark. The frozen -source words and inherited Clifford realization are reused, not readmitted as -a new complete native supplier. No new paid or productive profile, exponent, -precision/tape/stock/compiler funding or multiplication theorem is claimed. -The finite ABI theorem is not arbitrary monomial group/module closure and -makes no enlarged-family small-width exclusion. +The channel includes only complete-frame values of the frozen native bodies. +Original X/Y, partial-frame caches, changed words or new paid transformations +are additional information requiring their own source-bound analysis. Fixing +helpers or owned inputs alone does not remove this kernel. No approximation +or finite-precision lower bound is proved. + +No fixed-tape benchmark, selected cold replay, fresh complete native admission, +new paid/productive profile, exponent, precision/tape/stock/compiler funding, +Lean, Docker or complete multiplication theorem is claimed. No dependency +installation or unrelated historical suite was run. The optional full-history +ancestry preflight was not run in the shallow checkout; source blob pins and +the ordinary committed-byte preflight are separate checks. diff --git a/research/physical-zqy-scalar-span/VERIFY.json b/research/physical-zqy-scalar-span/VERIFY.json index 99d2287eb4..62110da3c2 100644 --- a/research/physical-zqy-scalar-span/VERIFY.json +++ b/research/physical-zqy-scalar-span/VERIFY.json @@ -18,10 +18,10 @@ "-W", "error", "-B", - "{package}/verify.py" + "{package}/phase_audit.py" ], - "timeout_seconds": 300, - "checks": "Exact rational history ranks, width-one physical quotient rank sandwich, absolute-phase control and tensor-square all-width certificate." + "timeout_seconds": 90, + "checks": "Independent retained Clifford/tableau/absolute-phase comparison of147456 native columns and36864 product columns, with phase/orientation controls." }, { "argv": [ @@ -31,10 +31,10 @@ "-W", "error", "-B", - "{package}/verify.py" + "{package}/phase_audit.py" ], - "timeout_seconds": 300, - "checks": "Exact rational history ranks, width-one physical quotient rank sandwich, absolute-phase control and tensor-square all-width certificate." + "timeout_seconds": 90, + "checks": "Independent retained Clifford/tableau/absolute-phase comparison of147456 native columns and36864 product columns, with phase/orientation controls." }, { "argv": [ @@ -43,10 +43,10 @@ "-W", "error", "-B", - "{package}/phase_audit.py" + "{package}/verify_kernel.py" ], "timeout_seconds": 90, - "checks": "Independent retained Clifford/tableau/absolute-phase comparison of147456 native columns and36864 product columns, with phase/orientation controls." + "checks": "Fresh actual-signed full native history kernel in all three frozen words; exact all-width ambiguity K_Y=I, HK=0; four target/compensator/sign/side-information controls. No width-one sum or rank inference." }, { "argv": [ @@ -56,10 +56,35 @@ "-W", "error", "-B", - "{package}/phase_audit.py" + "{package}/verify_kernel.py" ], "timeout_seconds": 90, - "checks": "Independent retained Clifford/tableau/absolute-phase comparison of147456 native columns and36864 product columns, with phase/orientation controls." + "checks": "Fresh actual-signed full native history kernel in all three frozen words; exact all-width ambiguity K_Y=I, HK=0; four target/compensator/sign/side-information controls. No width-one sum or rank inference." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/independent_kernel.py" + ], + "timeout_seconds": 90, + "checks": "Independent native/frame/group replay and Fraction-derived kernel, then original operator-coefficient HK=0 over all4891 histories, target and compensation controls. Does not import primary native/monomial/search code or consume the module decomposition." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/independent_kernel.py" + ], + "timeout_seconds": 90, + "checks": "Independent native/frame/group replay and Fraction-derived kernel, then original operator-coefficient HK=0 over all4891 histories, target and compensation controls. Does not import primary native/monomial/search code or consume the module decomposition." }, { "argv": [ @@ -68,10 +93,10 @@ "-W", "error", "-B", - "{package}/abi_closure.py" + "{package}/formal_kernel.py" ], "timeout_seconds": 90, - "checks": "Checks fixed1012 physical Z-ABI left maps, exact F9 commutation,59708 distinct signed products and zero anchors; consumes the freshly replayed primary exact546/546 rank certificate. Eventual-width proof is in PROOF.md." + "checks": "Same complete history invariant over72 formal free generators, cancelling only adjacent inverses. No actual-operator identifications, matrix independence or width-one linear relations; verifies all three cases." }, { "argv": [ @@ -81,10 +106,10 @@ "-W", "error", "-B", - "{package}/abi_closure.py" + "{package}/formal_kernel.py" ], "timeout_seconds": 90, - "checks": "Checks fixed1012 physical Z-ABI left maps, exact F9 commutation,59708 distinct signed products and zero anchors; consumes the freshly replayed primary exact546/546 rank certificate. Eventual-width proof is in PROOF.md." + "checks": "Same complete history invariant over72 formal free generators, cancelling only adjacent inverses. No actual-operator identifications, matrix independence or width-one linear relations; verifies all three cases." } ] } diff --git a/research/physical-zqy-scalar-span/formal_kernel.py b/research/physical-zqy-scalar-span/formal_kernel.py new file mode 100644 index 0000000000..7ce48b3660 --- /dev/null +++ b/research/physical-zqy-scalar-span/formal_kernel.py @@ -0,0 +1,98 @@ +#!/usr/bin/env python3 +"""Source-bound right kernel over formal native free words. + +THU New Media Research Center; substantial OpenAI Codex assistance. Apache-2.0. + +Only immediately adjacent inverse letters are reduced. No actual monomial +operator identification or phase/group normalization is performed. +""" +from pathlib import Path +from fractions import Fraction as F +from hashlib import sha256 +import argparse, json, sys, types +HERE = Path(__file__).resolve().parent +NATIVE_SHA = '1bad1ffe747c3977d1a6bc1cfa9faa4127e38cbf49d7fcf4ae8060fbc7f67d4e' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def left_row(row, op, backward): + # Each nonzero integer is a distinct formal letter with its signed inverse. + # Direction does not identify forward and backward letters: every direction + # is tested as a separate word system and independent observation family. + out = {} + for (role, old), value in row.items(): + word = () if old == 0 else old + reduced = word[1:] if word and word[0] == -op else (op,) + word + key = role, (reduced if reduced else 0) + q = out.get(key, F(0)) + value + if q: + out[key] = q + else: + out.pop(key, None) + return out + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--runtime', type=Path, default=HERE) + ap.add_argument('--write', action='store_true') + args = ap.parse_args() + runtime = args.runtime.resolve() + need(sha256((runtime/'native.py').read_bytes()).hexdigest() == NATIVE_SHA, 'actual native source pin') + sys.path.insert(0, str(runtime)) + import native as N + source, provider = N.read('source'), N.read('provider') + namespace = vars(N).copy() + namespace['left_row'] = left_row + replay = types.FunctionType(N.native_replay.__code__, namespace) + cases = {} + expected = {'provider_backward': (4891, 119521), 'source_backward': (5019, 80007), + 'source_forward': (4968, 94439)} + for name, program, backward in [ + ('provider_backward', provider['word'], True), + ('source_backward', source['programs']['backward'], True), + ('source_forward', source['programs']['forward'], False), + ]: + histories, _, _, _ = replay(source['canonical'], program, backward) + terms, max_word = 0, 0 + for row in histories: + residual = {} + for (role, word), value in row.items(): + need(role[0] == 'L' and 0 <= role[1] < 632, 'original input binding') + terms += 1 + max_word = max(max_word, 0 if word == 0 else len(word)) + active = role[1] < 224 if backward else 112 <= role[1] < 224 + if active: + key = role[1] % 112, word + q = residual.get(key, F(0)) + value + if q: + residual[key] = q + else: + residual.pop(key, None) + need(not residual, name + ' exact freeword HK=0') + need((len(histories), terms) == expected[name], 'frozen formal history family ' + name) + cases[name] = {'full_frame_histories': len(histories), 'history_formal_terms': terms, + 'maximum_surviving_word_length': max_word, 'exact_formal_HK_zero': True, + 'kernel_formula': '[I_112;I_112;0_408x112]' if backward else '[0_112x112;I_112;0_408x112]'} + result = {'schema': 'native-full-history-freeword-kernel/v1', + 'status': 'PASS_FORMAL_FREEWORD_RIGHT_KERNEL_THREE_CASES', + 'source_native_sha256': NATIVE_SHA, 'cases': cases, + 'distinct_native_generator_names': len(source['canonical']['warps']), + 'reductions': 'Only adjacent signed inverse cancellation on free words.', + 'actual_operator_identifications_used': False, 'phase_or_group_normalization_used': False, + 'matrix_sum_relations_used': False, + 'scope': 'Formal corroboration of the three frozen full-frame observation families, considered separately. Scalar identities over these formal words survive any consistent assignment of invertible operators, hence every tensor width. Ownership and legal native physical semantics remain inherited from the actual source.'} + encoded = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.write: + (HERE/'FORMAL-KERNEL.json').write_text(encoded) + else: + need(json.loads((HERE/'FORMAL-KERNEL.json').read_text()) == result, 'stable formal receipt') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/physical-zqy-scalar-span/independent_kernel.py b/research/physical-zqy-scalar-span/independent_kernel.py new file mode 100644 index 0000000000..39fc7e73f8 --- /dev/null +++ b/research/physical-zqy-scalar-span/independent_kernel.py @@ -0,0 +1,184 @@ +#!/usr/bin/env python3 +"""Generate a hidden-Y kernel independently, then verify original group rows. + +THU New Media Research Center; substantial OpenAI Codex assistance. Apache-2.0. + +This reads neither MODULE-CERTIFICATE.json nor search.py. It derives the +candidate without a saved kernel, then compares the derived rows with KERNEL.json. +Augmentation supplies only a candidate. The decisive check multiplies every +original actual-group history row by the candidate and cancels per group ID. +""" +from pathlib import Path +from fractions import Fraction as F +from hashlib import sha256 +from collections import Counter,defaultdict +from functools import lru_cache +import argparse,gzip,json,time,sys,struct +sys.dont_write_bytecode=True +HERE=Path(__file__).resolve().parent + +def require(ok,message): + if not ok:raise ValueError(message) + +def y_role(role):return role[0]=='L'and 112<=role[1]<224 + +def linear(columns,x): + y=0 + for j,col in enumerate(columns): + if x>>j&1:y^=col + return y + +def own_native(columns): + a=[sum(((columns[j]>>i)&1)<>j&1);a[j],a[pivot]=a[pivot],a[j];b[j],b[pivot]=b[pivot],b[j] + for i in range(9): + if i!=j and a[i]>>j&1:a[i]^=a[j];b[i]^=b[j] + require(a==[1<>i&1:row^=r + Q.append(row) + result=[] + for x in range(512): + y=linear(columns,x);bits=[i for i in range(9)if y>>i&1] + phase=sum((Q[i]>>i)&1 for i in bits)+2*sum((Q[i]>>j)&1 for i in bits for j in bits if i>2]>>2)+((a[v>>2]+v)&3)for v in b) +def conjugate(a):return tuple(4*(v>>2)+(-v%4)for v in a) +def inverse(a): + out=[None]*512 + for x,v in enumerate(a):out[v>>2]=4*x+(-v%4) + return tuple(out) + +def locate(runtime,relative,bare): + # Same-package default in a research checkout, or two exported input blobs. + for path in (runtime/'inputs'/bare,runtime/relative,runtime.parents[1]/relative): + if path.is_file():return path + raise ValueError('missing runtime input '+relative) + +def calculate(runtime,write=False): + started=time.monotonic();runtime=Path(runtime).resolve() + s=locate(runtime,'research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz','ACTUAL-WORD.json.gz') + p=locate(runtime,'research/native-rank8-helper-provider/WORD.json.gz','WORD.json.gz') + require(sha256(s.read_bytes()).hexdigest()=='7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05','source pin') + require(sha256(p.read_bytes()).hexdigest()=='7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc','provider pin') + canon=json.loads(gzip.decompress(s.read_bytes()))['canonical'];doc=json.loads(gzip.decompress(p.read_bytes()));require(doc['direction']=='backward','backward source') + operators=[tuple(4*x for x in range(512))];lookup={operators[0]:0} + def register(op): + if op not in lookup:lookup[op]=len(operators);operators.append(op) + return lookup[op] + warp={} + for w in canon['warps']: + forward=own_native(w['G_columns']);warp[w['op']]=register(conjugate(forward));warp[-w['op']]=register(conjugate(inverse(forward))) + @lru_cache(None) + def product(a,b):return register(compose(operators[a],operators[b])) + rows={('L',i):{(('L',i),0):F(1)}for i in range(632)};frames={('L',i):v for i,v in enumerate(canon['start'])};full={i for i,v in enumerate(canon['frames'])if len(v)==9} + require(full=={1}and canon['frames'][1]==[256,128,64,32,16,8,4,2,1],'standard full frame') + require(not any(v in full for v in frames.values()),'no initial full-frame fields') + def get(r): + if r not in rows:require(r[0]=='C','only owned additional roles');rows[r]={(r,0):F(1)};frames[r]=None + return rows[r] + histories=[];events=[];seen=set();counts=Counter() + for index,event in enumerate(doc['word']): + kind=event[0];counts[kind]+=1;touched=None + if kind=='scalar': + g,chart=event[1:];dst=tuple(g[1]);get(dst);touched=dst + if g[0]=='clear':require(dst[0]=='C','clear owned only');rows[dst]={};frames[dst]=chart + elif g[0]=='copy': + src=tuple(g[2]);get(src);require(dst[0]=='C'and not rows[dst]and frames[src]==chart,'copy owned zero at true chart');rows[dst]=dict(rows[src]);frames[dst]=chart + elif g[0]=='scale': + require(frames[dst]==chart,'scale chart');q=F(g[2],g[3]);rows[dst]={k:q*v for k,v in rows[dst].items()if q*v} + elif g[0]=='add': + src=tuple(g[2]);get(src);require(dst!=src and frames[src]==frames[dst]==chart,'ADD chart');q=F(g[3],g[4]) + for k,v in list(rows[src].items()): + z=rows[dst].get(k,F(0))+q*v + if z:rows[dst][k]=z + else:rows[dst].pop(k,None) + else:raise ValueError(g[0]) + elif kind=='warp': + _,role,op,before,after=event;dst=tuple(role);get(dst);require(frames[dst]==before,'warp chart');rows[dst]={(r,product(warp[op],a)):q for(r,a),q in rows[dst].items()};frames[dst]=after;touched=dst + elif kind=='climb': + dst=('L',event[2]);require(frames[dst]==event[3],'paid climb chart');frames[dst]=event[4];touched=dst + elif kind=='zero_retag': + dst=('L',event[1]);require(frames[dst]==event[2]and not rows[dst],'exact zero retag');frames[dst]=event[3];touched=dst + else:require(kind in ('phase','adapter'),'retained marker grammar') + if touched is not None and frames[touched]in full and rows[touched]: + tag=frozenset(rows[touched].items()) + if tag not in seen:seen.add(tag);histories.append(dict(rows[touched]));events.append({'event':index,'role':list(touched),'frame':frames[touched]}) + require(len(histories)==4891 and set(rows)=={('L',i)for i in range(632)}|{('C',i)for i in range(9)},'all632 and nine arbitrary owned source roles') + # Independent Fraction elimination on scalar augmentations. Y columns are + # always free variables; a pure-Y scalar constraint would reject the model. + basis={};aug_zero=0 + for history in histories: + augmented=defaultdict(F) + for(r,op),q in history.items():augmented[r]+=q + row={r:q for r,q in augmented.items()if q} + while row: + nonY=[r for r in row if not y_role(r)] + require(nonY,'augmentation has no constraint on independently arbitrary Y') + pivot=min(nonY);coefficient=row[pivot] + if pivot not in basis: + basis[pivot]={r:q/coefficient for r,q in row.items()};break + for r,q in basis[pivot].items(): + value=row.get(r,F(0))-coefficient*q + if value:row[r]=value + else:row.pop(r,None) + if not row:aug_zero+=1 + require(len(basis)==474,'independent augmentation rank') + # All unused nonY and all owned columns receive zero compensation. This is + # a scalar map with K_Y=I, not an inverse address-operator polynomial. + K={('L',i):({i-112:F(1)}if 112<=i<224 else{})for i in range(632)};K.update({('C',i):{}for i in range(9)}) + for pivot in sorted(basis,reverse=True): + vector=defaultdict(F) + for role,q in basis[pivot].items(): + if role!=pivot: + for j,value in K[role].items():vector[j]-=q*value + K[pivot]={j:q for j,q in vector.items()if q} + require(all(K['L',112+j]=={j:F(1)}for j in range(112)),'K_Y exactly identity') + require(all(not K['C',j]for j in range(9)),'source-owned dirt held fixed by the kernel') + require(all(K['L',j]=={j:F(1)}for j in range(112))and all(not K['L',j]for j in range(224,632)), + 'independently derived kernel is exactly delta X=delta Y, all helpers fixed') + declared=json.loads((runtime/'KERNEL.json').read_text()) + require(declared['original_input_roles']==632 and declared['free_Y_columns']==112 and len(declared['rows'])==632,'declared provider kernel shape') + declared_rows=[{int(j):F(q)for j,q in row}for row in declared['rows']] + require(all(declared_rows[i]==K['L',i]for i in range(632)), + 'independently derived kernel equals supplied small KERNEL rows') + def first_failure(kernel): + for index,row in enumerate(histories): + residual=defaultdict(F) + for(role,op),q in row.items(): + for j,value in kernel[role].items():residual[op,j]+=q*value + residual={key:q for key,q in residual.items()if q} + if residual:return {'history':index,'event':events[index],'first_nonzero_group_column':list(min(residual)),'coefficient':str(residual[min(residual)]),'residual_terms':len(residual)} + return None + require(first_failure(K)is None,'ORIGINAL actual signed-group H_j K = 0, per group element') + paired_terms=0 + for row in histories: + pairs=defaultdict(F) + for(role,op),q in row.items(): + if role[0]=='L'and role[1]<224:pairs[role[1]%112,op]+=q;paired_terms+=1 + require(not any(pairs.values()),'direct literal operator X_i plus Y_i cancellation') + # Actual failure witnesses, not just assertions about the rank algorithm. + wrong_y=dict(K);wrong_y['L',112]={};y_control=first_failure(wrong_y);require(y_control is not None,'wrong Y perturbation rejected') + role=next(r for r in sorted(K)if not y_role(r)and K[r]);j=next(iter(K[role]));wrong_N=dict(K);wrong_N[role]=dict(K[role]);wrong_N[role][j]+=1 + N_control=first_failure(wrong_N);require(N_control is not None,'wrong nonY compensation rejected') + no_N={r:(v if y_role(r)else{})for r,v in K.items()};no_N_control=first_failure(no_N);require(no_N_control is not None,'uncompensated original Y variation is visible') + encoded={'schema':'independent-scalar-hidden-Y-kernel/v1','Y_source_roles':list(range(112,224)),'original_input_rows':[{'role':list(r),'coefficients':[[j,str(q)]for j,q in sorted(K[r].items())]}for r in sorted(K)if r[0]=='L'],'owned_input_rows_zero':[list(r)for r in sorted(K)if r[0]=='C'],'definition':'delta logical input_r = sum_j K[r,j] deltaY_j; K_Y=I; every original actual-group full-frame history annihilates this map.'} + raw=json.dumps(encoded,indent=2,sort_keys=True)+'\n' + if write:(HERE/'KERNEL-INDEPENDENT.json').write_text(raw) + used={op for row in histories for role,op in row};base_digest=sha256(b''.join(sorted(struct.pack('<512H',*operators[i])for i in used))).hexdigest() + require(len(used)==59 and base_digest=='34ad3a3f37a53afd59e0d295d6dffa446819539b9ac46556ef51134eb888d831','independently replayed physical operator set binding') + result={'status':'PASS_INDEPENDENT_ORIGINAL_GROUP_HISTORY_HIDDEN_Y_KERNEL','method':'Own Fraction elimination of augmentation proposes scalar K; decisive independent verification is H_j K=0 in every actual group coefficient of every original replay row. No decomposition certificate, search import, modular calculation or width-one matrix-sum relation is used. The candidate is derived without reading saved kernel rows, then compared with KERNEL.json.','source_word_sha256':sha256(p.read_bytes()).hexdigest(),'source_payload_sha256':sha256(s.read_bytes()).hexdigest(),'full_frame_histories':4891,'original_history_group_terms':sum(len(row)for row in histories),'paired_X_Y_group_terms_checked':paired_terms,'original_independent_roles':632,'owned_entry_roles':9,'augmentation_nonY_rank':len(basis),'kernel_shape':'K=[I112;I112;0_408], and zero on all nine owned inputs','K_Y_identity_columns':112,'original_K_nonzero_entries':sum(len(v)for r,v in K.items()if r[0]=='L'),'nonzero_nonY_compensating_original_roles':sum(bool(v)and not y_role(r)for r,v in K.items()),'source_owned_compensation_is_zero':True,'actual_group_annihilation_checks':4891,'actual_observation_operator_count':len(used),'actual_observation_operator_set_sha256':base_digest,'kernel_sha256':sha256(raw.encode()).hexdigest(),'controls':{'wrong_Y_row':y_control,'wrong_nonY_compensation':N_control,'Y_variation_without_nonY_compensation':no_N_control,'supplied_original_Y0_identity_observation':{'non_annihilated_Y_column':0,'identity_operator_coefficient':'1'}},'all_width_reason':'Each exact signed group identity lifts by operator composition to every tensor width. H_j K=0 retains scalar owner coefficients outside tensor powers and does not use physical width-one linear relations.','theorem':'At every width, every original Y variation can be compensated by the same logical X variation, with all helpers and owned entries fixed, leaving every admitted full-frame history unchanged. Therefore no nonzero pure-Y linear observation lies in their module even under arbitrary address-End left coefficients; no deterministic postprocessing of only those snapshots can recover a nonconstant function of Y.','physical_chart_guard':'Logical source variables are converted to physical independent inputs by their invertible birth frames. All snapshots share the one full inverse-transpose Gaussian Phi. Right birth factors and common Phi preserve annihilation and the hidden-Y fiber; owned chart/precision execution remains inherited.','limits':'Only the unchanged frozen native full-frame snapshots. Separate reads of partial-frame/main Y, modified paid contacts/history or new supplied correlated observations are outside this theorem. Fixing helper or owned values alone does not evade this particular kernel, because it changes only X and Y. No paid lower bound, new caller or new kappa is asserted.','seconds':time.monotonic()-started} + return result + +if __name__=='__main__': + parser=argparse.ArgumentParser();parser.add_argument('--write',action='store_true');parser.add_argument('--runtime',type=Path,default=HERE,help='package containing KERNEL.json; sources found in its repository or inputs/');args=parser.parse_args();result=calculate(args.runtime,args.write);path=HERE/'INDEPENDENT-KERNEL-AUDIT.json' + if args.write:path.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + old=json.loads(path.read_text());old.pop('seconds');new=dict(result);new.pop('seconds');require(old==new,'stable independent kernel audit') + print(json.dumps({k:result[k]for k in ('status','full_frame_histories','augmentation_nonY_rank','K_Y_identity_columns','original_K_nonzero_entries','seconds')},sort_keys=True)) diff --git a/research/physical-zqy-scalar-span/verify_kernel.py b/research/physical-zqy-scalar-span/verify_kernel.py new file mode 100644 index 0000000000..036d1f199f --- /dev/null +++ b/research/physical-zqy-scalar-span/verify_kernel.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Read-only exact right-kernel check for the complete frozen full history. + +Replays the actual signed-native provider and checks H K = 0 by cancellation +of identical literal monomial operators, separately for every original-input +column. No discovery eliminator, finite-field rank test, width-one matrix-sum +identity, or operator-polynomial inverse is used. Apache-2.0; substantial +OpenAI Codex assistance for THU New Media Research Center (@thu-nmrc). +""" +from pathlib import Path +from fractions import Fraction as F +from hashlib import sha256 +import argparse, importlib.util, json, sys +HERE = Path(__file__).resolve().parent +KERNEL_SHA = 'ad403cdd98975ae9a8033afff5a86f96d055e44c5be19c1f171387cf26cd3b81' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def y_identity(kernel): + return all(kernel[112+j] == {j: F(1)} for j in range(112)) + + +def residual(row, kernel): + """Multiply one actual H row by scalar K, retaining literal operator IDs.""" + out = {} + for (role, operator), value in row.items(): + need(role[0] == 'L' and 0 <= role[1] < 632, + 'every observable depends only on the 632 original logical inputs') + for column, scalar in kernel[role[1]].items(): + key = column, operator + q = out.get(key, F(0)) + value * scalar + if q: + out[key] = q + else: + out.pop(key, None) + return out + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--runtime', type=Path, default=HERE) + ap.add_argument('--write', action='store_true', help='author the frozen result; default only compares') + args = ap.parse_args() + runtime = args.runtime.resolve() + need((runtime/'native.py').is_file() and (runtime/'monomial.py').is_file(), + 'actual native runtime directory') + sys.path.insert(0, str(runtime)) + import native as N + import monomial as M + raw = (HERE/'KERNEL.json').read_bytes() + need(sha256(raw).hexdigest() == KERNEL_SHA, 'frozen sparse kernel bytes') + certificate = json.loads(raw) + need(certificate['schema'] == 'native-full-history-Y-kernel/v1', 'kernel schema') + need(certificate['original_input_roles'] == 632 and certificate['free_Y_columns'] == 112, + 'kernel dimensions') + need(sha256((runtime/'native.py').read_bytes()).hexdigest() == certificate['source_native_sha256'], + 'source native interpreter pin') + need(sha256((runtime/'monomial.py').read_bytes()).hexdigest() == certificate['source_monomial_sha256'], + 'literal signed-monomial evaluator pin') + encoded_rows = certificate['rows'] + need(len(encoded_rows) == 632, 'one kernel row for every independent original input') + kernel = [] + for encoded in encoded_rows: + row = {} + for column, coefficient in encoded: + value = F(coefficient) + need(isinstance(column, int) and 0 <= column < 112 and column not in row and value, + 'unique nonzero scalar kernel entry') + row[column] = value + kernel.append(row) + need(y_identity(kernel), 'K_Y is exactly the identity: every original Y deformation is available') + need(kernel[:112] == kernel[112:224] and all(not row for row in kernel[224:]), + 'explicit K=(I,I,0): equal X/Y displacement and unchanged independent helpers') + + source, provider = N.read('source'), N.read('provider') + canon = source['canonical'] + N.initialize(canon) + histories, final, frames, full = N.native_replay(canon, provider['word'], True) + need(len(histories) == 4891, 'all distinct frozen backward full-frame histories') + need(len(N.operators) == 215, 'actual signed native operator registry') + literal_columns = [list(M.decode(op)) for op in N.operators] + need(all(len(columns) == 512 and len({v//4 for v in columns}) == 512 + and all(0 <= v < 2048 for v in columns) for columns in literal_columns), + 'every operator is an actual one-column signed monomial permutation') + need(len(set(N.operators)) == len(N.operators), 'literal operator canonicalization') + need(N.operators[0] == M.IDENTITY, 'literal identity index') + terms = 0 + active_terms = 0 + for j, row in enumerate(histories): + need(all(0 <= operator < len(N.operators) for role, operator in row), + 'every history term uses the fresh literal operator registry') + need(not residual(row, kernel), 'exact H K = 0 at history ' + str(j)) + terms += len(row) + active_terms += sum(bool(kernel[role[1]]) for role, operator in row) + need(terms == 119515, 'full actual-history term count') + + def extra_case(label, program, backward, case_kernel): + # A fresh module instance gives each source case its own authenticated + # literal registry, without changing the accepted runtime on disk. + spec = importlib.util.spec_from_file_location('kernel_native_' + label, runtime/'native.py') + fresh = importlib.util.module_from_spec(spec) + spec.loader.exec_module(fresh) + fresh.initialize(canon) + case_histories, _, _, _ = fresh.native_replay(canon, program, backward) + case_terms = sum(map(len, case_histories)) + case_active = 0 + for j, row in enumerate(case_histories): + need(not residual(row, case_kernel), 'exact ' + label + ' HK=0 at history ' + str(j)) + case_active += sum(bool(case_kernel[role[1]]) for role, operator in row) + columns = [list(M.decode(op)) for op in fresh.operators] + need(len(set(fresh.operators)) == len(fresh.operators), label + ' literal operator uniqueness') + return { + 'direction': 'raw backward' if backward else 'forward', + 'full_frame_histories': len(case_histories), 'history_exact_terms': case_terms, + 'history_terms_with_nonzero_kernel_row': case_active, + 'literal_group_operators': len(fresh.operators), + 'literal_decoded_operator_columns_sha256': sha256(json.dumps(columns, separators=(',', ':')).encode()).hexdigest(), + 'kernel_formula': 'K_X=I_112, K_Y=I_112, K_helpers=0_408x112' if backward else 'K_X=0_112x112, K_Y=I_112, K_helpers=0_408x112', + 'exact_HK_zero': True, + } + + forward_kernel = [{} for _ in range(112)] + [{j: F(1)} for j in range(112)] + [{} for _ in range(408)] + need(len(forward_kernel) == 632 and y_identity(forward_kernel), 'explicit forward kernel target freedom') + source_backward = extra_case('source_backward', source['programs']['backward'], True, kernel) + source_forward = extra_case('source_forward', source['programs']['forward'], False, forward_kernel) + need(source_backward['full_frame_histories'] == 5019 and source_backward['history_exact_terms'] == 80001, + 'frozen source-backward observation family') + need(source_forward['full_frame_histories'] == 4968 and source_forward['history_exact_terms'] == 94137, + 'frozen source-forward observation family') + + # Four controls test distinct proof obligations. These deliberately altered + # test objects are not claimed to be legal alternate native producers. + zero_kernel = [{} for _ in range(632)] + need(all(not residual(row, zero_kernel) for row in histories), 'zero-kernel test baseline') + control_target = not y_identity(zero_kernel) + need(control_target, 'control: the vacuous zero kernel must fail target freedom') + + missing = [dict(row) for row in kernel] + missing[0] = {} + missing_failures = [j for j, row in enumerate(histories) if residual(row, missing)] + need(missing_failures, 'control: deleting the X_0 compensator must expose a history') + + sign_index = next(j for j, row in enumerate(histories) + if any(role[1] < 112 for role, operator in row)) + corrupted = dict(histories[sign_index]) + term = next(key for key in corrupted if key[0][1] < 112) + corrupted[term] = -corrupted[term] + sign_residual = residual(corrupted, kernel) + need(sign_residual, 'control: changing one signed X observation term must break cancellation') + + side_observation = {(('L', 112), 0): F(1)} + side_residual = residual(side_observation, kernel) + need(side_residual, 'control: adding an original/lower-frame Y side observation must break the barrier') + + operator_digest = sha256(json.dumps(literal_columns, separators=(',', ':')).encode()).hexdigest() + result = { + 'schema': 'native-full-history-direct-scalar-kernel/v1', + 'status': 'PASS_EXACT_ALL_WIDTH_FULL_HISTORY_Y_BLINDNESS', + 'kernel_sha256': KERNEL_SHA, + 'source_native_sha256': certificate['source_native_sha256'], + 'source_monomial_sha256': certificate['source_monomial_sha256'], + 'source_inputs': {name: {'path': path, 'sha256': digest} + for name, (path, digest) in sorted(N.INPUTS.items())}, + 'direction': 'raw backward', + 'full_frame_histories': len(histories), + 'history_exact_terms': terms, + 'history_terms_with_nonzero_kernel_row': active_terms, + 'original_input_rows': 632, 'free_Y_columns': 112, + 'kernel_nonzero_rows': sum(bool(row) for row in kernel), + 'kernel_scalar_terms': sum(len(row) for row in kernel), + 'kernel_formula': 'K_X=I_112, K_Y=I_112, K_helpers=0_408x112', + 'literal_group_operators': len(N.operators), + 'literal_decoded_operator_columns_sha256': operator_digest, + 'cases': { + 'provider_backward': { + 'direction': 'raw backward', 'full_frame_histories': len(histories), + 'history_exact_terms': terms, 'history_terms_with_nonzero_kernel_row': active_terms, + 'literal_group_operators': len(N.operators), + 'literal_decoded_operator_columns_sha256': operator_digest, + 'kernel_formula': 'K_X=I_112, K_Y=I_112, K_helpers=0_408x112', + 'exact_HK_zero': True, + }, + 'source_backward': source_backward, + 'source_forward': source_forward, + }, + 'negative_controls': { + 'zero_kernel_passes_HK_but_fails_Y_identity': control_target, + 'deleted_X0_compensator': {'rejected': True, 'failing_histories': len(missing_failures), + 'first_failing_history': missing_failures[0]}, + 'one_signed_X_history_coefficient': {'rejected': True, 'history': sign_index, + 'residual_literal_terms': len(sign_residual)}, + 'original_Y_side_observation': {'rejected': True, 'residual_literal_terms': len(side_residual)} + }, + 'all_width_lift': 'Every coefficient of HK cancels between identical actual signed monomial operators, before numerical evaluation. Literal products and phase identities lift to every positive tensor width, with exterior scalar rational coefficients unchanged.', + 'information_consequence': 'For every logical original Y displacement v, displace logical original X by the same v in either backward case, or leave X unchanged in the source-forward case; leave all 408 independent helper inputs fixed. Every full-frame history is identical. Thus a decoder receiving only that complete history cannot determine a nonconstant Y-only function, even with arbitrary nonlinear postprocessing.', + 'physical_coordinates': 'Logical original-input coordinates are used. Each physical independent input differs by an invertible birth-chart right factor. Conjugating the input displacement by those factors preserves HK=0 and arbitrary variation of physical Y; this is not a claim that the physical input embedding is scalar-only or free.', + 'scope': 'Only the frozen #5402 raw-backward provider and original source-backward/source-forward full-frame observation families, each considered separately. The decoder is not also given lower-frame values, original inputs, new paid observations, or a changed producer. Source native, phase and compiler premises are inherited.', + 'width_one_matrix_sum_relations_used': False, + 'polynomial_operator_inverses_used': False, + 'module_factorization_required_at_runtime': False, + 'new_observation_or_kappa': False, + } + encoded = json.dumps(result, indent=2, sort_keys=True) + '\n' + if args.write: + (HERE/'KERNEL-RESULT.json').write_text(encoded) + else: + need(json.loads((HERE/'KERNEL-RESULT.json').read_text()) == result, + 'stable direct-kernel receipt differs') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main() From be292a4c2724a17c7401bb736f969e898c43f0f2 Mon Sep 17 00:00:00 2001 From: thu-nmrc Date: Sun, 25 Oct 2026 04:43:03 +0800 Subject: [PATCH 3/3] Correct recorded local Python patch version --- research/physical-zqy-scalar-span/VALIDATION.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/physical-zqy-scalar-span/VALIDATION.md b/research/physical-zqy-scalar-span/VALIDATION.md index 810cb59e6a..4ab1dbb85a 100644 --- a/research/physical-zqy-scalar-span/VALIDATION.md +++ b/research/physical-zqy-scalar-span/VALIDATION.md @@ -1,6 +1,6 @@ # Validation scope -Python 3.12.14, standard library only, macOS arm64. The current registered +Python 3.12.13, standard library only, macOS arm64. The current registered suite consists of eight commands. All eight pass on the kernel extension. Default replay compares frozen receipts and writes no package files.