diff --git a/research/fresh-stage-independent-audit/README.md b/research/fresh-stage-independent-audit/README.md new file mode 100644 index 0000000000..502832704d --- /dev/null +++ b/research/fresh-stage-independent-audit/README.md @@ -0,0 +1,121 @@ +# Independent review: retain the Q conjugations in the fresh-stage inverse bound + +The literal inverse extension in PR #5408's `PROOF.md` §1 is too broad: +“also applies to B_f^-1” must refer to **Q^(-tensor f) B_f^-1 Q^(tensor f)**. +We give a source-bound counterexample to the unconjugated wording and an +independent review of the corrected statement. The actual negative-bank +postdecoder in §6 already has the correct conjugations. + +For one stage, put `D_f = diag_i(K_i^(tensor f))`. Then + +``` +C_f^-1 = D_f^-1 (A^-1 ⊗ I) D_f, A^-1 = (A + 12I)/13. +``` + +Every row of this actual inverse has 53 nonzero owner coefficients. Computing +the first term with COPY/SCALE and adding the other 52 terms uses **5,824 ADDs +for every positive f**. Keep the normalized inputs and outputs in separate +owned banks, then apply the inverse monomial maps and clear scratch. The +literal claim would require 5,826 ADDs at `k=1, f=2925`. This is an exact +coefficient-program certificate and a written construction; it does not +materialize that enormous tensor or supply a physical finite-precision invoice. +The source already has its own smaller recoding recipe; our upper bound is +an independent witness, with no optimality claim. + +[REVIEW.md](REVIEW.md) checks the ordered fresh-stage factorization, the +nonzero path for every nonzero integer power, the four-entry conjugation, +and the support contraction. It records no further defect in §§2–6 under +the stated interface assumptions. [markers.py](markers.py) independently +builds local relations by joining literal row-dot signatures and propagates +constraints through the resulting layered graph. It recovers the sole owner +path for **all 13 saved certificates**, covering stage counts 1–9, 18, 19, 32 +and 64, and binds them to **all 16 saved negative banks**. These finite checks +corroborate the written all-length proof; a census through 64 is not that proof. + +The corrected conclusions remain `ADDs >= max(0,2f-24k)` for arbitrary fixed +fresh-stage length and at least `max(0,2f-6)` for each saved negative bank. +The per-bank bounds cannot be added, and the earlier two-stage offset-two +result remains stronger for its named banks. No new obstruction theorem, +new provider, improved κ, formal-kernel acceptance, or independent human +review is claimed. The current selected κ at our base is 0.003027288235; +this package does not change it or its five framework assumptions. + +## Evidence and reproduction + +Use Python 3.12 with the standard library, from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/fresh-stage-independent-audit --check-only +python3.12 -B scripts/research_package.py --package research/fresh-stage-independent-audit +python3.12 -I -O -B research/fresh-stage-independent-audit/verify.py +``` + +Expected marker: `PASS_INDEPENDENT_FRESH_STAGE_AUDIT_WITH_INVERSE_SCOPE_FINDING`. +The verifier authenticates 14 predecessor inputs, checks all 12,544 entries +of the exact code polynomial, 57,344 literal signed normalizer entries, and +512 conjugated columns and rows. It independently counts and reconstructs +marker paths, checks all actual bank words and nonzero coefficients, and +compares the full deterministic [RESULT.json](RESULT.json). +Controls cover a missing inverse diagonal term, tensor-powered owner scalars, +a fixed central vector, wrong Q orientation, empty/zero markers (53 paths), +an impossible marker endpoint (zero paths), zero powers, repeated stages, +and the wrong bank endpoint type. Neither predecessor checker nor proposer +is imported or run. The implementations share their source data, Python, +and the finite-state mathematical invariant; this is the stated limit of +computational independence. + +[VERIFICATION.md](VERIFICATION.md) records the actual normal/optimized replay, +source-history preflight and Git-free export checks. The saved endpoint and +its producer lineage remain premises. No full producer, compiler, outer, +selected cold, Lean or Docker replay was performed. + +## Assignment, overlap and scope + +We took the [explicit PR #5408 review handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19156413), +with the [canonical scoped claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19173519). +The source head is `256126eeb1607c0bf52996c3d90490f2b786b94a`; the package +starts from canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`. +[SOURCES.json](SOURCES.json) pins the actual committed bytes and retained +notices. [TASK.json](TASK.json) records the changed formal-interface card: +this is a written/executable interface review, without a proof-assistant build. + +The 04:46–04:48 UTC snapshot on 2026-10-25 covered 364 open PR bodies, +4,771 Discussion records and all 7,402 tracked local package/ledger notes. +The explicit review request and family thread were inspected. No competing +review appeared in that coverage; arbitrary diffs and unpublished work were +not searched. The existing numerical factor-cap follow-up was already +addressed by #5500; active precision/CRT claims were left separate. The +native-tensor least-width question would require a different result and was +not undertaken. The current picker was run once (seed +`bf5df56858d3ce7748b6d7c617abe1fe`, adversarial-audit suggestions); the explicit +review handoff supplied this bounded assignment. Baseline binding checks +are orientation only, not scientific acceptance. + +## Open next questions + +The concrete handoff is to retain the Q conjugations when restating the +inverse theorem or citing it in later decoder work. The frozen predecessor +is unchanged; this review supplies an explicit erratum and counterexample. + +A formalization of the corrected contraction-to-caller implication remains +open: begin with the single shared binary line, distinct private-stage +supports, and initially independent role coordinates, then connect an exact +marker-path certificate to row support. It would give proof-kernel checking +of the reviewed interface. No formal encoding or build is supplied here. +The source's paid-decoder and correlated-history questions remain open; +this review does not take over their existing claims. + +## Credit + +Prepared by Hiroki KUMAZAKI with substantial OpenAI Codex assistance, including +separate proof-review, marker-checker and counterexample-review subagents. +All reviewers are automated participants in the same session. + +Ali Romman / #5408 supplied the all-length theorem and marker certificates; +Dillon / #4933 supplied the physical normalizers and typed caller; +Cinna Davis / #5065 supplied the two-stage marker proof; Dugongue / #4929 +supplied the center-free code. Cao Yifan / intqwq, Cinna Davis / 1337isnot1337, +zxv, Jacob Alan Sussman, Ryanson Jonathan and the retained native/controller +lineage retain their credit. Source-specific NOTICE, LICENSE and ORIGINS +remain pinned and are included by the declared-input export. New review, +counterexample and independently implemented checks are Apache-2.0. diff --git a/research/fresh-stage-independent-audit/RESULT.json b/research/fresh-stage-independent-audit/RESULT.json new file mode 100644 index 0000000000..c5cf2f27d6 --- /dev/null +++ b/research/fresh-stage-independent-audit/RESULT.json @@ -0,0 +1,1854 @@ +{ + "authenticated_inputs": 14, + "complete_producer_replayed": false, + "inverse_scope_counterexample": { + "add_count_for_every_positive_tensor_width": 5824, + "incorrect_literal_lower_bound": 5826, + "incorrect_tensor_squared_coefficient": "1/676", + "inverse_formula": "A^-1=(A+12I)/13", + "inverse_nonzero_terms_per_owner": 53, + "large_tensor_materialized": false, + "matrix_polynomial_entries": 12544, + "omitted_diagonal_product_entry_0_1": "6/13", + "once_applied_owner_coefficient": "-1/26", + "scope": "Unconjugated B_f^-1 at k=1, a_1=1", + "witness_tensor_width": 2925 + }, + "marker_audit": { + "actual_negative_bank_count": 16, + "controls": { + "empty_marker_paths": 53, + "impossible_output": { + "changed_output_bit": 0, + "outputs": [ + 128640 + ], + "paths": 0 + }, + "repeated_stage_rejected": true, + "wrong_endpoint_type_rejected": true, + "zero_marker_paths": 53, + "zero_power_rejected": true + }, + "independence_limit": "separate code and transition construction; shared finite-state mathematical invariant, source data and Python", + "marker_certificates": [ + { + "central_masks": [ + 1, + 0 + ], + "complete_relation_edges": 80, + "constraint_rounds": 1, + "inputs": [ + 309 + ], + "markers": 1, + "outputs": [ + 290 + ], + "owners": [ + 0, + 1 + ], + "paths": 1, + "prefix_reachable_peak": 1, + "stages": 1, + "surviving_domain_sizes": [ + 1, + 1 + ] + }, + { + "central_masks": [ + 0, + 1, + 1 + ], + "complete_relation_edges": 91, + "constraint_rounds": 2, + "inputs": [ + 126614 + ], + "markers": 1, + "outputs": [ + 128641 + ], + "owners": [ + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 1, + "stages": 2, + "surviving_domain_sizes": [ + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 1, + 0, + 1, + 0 + ], + "complete_relation_edges": 238, + "constraint_rounds": 3, + "inputs": [ + 3899261 + ], + "markers": 1, + "outputs": [ + 3500402 + ], + "owners": [ + 0, + 1, + 0, + 1 + ], + "paths": 1, + "prefix_reachable_peak": 26, + "stages": 3, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 1, + 0, + 1, + 1, + 1 + ], + "complete_relation_edges": 2068, + "constraint_rounds": 2, + "inputs": [ + 506572403 + ], + "markers": 1, + "outputs": [ + 506044517 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 23, + "stages": 4, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 2, + 1, + 0, + 3, + 0, + 0 + ], + "complete_relation_edges": 1508, + "constraint_rounds": 2, + "inputs": [ + 833124451870, + 1265346890653 + ], + "markers": 2, + "outputs": [ + 832888131600, + 1265045820306 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1 + ], + "paths": 1, + "prefix_reachable_peak": 4, + "stages": 5, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 0, + 0, + 0, + 1, + 1, + 1, + 1 + ], + "complete_relation_edges": 371, + "constraint_rounds": 2, + "inputs": [ + 408929468020584 + ], + "markers": 1, + "outputs": [ + 400167869869937 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 1, + "stages": 6, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 2, + 2, + 0, + 2, + 0, + 3, + 2, + 1 + ], + "complete_relation_edges": 185, + "constraint_rounds": 2, + "inputs": [ + 49963241663044660, + 139458250462523461 + ], + "markers": 2, + "outputs": [ + 47172741147073581, + 142264281478921796 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "paths": 1, + "prefix_reachable_peak": 1, + "stages": 7, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 1, + 0, + 1, + 1, + 0, + 0, + 1, + 0, + 1 + ], + "complete_relation_edges": 633, + "constraint_rounds": 3, + "inputs": [ + 22574143951628378081 + ], + "markers": 1, + "outputs": [ + 21854119931960855023 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 25, + "stages": 8, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 3, + 0, + 3, + 0, + 0, + 3, + 1, + 2, + 1, + 1 + ], + "complete_relation_edges": 1413, + "constraint_rounds": 2, + "inputs": [ + 3269233485147391114919, + 4403999331618672021121 + ], + "markers": 2, + "outputs": [ + 3120937267758885349545, + 4550277929673967599758 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "paths": 1, + "prefix_reachable_peak": 9, + "stages": 9, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 1, + 2, + 1, + 3, + 2, + 3, + 2, + 3, + 2, + 2, + 2, + 3, + 1, + 3, + 2, + 1, + 0, + 0, + 3 + ], + "complete_relation_edges": 1611, + "constraint_rounds": 2, + "inputs": [ + 1910808833422019235783220062917221040555207, + 31138120231488384951815458939426290644375402 + ], + "markers": 2, + "outputs": [ + 2436180975508191661473333245521833073611465, + 32354959455843396658776706535292212231231869 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 2, + "stages": 18, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 1, + 0, + 3, + 2, + 1, + 3, + 1, + 0, + 2, + 0, + 1, + 2, + 3, + 3, + 2, + 0, + 3, + 2, + 3, + 3 + ], + "complete_relation_edges": 1561, + "constraint_rounds": 2, + "inputs": [ + 70541796919628375671566128214651723834380243, + 7254591141270298746910948977345352434546466706 + ], + "markers": 2, + "outputs": [ + 70368260887907869768462332338644318675059141, + 7255288063431933148133294877574589918408690059 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "paths": 1, + "prefix_reachable_peak": 9, + "stages": 19, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 4, + 3, + 2, + 0, + 5, + 3, + 1, + 2, + 1, + 3, + 1, + 3, + 0, + 0, + 5, + 6, + 5, + 5, + 1, + 7, + 0, + 7, + 1, + 2, + 7, + 5, + 3, + 7, + 3, + 3, + 7, + 1, + 5 + ], + "complete_relation_edges": 353, + "constraint_rounds": 2, + "inputs": [ + 90820347916622095582518564211431716385362683871828793962635448903515985308854, + 10473238722956155051163163647634649414165919268007979792005949676167568968016, + 138933692058999963102023854015813076970582531981952560053409013640878614458377 + ], + "markers": 3, + "outputs": [ + 94452985697486039956605139226392667465899586450859573343428431049616926335649, + 6858269628419596719445742088858170852359318188332713194368772370599540969798, + 143495594554338628409961492925093163987761029242687699744375586590868285499423 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 6, + "stages": 32, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + }, + { + "central_masks": [ + 1, + 2, + 3, + 2, + 2, + 1, + 0, + 2, + 2, + 0, + 2, + 2, + 2, + 0, + 0, + 1, + 3, + 2, + 0, + 1, + 2, + 1, + 0, + 2, + 0, + 1, + 2, + 1, + 3, + 0, + 1, + 1, + 1, + 1, + 0, + 3, + 0, + 1, + 3, + 3, + 3, + 3, + 1, + 1, + 3, + 0, + 0, + 1, + 2, + 1, + 3, + 3, + 2, + 3, + 2, + 0, + 1, + 2, + 2, + 0, + 1, + 3, + 1, + 1, + 3 + ], + "complete_relation_edges": 6323, + "constraint_rounds": 60, + "inputs": [ + 3343955490819597787952613139068032833544208852026367057145856864438779104667712000068790382824883088091813720035528484315720325081696655061336528118435375, + 7805584683125670274885243387008365246617964388761818552047635448596094037468158648266415105160820519742545074469325854219248677138452069352146598005629804 + ], + "markers": 2, + "outputs": [ + 3343961884039066594997558333214289813568491862637150133821734482051523076191979390690581505857489784572347073155187852268426357753429309995607163030159417, + 8121474799786516627786257427750825150934320181363805622384552346647095723269729049990937847858538604623435067050497827906824472277941323749250980614038395 + ], + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "paths": 1, + "prefix_reachable_peak": 41, + "stages": 64, + "surviving_domain_sizes": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ] + } + ], + "method": "literal row-dot signature joins, complete layered relations, chain arc consistency, exact DAG count", + "negative_banks": [ + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + -1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0 + ], + "role": 0, + "selected_path_coefficient": "1/52", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ] + ], + "stages": 2, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + -1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1 + ], + "role": 1, + "selected_path_coefficient": "-1/104", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ] + ], + "stages": 3, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1, + 0 + ], + "role": 2, + "selected_path_coefficient": "1/208", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ] + ], + "stages": 4, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 6, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27, + 25 + ], + "marker_count": 2, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1 + ], + "role": 3, + "selected_path_coefficient": "-1/416", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ], + [ + 25, + -1 + ] + ], + "stages": 5, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27, + 25, + 23 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "role": 4, + "selected_path_coefficient": "1/832", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ], + [ + 25, + -1 + ], + [ + 23, + -1 + ] + ], + "stages": 6, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 6, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27, + 25, + 23, + 21 + ], + "marker_count": 2, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "role": 5, + "selected_path_coefficient": "-1/1664", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ], + [ + 25, + -1 + ], + [ + 23, + -1 + ], + [ + 21, + -1 + ] + ], + "stages": 7, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "role": 6, + "selected_path_coefficient": "1/3328", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ], + [ + 25, + -1 + ], + [ + 23, + -1 + ], + [ + 21, + -1 + ], + [ + 19, + -1 + ] + ], + "stages": 8, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 6, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17 + ], + "marker_count": 2, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "role": 7, + "selected_path_coefficient": "-1/6656", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ], + [ + 25, + -1 + ], + [ + 23, + -1 + ], + [ + 21, + -1 + ], + [ + 19, + -1 + ], + [ + 17, + -1 + ] + ], + "stages": 9, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + 1, + -1 + ], + "decoder_execution_stages": [ + 1, + 0 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0 + ], + "role": 8, + "selected_path_coefficient": "1/52", + "source_word": [ + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 2, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 3, + 1, + 0 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1 + ], + "role": 9, + "selected_path_coefficient": "-1/104", + "source_word": [ + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 3, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + 1, + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 5, + 3, + 1, + 0 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1, + 0 + ], + "role": 10, + "selected_path_coefficient": "1/208", + "source_word": [ + [ + 5, + -1 + ], + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 4, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 6, + "decoder_execution_powers": [ + 1, + 1, + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 7, + 5, + 3, + 1, + 0 + ], + "marker_count": 2, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1 + ], + "role": 11, + "selected_path_coefficient": "-1/416", + "source_word": [ + [ + 7, + -1 + ], + [ + 5, + -1 + ], + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 5, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + 1, + 1, + 1, + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 9, + 7, + 5, + 3, + 1, + 0 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "role": 12, + "selected_path_coefficient": "1/832", + "source_word": [ + [ + 9, + -1 + ], + [ + 7, + -1 + ], + [ + 5, + -1 + ], + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 6, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 6, + "decoder_execution_powers": [ + 1, + 1, + 1, + 1, + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ], + "marker_count": 2, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1 + ], + "role": 13, + "selected_path_coefficient": "-1/1664", + "source_word": [ + [ + 11, + -1 + ], + [ + 9, + -1 + ], + [ + 7, + -1 + ], + [ + 5, + -1 + ], + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 7, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 3, + "decoder_execution_powers": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ], + "marker_count": 1, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "role": 14, + "selected_path_coefficient": "1/3328", + "source_word": [ + [ + 13, + -1 + ], + [ + 11, + -1 + ], + [ + 9, + -1 + ], + [ + 7, + -1 + ], + [ + 5, + -1 + ], + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 8, + "surviving_paths": 1 + }, + { + "conjugated_decoder_add_offset": 6, + "decoder_execution_powers": [ + -1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -1 + ], + "decoder_execution_stages": [ + 32, + 31, + 29, + 27, + 25, + 23, + 21, + 19, + 17, + 15, + 13, + 11, + 9, + 7, + 5, + 3, + 1, + 0 + ], + "marker_count": 2, + "owners": [ + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0, + 1, + 0 + ], + "role": 15, + "selected_path_coefficient": "1/44302336", + "source_word": [ + [ + 32, + 1 + ], + [ + 31, + -1 + ], + [ + 29, + -1 + ], + [ + 27, + -1 + ], + [ + 25, + -1 + ], + [ + 23, + -1 + ], + [ + 21, + -1 + ], + [ + 19, + -1 + ], + [ + 17, + -1 + ], + [ + 15, + -1 + ], + [ + 13, + -1 + ], + [ + 11, + -1 + ], + [ + 9, + -1 + ], + [ + 7, + -1 + ], + [ + 5, + -1 + ], + [ + 3, + -1 + ], + [ + 1, + -1 + ], + [ + 0, + 1 + ] + ], + "stages": 18, + "surviving_paths": 1 + } + ], + "normalizer_truth_table_entries": 57344, + "saved_certificate_count": 13, + "scope": "finite path isolation and nonzero coefficients for the Q-conjugated inverse decoder; no lower bound asserted for bare B inverse" + }, + "normalizers_and_conjugation": { + "conjugated_columns_and_rows": 512, + "fixed_central_vector_control_support": 1, + "four_entry_magnitude_squared": "1/4", + "literal_normalizer_entries": 57344, + "marker_orientation_columns": 512, + "wrong_outer_Q_orientation_rejected": true + }, + "proof_review": "REVIEW.md; written argument, not formal-kernel acceptance", + "selected_frontier_changed": false, + "status": "PASS_INDEPENDENT_FRESH_STAGE_AUDIT_WITH_INVERSE_SCOPE_FINDING" +} diff --git a/research/fresh-stage-independent-audit/REVIEW.md b/research/fresh-stage-independent-audit/REVIEW.md new file mode 100644 index 0000000000..16d32cc9d5 --- /dev/null +++ b/research/fresh-stage-independent-audit/REVIEW.md @@ -0,0 +1,242 @@ +# Independent audit of fresh-stage terminal separation + +This review concerns Sections 2–6 of Ali Romman's PR #5408, +`research/fresh-stage-code-separation`, at source head +`256126eeb1607c0bf52996c3d90490f2b786b94a`. The audit starts from canonical +main `32890bc5de034ab8fc93ac88ead7279a6a416d04` and leaves the frozen source +unchanged. It is an independently derived mathematical and executable review +with substantial OpenAI Codex assistance, not independent human review, +proof-kernel acceptance, or a new priority claim for the underlying theorem. + +**Outcome:** the fresh-stage argument proves the stated lower bound for +`J_f = Q^(-tensor f) B_f Q^(tensor f)`, and for the correspondingly conjugated +inverse. One sentence in source Section 1 incorrectly extends this bound to +the **bare** `B_f^-1`. The actual negative-bank decoder in Section 6 has the +required conjugation, so that application is unaffected by this finding. + +## 1. Finding: the bare inverse has a constant ADD implementation + +Source Section 1 says, “It also applies to B_f^-1”. Read literally, this is +false. The correct replacement is `Q^(-tensor f) B_f^-1 Q^(tensor f)`. + +For the allowed one-stage case, put `D_f = diag_i(K_i^(tensor f))`. Then + + C_f = D_f^-1 (A tensor I) D_f, + C_f^-1 = D_f^-1 (A^-1 tensor I) D_f, + A^-1 = (A + 12I)/13. + +The last equality follows by multiplying out `A(A+12I)=13I`. The frozen +112-by-112 matrix has zero diagonal and exactly 52 nonzero entries per row. +Thus each row of `A^-1` has 53 nonzero terms: its diagonal coefficient is +`12/13`, and its other coefficients are `+1/26` or `-1/26`. + +COPY the 112 inputs into an owned normalized bank and apply `D_f`. Keep a +separate 112-field output bank and one reusable scaled-term temporary. For +each output owner, COPY and SCALE its first term into its output field, then +accumulate its other 52 terms using 52 binary scalar ADDs. Preserve the +normalized inputs until all outputs have been formed. Apply `D_f^-1` to the +outputs, COPY them to their destinations, and CLEAR the owned scratch. +The two surrounding `D_f` maps are monomial address maps. This gives the exact +bare inverse using `112*52 = 5,824` ADDs for every positive `f`, in the same +owner-field scalar/monomial word model used by the source. No Gaussian gate +is used. The number of elementary tape operations or required arithmetic +precision is not asserted to be constant. + +At `k=1, f=2,925`, the erroneous extension would require +`2f-24k = 5,826` ADDs. The 5,824-ADD construction is a strict counterexample. +Its verification only needs the finite owner matrix and the signed monomial +normalizers; constructing an exponentially large tensor matrix is unnecessary. +Even without the source sparsity, dense mixing gives the width-independent +upper bound `112*111` ADDs. The source already supplies its own smaller +896-ADD code-evaluation recipe; 5,824 is an independently checked sufficient +upper bound, not a new or optimal recoding algorithm. + +This finding does not provide a cheap negative-bank decoder: that decoder is +`Q^(-tensor f) B_f^-1 Q^(tensor f)`. It also does not give a favorable recursive +invoice, address the physical realization of denominator 13, or alter kappa. + +## 2. Independent subgroup and path argument + +Write the address space as `W = E direct-sum V_1 ... direct-sum V_k`, where +`E=` is one-dimensional over `F2`. A member of `H_s` preserves `E+V_s` +and fixes every other private space pointwise. This preservation condition, +as well as the pointwise condition, matters in computing the intersection. + +An element common to `H_k` and the group supported on the earlier spaces +fixes every private basis vector: the earlier group fixes `V_k`, and `H_k` +fixes the other private spaces. Its image of `e` belongs both to `E+V_k` +and to `E+V_1+...+V_(k-1)`, hence to `E`. Invertibility forces that image +to be the sole nonzero vector `e`. The intersection is therefore trivial. + +From `F_k...F_1=F'_k...F'_1`, the quotient `(F'_k)^-1 F_k` lies in this +intersection. Remove the equal last factors and induct. This proves unique +ordered factorization without commuting any stages. It works in any chosen +order of distinct private blocks, but does not establish uniqueness for words +that revisit a block. Over a larger common space the intersection can be +nontrivial; over a field larger than `F2`, even its one-dimensional general +linear group need not be trivial. + +For fixed initial and final owners, equality of complete binary path maps +therefore implies equality of each local factor. At the last factor, cancel +the known final-owner normalizer on the left. Distinct values of `G_i e` +imply distinct `G_i`, so the previous owner is determined. Repeat backwards. +Thus different owner paths have distinct complete binary maps. This alone +does not claim that arbitrary sums of their matrix entries cannot cancel. +The coordinate contraction below supplies the needed stronger conclusion. + +## 3. Powers and the selected path + +The source polynomial gives `(A-I)(A+13I)=0`. Since its roots are distinct +and nonzero, the exact projectors + + P_1=(A+13I)/14, P_-13=(I-A)/14 + +give `A^a=P_1+(-13)^a P_-13` for every integer `a`, including negative ones. +Consequently `A^a=alpha_a A+(1-alpha_a)I`, with +`alpha_a=(1-(-13)^a)/14`. For a nonzero integer `a`, `(-13)^a` is never 1, +so `alpha_a` is nonzero. This also follows for `C_s,f` from its explicit +block-diagonal monomial conjugacy, with owner coefficients outside the tensor. + +At every stage choose the alternating owners `j_s=s mod 2`. Its off-diagonal +coefficient is `-alpha_(a_s)/2`, so its complete coefficient is nonzero for +all allowed powers. Its first local map sends `e` to a vector other than +`e`: otherwise the distinct port images of owners 0 and 1 would coincide. +That image is nonzero, so it has a nonzero component in the first private +space. All subsequent stages fix that component. The full selected map +therefore moves `e`, for both parities of `k`. Tiny nonzero coefficients cause +no issue in this exact argument; no finite-precision stability is inferred. + +## 4. Central conjugation and row support + +Let `M|x>=s(x)|Gx>` with `s(x)` in `{+1,-1}`. Set +`a=(1+i)/2`, `b=(1-i)/2`; then `Q=aI+bT_e` and `Q^-1=bI+aT_e`. +Using `ab=1/2`, `b^2=-i/2`, and `a^2=i/2` gives + + Q^-1 M Q |x> = (1/2)[s(x)|Gx> - i s(x+e)|Gx+Ge> + + i s(x)|Gx+e> + s(x+e)|Gx+Ge+e>]. + +Invertibility and `Ge!=e` imply that `Ge` and `e` are linearly independent +over `F2`. All four destinations are distinct, with coefficient modulus +`1/2`. The adjoint is `Q^-1 M^-1 Q`, and `G^-1e!=e`, so every row also has +exactly four entries. In particular its row absolute sum is 2 and row +Euclidean norm is 1. The support of each tensor-power row is exactly `4^f`. +These assertions apply to each selected monomial conjugate, not to the sum +over owner paths. + +For a fixed owner block, the tensor identity that is actually available is + + J_f = sum_path c_path (Q^-1 M_path Q)^(tensor f). + +It follows by composing tensor powers along each path before summing paths. +Replacing this expression by the tensor power of a width-one owner sum +would introduce different cross terms and is not used. + +## 5. Marker contraction and the ADD bound + +Every path map is orthogonal over `F2`. Its images of the `8k` private basis +vectors are orthonormal, so their span is nondegenerate of codimension one. +Its orthogonal complement has exactly one nonzero vector, namely the image +of `e`. Thus agreement on those private basis vectors determines the entire +map. This argument explicitly handles the characteristic-two setting; it +does not assume that an arbitrary codimension-one span is nondegenerate. + +Choose the selected map `G_*`. For each private basis vector `x_l`, set +`y_l=G_*x_l` and `ell_l(N)=(Q N Q^-1)[y_l,x_l]`. On a path term this is +the signed monomial entry at `(y_l,x_l)`, hence zero or `+1/-1`. All selected +entries are nonzero; every other path has at least one zero by the preceding +map determination and path uniqueness. Contracting `m=8k` tensor factors +therefore leaves exactly + + c_* eta (Q^-1 M_* Q)^(tensor (f-m)), eta in {+1,-1}. + +Each marker functional uses at most two output indices and two input indices +because each row and column of `Q` and `Q^-1` has support two. Fix an output +row on the remaining tensor factors. The contraction draws on at most `2^m` +original rows. If each original row has support at most `S`, projecting away +its marker input coordinates leaves at most `S` possible remaining input +coordinates. The union over the selected rows has at most `2^m S` elements; +the additional summation over marker input choices does not introduce an +extra factor `2^m`. Cancellation can only reduce this union. + +The isolated row has `4^(f-m)` entries. Therefore +`S >= 2^(2f-3m)` for `f>=m`. Initially each independent input or clean-workspace +row has support at most one. SCALE, monomial maps, COPY and CLEAR preserve +this maximum, and one binary ADD increases it by at most a factor two. +After `g` ADDs, `S<=2^g`, even with arbitrary owner mixing and workspace. +This gives `g>=max(0,2f-24k)`; when `f=max(0,2f-3m)`. The contraction is a mathematical certificate, not a free +instruction. Independent inputs, a linear input-independent schedule, binary +ADDs, and initially uncorrelated workspace are essential interface premises. +An unpriced correlated history or a paid nonmonomial operation is not covered. +For the constant-in-width exclusion, `k` is fixed independently of `f`. + +## 6. Binding the sixteen saved negative banks + +The frozen `GAUGE.json` lists negative roles 0 through 15, each with operator +`Q^-1 B_i D_i`. Their left-to-right code words contain distinct stages and +only exponents `+1/-1`; the lengths and supplied marker sizes are: + +| Negative roles | Stage count | Marker count | ADD offset | +| --- | ---: | ---: | ---: | +| 0, 8 | 2 | 1 | 3 | +| 1, 9 | 3 | 1 | 3 | +| 2, 10 | 4 | 1 | 3 | +| 3, 11 | 5 | 2 | 6 | +| 4, 12 | 6 | 1 | 3 | +| 5, 13 | 7 | 2 | 6 | +| 6, 14 | 8 | 1 | 3 | +| 7 | 9 | 2 | 6 | +| 15 | 18 | 2 | 6 | + +The finite-state certificate has a sufficient state: current owner and one +shared bit per marker. Before a stage, that stage's private input bits have +never been touched. After it, its prescribed private output bits will never +be touched again. No other historical data can affect the next local map. +Counting paths with nonnegative integer multiplicities thus loses no candidate. +Allowing every nonzero `A` edge and every diagonal is a superset of the support +of every `A^a`. If exactly one path survives these constraints, the alternating +path's nonzero coefficient proves isolation for all the allowed powers. +The independent checker in this package uses the local relation +`G_j(input)=G_i(output)` and a complete layered relation count; it does not +import the predecessor evaluator. Finite counts corroborate this invariant, +while the all-length subgroup and contraction arguments remain written proofs. + +For a word printed left to right, inversion reverses its algebraic factors +and negates their powers. Its execution order is therefore the printed order +with negated powers. Renaming the fresh private blocks in that order fixes +`e` and commutes with `Q`; it preserves the marker and support arguments. +This binds the length-specific certificates to the actual bank words, not +just to abstract positive powers of a repeated stage. + +If the required job is `Q^-1 D_i`, the unique linear postdecoder on an +arbitrary emitted bank is + + (Q^-1 D_i)(Q^-1 B_i D_i)^-1 = Q^-1 B_i^-1 Q. + +Invertibility of `D_i` justifies the cancellation. Independent additional +inputs cannot alter this restriction of an exact linear decoder; correlated +retained histories can. Thus each of the sixteen saved negative-bank +interfaces has the uniform bound `max(0,2f-6)`, with the stronger offsets +listed above. These lower bounds cannot be added across banks. + +The endpoint identity, fresh-stage embeddings, and original input interface +are inherited from the saved PR4933 caller. This review checks their supplied +data and their mathematical implication, not the complete native producer, +supplier, compiler, outer construction, or its arithmetic and movement bill. +There is no other finding in Sections 2–6 under these explicit premises. + +## Attribution and limits + +Ali Romman / PR5408 owns the reviewed fresh-stage separation and short-marker +result. Dillon / PR4933 supplied the normalizers, one-stage support argument +and typed caller; Cinna Davis / PR5065 supplied the two-stage predecessor; +Dugongue / PR4929 supplied the center-free code. The retained Cao Yifan / +intqwq, Cinna Davis / 1337isnot1337, zxv, Jacob Alan Sussman, Ryanson Jonathan, +and native/controller contributors retain their source credit and notices. +This package contributes the independent audit and the explicit bare-inverse +scope counterexample. It claims no original discovery of the inherited +polynomial, four-point identity, scalar code, or support-growth principle. +It supplies no new frontier value, full cost admission, human approval, or +formal proof acceptance. diff --git a/research/fresh-stage-independent-audit/SOURCES.json b/research/fresh-stage-independent-audit/SOURCES.json new file mode 100644 index 0000000000..3e92f186f7 --- /dev/null +++ b/research/fresh-stage-independent-audit/SOURCES.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/fresh-stage-code-separation/MARKERS.json", + "usage": "input", + "git_blob": "da17f5279a5cd7c8d1462a64d7a66fffb9345e30", + "sha256": "99a97d27084e3ec6df5dbe4e71ba8b7bbb9cf4c0f6af26a70e4de3aeb2da145d" + }, + { + "path": "research/fresh-stage-code-separation/PROOF.md", + "usage": "input", + "git_blob": "05250589174e598fc9e6aeb00b2f6b8c04de8db1", + "sha256": "aa8e61ca5232ad62cdeb35f671093953e7b9dede6f9e048418b6f8ff48ba5e0a" + }, + { + "path": "research/fresh-stage-code-separation/README.md", + "usage": "input", + "git_blob": "48ff1cede85d5108da77eded961baad6953a3fd8", + "sha256": "196f5ec2ff0d9520440a2a302e09207273e00a62049faf02a86a39cc8a934ef5" + }, + { + "path": "research/fresh-stage-code-separation/RESULT.json", + "usage": "input", + "git_blob": "11420b222f20048a4bc2bc269f258ec7eb517bfd", + "sha256": "2bf8dca075fc0a21e378a7d64649a3dc65cff5d54d62378c3c14b66b62671601" + }, + { + "path": "research/fresh-stage-code-separation/SOURCES.json", + "usage": "input", + "git_blob": "289aea3b2e24e0869e4258f30f432105d7d676d9", + "sha256": "9fa0352667e9161b1e0f0a3949edb59a24f21e80e95616e617f76bbd88223f27" + }, + { + "path": "research/fresh-stage-code-separation/TASK.json", + "usage": "input", + "git_blob": "e72549b291f07d3d721de16b299e2d4187a4a2f6", + "sha256": "1a8ba1087b46d0c26c66fcf3068397f839158e850ded3afc621d3e167a04cb80" + }, + { + "path": "research/fresh-stage-code-separation/inputs/CODE.json", + "usage": "input", + "git_blob": "03170f4a31f7a8a3db7228f1cd5a6fdcb32720ae", + "sha256": "8be7f3f073b7981ec91c6af43edff0ac8a89f4824ef6026ae758c287dd6c03d0" + }, + { + "path": "research/fresh-stage-code-separation/inputs/GAUGE.json", + "usage": "input", + "git_blob": "69877f15147153322451f72f7d8ba7879c2ff6be", + "sha256": "e99bb62b7d63136204374c4469a243f02a338ddcd26603dd7e56688ffe0bb331" + }, + { + "path": "research/fresh-stage-code-separation/inputs/GAUGE.md", + "usage": "input", + "git_blob": "13269f7b1f98535151de173477f9e7d9a0d81079", + "sha256": "09c4e86d99245734761569efd13473623ffdd857e9eae092bd7f54bfd2f42f06" + }, + { + "path": "research/fresh-stage-code-separation/inputs/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "research/fresh-stage-code-separation/inputs/NORMALIZERS.json", + "usage": "input", + "git_blob": "bca92c222c395d3d75c047fbb678f3cd0947c60f", + "sha256": "ae8aad06aa5d1811d725895b3ab5a4f4daa9dcdd88294aa0d5f723e78bb1e0da" + }, + { + "path": "research/fresh-stage-code-separation/inputs/NOTICE", + "usage": "input", + "git_blob": "985b6b1bc76dacd54a9cbe9897f3b659ae93c3a4", + "sha256": "317b1c5e040bab50ebfc3d0cdb3a47fc30e2f872a00895f563d7931749b1cc7b" + }, + { + "path": "research/fresh-stage-code-separation/inputs/ORIGINS.json", + "usage": "input", + "git_blob": "e18a033d4de1d997f55e84d1535fc6cde20424c4", + "sha256": "10cf47173ca238c32adb923daae7c1137c2e9c86c7066301d68fc74442b3f4d7" + }, + { + "path": "research/fresh-stage-code-separation/inputs/TERMINAL.md", + "usage": "input", + "git_blob": "213a1726761224d6f705b90affc52b6600c95676", + "sha256": "49e8f958e0a43f5d0b307dbef81c81076a55e83137563d7e620c608201d6dbcc" + } + ] +} diff --git a/research/fresh-stage-independent-audit/TASK.json b/research/fresh-stage-independent-audit/TASK.json new file mode 100644 index 0000000000..6900702820 --- /dev/null +++ b/research/fresh-stage-independent-audit/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent written proof and source-bound marker-to-bank review of PR5408, with an exact counterexample to its literal unconjugated inverse extension.", + "scope_change_reason": "An explicit open independent-review handoff was selected over the picker suggestions. This formal-interface card is narrowed to mathematical and executable checking before formalization; no proof-assistant theorem or acceptance is claimed.", + "bottleneck_link": "The terminal-decoder obstruction must have its exact Q-conjugated interface before later work can use it to reject a purported free adapter. This review corrects an overbroad inverse statement and independently verifies its actual sixteen-bank certificate binding, without changing the selected frontier.", + "budget_minutes": 60, + "stop_rule": "Stop after the written proof review, inverse scope counterexample, thirteen marker certificates and sixteen bank bindings; no new mechanism, producer cold replay, formal build or selected change.", + "outcome": "completed", + "evidence": "REVIEW.md, RESULT.json, verify.py, markers.py, VERIFICATION.md", + "author": "Hiroki KUMAZAKI", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate automated proof-review, marker-checker and counterexample-review subagents in this session. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Can the corrected Q-conjugated all-length contraction and marker-to-caller implication be formalized with its fresh-stage and independent-input hypotheses?", + "why_it_matters": "It would make the reviewed interface proof kernel-checkable without expanding the claim to unconjugated codes or correlated histories.", + "first_step": "Encode ordered local binary maps on one common line and disjoint private spaces, then formalize the contraction support union bound and bind one exact marker certificate.", + "blocked_by": "No formal encoding or proof-assistant build is supplied; producer/outer admission remains a separate obligation." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19173519", + "source_pr": { + "number": 5408, + "head": "256126eeb1607c0bf52996c3d90490f2b786b94a" + } +} diff --git a/research/fresh-stage-independent-audit/VERIFICATION.md b/research/fresh-stage-independent-audit/VERIFICATION.md new file mode 100644 index 0000000000..d8547f777a --- /dev/null +++ b/research/fresh-stage-independent-audit/VERIFICATION.md @@ -0,0 +1,50 @@ +# Verification record + +Environment: CPython 3.12.13, Linux x86_64, standard library only, 2026-10-25. +The working base is canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`. +The publication refresh retained that main and the reviewed PR5408 head +`256126eeb1607c0bf52996c3d90490f2b786b94a`; relevant guidance, selected record +and predecessor source bytes had not changed. + +The following checks passed: + +```sh +python3.12 -B scripts/research_package.py --package research/fresh-stage-independent-audit --check-only +python3.12 -B scripts/research_package.py --package research/fresh-stage-independent-audit +python3.12 -I -O -B research/fresh-stage-independent-audit/verify.py +python3.12 -B scripts/check_research_commit.py --package research/fresh-stage-independent-audit --check-source-history +python3.12 -B scripts/export_research_package.py export --package research/fresh-stage-independent-audit --output /tmp/imb-fresh-stage-audit.tar +python3.12 -B scripts/export_research_package.py check /tmp/imb-fresh-stage-audit.tar +``` + +The committed-byte/source-history check is a transport/provenance check, not +mathematical acceptance. The export was extracted with Python's `data` tar +filter into a fresh directory outside the checkout. Using the absolute Python +interpreter path with `PATH=/nonexistent`, empty `PYTHONPATH`, and `-I -O -B`, +its exported `verify.py` passed without Git or predecessor evaluator imports. +The normal registered replay and optimized Git-free replay both compared the +complete receipt exactly. The package uses explicit exceptions, not Python +assertions, for proof-relevant checks. + +The result includes the 5,824-versus-5,826 bare-inverse counterexample, +12,544 exact matrix-polynomial entries, 57,344 signed normalizer entries, +512 four-entry conjugated rows/columns, all 13 saved marker certificates, +all 16 negative-bank bindings, exact surviving coefficients, and the semantic +controls enumerated in README.md. The full all-length proof is the written +argument reviewed in REVIEW.md; the finite certificate is not a proof of +unbounded length by enumeration. No exponentially large tensor was built. + +Submission overlap refresh completed at 05:05:08 UTC. It covered 369 open +PR bodies, 4,773 Discussion records and every one of the base's 7,402 tracked +local notes (plus this package's two then-untracked notes). All pagination +and local-inventory coverage fields were complete, with no warnings. The +relevant matches were the original handoff, its source completion, repeated- +stage follow-up #5412, and our own claim/pointer; no competing independent +review appeared. Arbitrary diffs and unpublished work remain outside coverage. + +Substantial AI assistance includes separate automated proof review, +independently implemented marker relations, and an adversarial review of the +counterexample and its allowed instruction model. These are not independent +human review or proof-kernel acceptance. No source producer, native/compiler, +outer, selected cold, Lean or Docker replay was run. Hosted CI is separate +from this local record and is reported on the pull request. diff --git a/research/fresh-stage-independent-audit/VERIFY.json b/research/fresh-stage-independent-audit/VERIFY.json new file mode 100644 index 0000000000..1434d19967 --- /dev/null +++ b/research/fresh-stage-independent-audit/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fresh-stage-code-separation/MARKERS.json", + "research/fresh-stage-code-separation/PROOF.md", + "research/fresh-stage-code-separation/README.md", + "research/fresh-stage-code-separation/RESULT.json", + "research/fresh-stage-code-separation/SOURCES.json", + "research/fresh-stage-code-separation/TASK.json", + "research/fresh-stage-code-separation/inputs/CODE.json", + "research/fresh-stage-code-separation/inputs/GAUGE.json", + "research/fresh-stage-code-separation/inputs/GAUGE.md", + "research/fresh-stage-code-separation/inputs/LICENSE", + "research/fresh-stage-code-separation/inputs/NORMALIZERS.json", + "research/fresh-stage-code-separation/inputs/NOTICE", + "research/fresh-stage-code-separation/inputs/ORIGINS.json", + "research/fresh-stage-code-separation/inputs/TERMINAL.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact inverse-scope counterexample, signed normalizers and Q orientation, independent layered-constraint audit of thirteen marker certificates and all sixteen negative banks, semantic controls and full deterministic receipt." + } + ] +} diff --git a/research/fresh-stage-independent-audit/markers.py b/research/fresh-stage-independent-audit/markers.py new file mode 100644 index 0000000000..ec10533247 --- /dev/null +++ b/research/fresh-stage-independent-audit/markers.py @@ -0,0 +1,266 @@ +"""Independent marker audit through a joined, layered constraint graph. + +Hiroki KUMAZAKI, with substantial OpenAI Codex assistance. Apache-2.0. + +run(source) reads the authenticated predecessor package supplied by the caller. +It imports neither the proposer nor either predecessor dynamic program. Local +relations are built by joining G_j(input)=G_i(output), using literal G_rows. +Arc consistency retains precisely the source-to-terminal paths of this chain; +an exact DAG count and explicit surviving owner sequence complete the check. +The finite-state invariant is shared mathematics, not independent human review. +""" +from collections import defaultdict +from fractions import Fraction +from functools import lru_cache +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def row_image(rows, value): + return sum(((row & value).bit_count() % 2) << bit + for bit, row in enumerate(rows)) + + +def load_tables(ports): + need(len(ports) == 112, "all 112 source normalizers") + forward, inverse = [], [] + for owner, port in enumerate(ports): + rows = port['G_rows'] + need(port['port'] == owner and len(rows) == 9 + and all(type(row) is int and 0 <= row < 512 for row in rows), + "literal nine-axis source rows") + table = tuple(row_image(rows, x) for x in range(512)) + need(len(set(table)) == 512, "each literal source map is invertible") + back = [0]*512 + for x, y in enumerate(table): + back[y] = x + forward.append(table) + inverse.append(tuple(back)) + return forward, inverse + + +def chain_images(forward, inverse, owners, inputs): + values = list(inputs) + for stage, (left, right) in enumerate(zip(owners, owners[1:])): + shift = 1+8*stage + for position, value in enumerate(values): + local = (value & 1) | (((value >> shift) & 255) << 1) + image = inverse[right][forward[left][local]] + values[position] = ((value & ~(1 | (255 << shift))) + | (image & 1) | ((image >> 1) << shift)) + return values + + +def central_mask(values): + return sum((value & 1) << i for i, value in enumerate(values)) + + +def joined_layers(forward, allowed, count, inputs, outputs): + """Build complete relations, including unreachable states, by signature join.""" + multiplicity = 1 << len(inputs) + layers = [] + for stage in range(count): + shift = 1+8*stage + source_private = [(x >> shift) & 255 for x in inputs] + target_private = [(x >> shift) & 255 for x in outputs] + target_signatures = defaultdict(list) + for owner, table in enumerate(forward): + for mask in range(multiplicity): + signature = tuple(table[(value << 1) | ((mask >> i) & 1)] + for i, value in enumerate(target_private)) + target_signatures[signature].append(owner*multiplicity+mask) + edges = [] + for owner, table in enumerate(forward): + for mask in range(multiplicity): + signature = tuple(table[(value << 1) | ((mask >> i) & 1)] + for i, value in enumerate(source_private)) + for target in target_signatures.get(signature, ()): + if allowed[target//multiplicity][owner]: + edges.append((owner*multiplicity+mask, target)) + layers.append(tuple(edges)) + return layers + + +def inspect_graph(layers, start, finish, multiplicity, total_owners=112): + """Count paths in the complete graph after chain-constraint propagation.""" + count = len(layers) + universe = set(range(total_owners*multiplicity)) + domains = [{start}]+[set(universe) for _ in range(count-1)]+[{finish}] + changed, rounds = True, 0 + while changed: + changed = False + rounds += 1 + for stage, edges in enumerate(layers): + surviving = [(left, right) for left, right in edges + if left in domains[stage] and right in domains[stage+1]] + source_domain = {left for left, _ in surviving} + target_domain = {right for _, right in surviving} + if domains[stage] != source_domain or domains[stage+1] != target_domain: + changed = True + domains[stage], domains[stage+1] = source_domain, target_domain + adjacency = [] + for stage, edges in enumerate(layers): + by_source = defaultdict(list) + for left, right in edges: + if left in domains[stage] and right in domains[stage+1]: + by_source[left].append(right) + adjacency.append({left: tuple(sorted(rights)) for left, rights in by_source.items()}) + + @lru_cache(None) + def completions(stage, state): + if stage == count: + return int(state == finish) + return sum(completions(stage+1, right) + for right in adjacency[stage].get(state, ())) + + path_count = completions(0, start) if start in domains[0] else 0 + witness = [] + if path_count == 1: + state = start + witness.append(state) + for stage in range(count): + choices = [right for right in adjacency[stage].get(state, ()) + if completions(stage+1, right)] + need(len(choices) == 1, "one successor on the recovered unique path") + state = choices[0] + witness.append(state) + need(state == finish and all(len(domain) == 1 for domain in domains), + "arc-consistent domains recover the sole complete witness") + # This is a node-reachability count, separately checking the saved peak field. + reachable, peak = {start}, 1 + for edges in layers: + reachable = {right for left, right in edges if left in reachable} + peak = max(peak, len(reachable)) + return { + 'paths': path_count, + 'owners': [state//multiplicity for state in witness], + 'central_masks': [state % multiplicity for state in witness], + 'complete_relation_edges': sum(map(len, layers)), + 'constraint_rounds': rounds, + 'prefix_reachable_peak': peak, + 'surviving_domain_sizes': [len(domain) for domain in domains], + } + + +def audit_markers(forward, inverse, allowed, count, inputs, outputs=None): + need(type(count) is int and count > 0, "positive fresh stage count") + need(all(type(x) is int and 0 <= x < 1 << (8*count+1) for x in inputs), + "marker inputs have exactly the declared shared/private geometry") + owners = [stage % 2 for stage in range(count+1)] + expected = chain_images(forward, inverse, owners, inputs) + outputs = expected if outputs is None else outputs + need(len(outputs) == len(inputs) and all(type(x) is int and 0 <= x < 1 << (8*count+1) + for x in outputs), "marker output domain") + multiplicity = 1 << len(inputs) + layers = joined_layers(forward, allowed, count, inputs, outputs) + report = inspect_graph(layers, central_mask(inputs), + (count % 2)*multiplicity+central_mask(outputs), multiplicity) + report.update(stages=count, inputs=list(inputs), outputs=list(outputs), markers=len(inputs)) + return report + + +def bank_word(bank): + word = bank['code_word_left_to_right'] + need(type(word) is list and word and all( + type(term) is list and len(term) == 2 and type(term[0]) is int and term[0] >= 0 + and type(term[1]) is int and term[1] != 0 for term in word), + "nonempty bank word with nonzero integer powers") + stages = [stage for stage, _ in word] + need(len(set(stages)) == len(stages), "distinct actual fresh private stages") + need(type(bank['central_exponent']) is int and bank['central_exponent'] == -1 + and bank['operator'] == 'Q^-1 B D' + and bank['gaussian_stages'] == stages + and bank['plain_gaussian_after_free_postdecode'] is False, + "actual negative-bank endpoint type") + return word + + +def rejected(call): + try: + call() + except ValueError: + return True + raise ValueError("expected malformed bank rejection") + + +def run(source: Path): + source = Path(source) + code = json.loads((source/'inputs/CODE.json').read_text()) + normalizers = json.loads((source/'inputs/NORMALIZERS.json').read_text()) + gauge = json.loads((source/'inputs/GAUGE.json').read_text()) + saved = json.loads((source/'MARKERS.json').read_text()) + a = [[Fraction(value) for value in row] for row in code['A']] + need(len(a) == 112 and all(len(row) == 112 for row in a), "source coefficient dimensions") + forward, inverse = load_tables(normalizers['ports']) + # Include diagonals even when their particular source power has zero weight: + # isolation in this larger graph is sufficient for every nonzero integer power. + allowed = [[i == j or a[i][j] != 0 for j in range(112)] for i in range(112)] + certificates, by_length = [], {} + for candidate in saved['candidates']: + count, inputs = candidate['stages'], candidate['markers'] + need(count not in by_length and type(inputs) is list and inputs, "distinct saved marker records") + report = audit_markers(forward, inverse, allowed, count, inputs) + need(report['paths'] == candidate['count'] == 1 + and report['prefix_reachable_peak'] == candidate['peak'], "saved count and reachable-peak claims") + need(report['owners'] == [stage % 2 for stage in range(count+1)], + "unique witness is the actual alternating owner chain") + need(chain_images(forward, inverse, report['owners'], [1])[0] != 1, + "isolated source path moves the shared central line") + certificates.append(report) + by_length[count] = report + need(sorted(by_length) == [1, 2, 3, 4, 5, 6, 7, 8, 9, 18, 19, 32, 64], + "all thirteen frozen marker certificates are checked") + + banks = [] + negatives = [bank for bank in gauge['typed_caller']['endpoint'] if bank['central_exponent'] == -1] + need([bank['role'] for bank in negatives] == list(range(16)), "all sixteen actual negative banks") + for bank in negatives: + word = bank_word(bank) + report = by_length[len(word)] + powers = [-power for _, power in word] + coefficient = Fraction(1) + for step, power in enumerate(powers): + alpha = (1-Fraction(-13)**power)/14 + need(alpha != 0, "each inverse-decoder power has a nonzero off-diagonal coefficient") + coefficient *= alpha*a[report['owners'][step+1]][report['owners'][step]] + need(coefficient != 0, "recovered owner path has nonzero exact source coefficient") + banks.append({'role': bank['role'], 'source_word': word, + 'decoder_execution_stages': [stage for stage, _ in word], + 'decoder_execution_powers': powers, 'stages': len(word), + 'marker_count': report['markers'], 'surviving_paths': report['paths'], + 'owners': report['owners'], 'selected_path_coefficient': str(coefficient), + 'conjugated_decoder_add_offset': 3*report['markers']}) + + empty = audit_markers(forward, inverse, allowed, 2, []) + zero = audit_markers(forward, inverse, allowed, 2, [0]) + need(empty['paths'] == zero['paths'] > 1, "empty and zero markers fail to isolate") + source_marker = by_length[2]['inputs'] + source_output = by_length[2]['outputs'] + impossible = None + for bit in range(17): + altered = source_output[:] + altered[0] ^= 1 << bit + result = audit_markers(forward, inverse, allowed, 2, source_marker, altered) + if result['paths'] == 0: + impossible = {'changed_output_bit': bit, 'outputs': altered, 'paths': 0} + break + need(impossible is not None, "perturbed literal endpoint admits no complete path") + bad_power = dict(negatives[0], code_word_left_to_right=[[32, 0], [31, -1]]) + repeated_stage = dict(negatives[0], code_word_left_to_right=[[32, 1], [32, -1]], gaussian_stages=[32, 32]) + wrong_type = dict(negatives[0], operator='B^-1') + controls = {'empty_marker_paths': empty['paths'], 'zero_marker_paths': zero['paths'], + 'impossible_output': impossible, + 'zero_power_rejected': rejected(lambda: bank_word(bad_power)), + 'repeated_stage_rejected': rejected(lambda: bank_word(repeated_stage)), + 'wrong_endpoint_type_rejected': rejected(lambda: bank_word(wrong_type))} + return {'marker_certificates': certificates, 'negative_banks': banks, 'controls': controls, + 'normalizer_truth_table_entries': 112*512, + 'saved_certificate_count': len(certificates), 'actual_negative_bank_count': len(banks), + 'method': 'literal row-dot signature joins, complete layered relations, chain arc consistency, exact DAG count', + 'scope': 'finite path isolation and nonzero coefficients for the Q-conjugated inverse decoder; no lower bound asserted for bare B inverse', + 'independence_limit': 'separate code and transition construction; shared finite-state mathematical invariant, source data and Python'} diff --git a/research/fresh-stage-independent-audit/verify.py b/research/fresh-stage-independent-audit/verify.py new file mode 100644 index 0000000000..e4b76101d3 --- /dev/null +++ b/research/fresh-stage-independent-audit/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Independent source/operator and inverse-scope audit; Python 3.12 stdlib. + +Hiroki KUMAZAKI, with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor verifier is imported or executed. See REVIEW.md for the proof. +""" +from collections import Counter +from fractions import Fraction as F +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / 'research/fresh-stage-code-separation' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate(): + manifest = json.loads((HERE / 'SOURCES.json').read_text()) + count = 0 + for entry in manifest['files']: + if entry['usage'] == 'input': + raw = (ROOT / entry['path']).read_bytes() + require(hashlib.sha256(raw).hexdigest() == entry['sha256'], + 'Source byte mismatch: ' + entry['path']) + count += 1 + return count + + +def apply_rows(rows, x): + return sum(((row & x).bit_count() % 2) << j for j, row in enumerate(rows)) + + +def monomials(): + ports = json.loads((SOURCE / 'inputs/NORMALIZERS.json').read_text())['ports'] + require(len(ports) == 112, '112 source normalizers') + tables = [] + for i, port in enumerate(ports): + rows, z = port['G_rows'], port['Z_mask'] + require(port['port'] == i and len(rows) == 9, 'Ordered nine-axis ports') + require(all(type(r) is int and 0 <= r < 512 for r in rows), 'Binary rows') + require(type(z) is int and 0 <= z < 512, 'Binary sign mask') + require(all((rows[r] & rows[s]).bit_count() % 2 == (r == s) + for r in range(9) for s in range(9)), 'Orthogonal row Gram matrix') + require(apply_rows(rows, 1) == port['q'], 'Central image binding') + require(port['K_word'] == [['P', rows], ['D', [0]*9, [2*((z >> j) & 1) for j in range(9)]]], + 'Literal signed P then D normalizer') + table = [] + for x in range(512): + # Evaluate the literal word with a Z/4 phase accumulator. + y, phase = x, 0 + for instruction in port['K_word']: + if instruction[0] == 'P': + y = apply_rows(instruction[1], y) + else: + require(instruction[1] == [0]*9, 'No quadratic phase in K') + phase += sum(c*((y >> j) & 1) for j, c in enumerate(instruction[2])) + require(phase % 2 == 0, 'Real signed normalizer') + sign = (1, -1)[(phase // 2) % 2] + require(sign == (-1)**((z & y).bit_count() % 2), 'Exact output phase') + table.append((y, sign)) + require(len({y for y, _ in table}) == 512, 'Bijection') + tables.append(table) + require(len({p['q'] for p in ports}) == 112, 'Distinct central images') + return tables + + +def inverse(table): + out = [None]*len(table) + for x, (y, sign) in enumerate(table): + out[y] = (x, sign) + require(all(v is not None for v in out), 'Monomial inverse domain') + return out + + +def gadd(a, b): + return a[0]+b[0], a[1]+b[1] + + +def gmul(a, b): + return a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0] + + +def put(out, y, value): + out[y] = gadd(out.get(y, (F(0), F(0))), value) + if out[y] == (0, 0): + del out[y] + + +def q_column(vector, backwards=False): + sign = -1 if backwards else 1 + out = {} + for x, c in vector.items(): + put(out, x, gmul(c, (F(1, 2), F(sign, 2)))) + put(out, x ^ 1, gmul(c, (F(1, 2), F(-sign, 2)))) + return out + + +def m_column(table, vector): + out = {} + for x, c in vector.items(): + y, sign = table[x] + put(out, y, (sign*c[0], sign*c[1])) + return out + + +def geometry(tables): + inv = inverse(tables[1]) + path = [] + for y, s in tables[0]: + z, t = inv[y] + path.append((z, s*t)) + require(path[1][0] != 1, 'Alternating first transition moves e') + rows = Counter() + for x in range(512): + basis = {x: (F(1), F(0))} + n = q_column(m_column(path, q_column(basis)), backwards=True) + require(len(n) == 4, 'Conjugated column has four entries') + for y, c in n.items(): + require(c[0]**2 + c[1]**2 == F(1, 4), 'Four exact magnitudes 1/2') + rows[y] += 1 + # Independent sparse multiplication of Q (Q^-1 M Q) Q^-1. + recovered = q_column(q_column(m_column(path, + q_column(q_column(basis, backwards=True))), backwards=True)) + require(recovered == m_column(path, basis), 'Marker conjugation orientation') + fixed = q_column(q_column(basis), backwards=True) + require(fixed == basis, 'Ge=e identity control has one entry, not four') + require(set(rows.values()) == {4} and len(rows) == 512, 'Four entries in every row') + basis = {0: (F(1), F(0))} + wrong = q_column(q_column(m_column(path, + q_column(q_column(basis, backwards=True))), backwards=True), backwards=True) + require(wrong != m_column(path, basis), 'Wrong outer Q orientation is detected') + return {'literal_normalizer_entries': 112*512, + 'conjugated_columns_and_rows': 512, + 'four_entry_magnitude_squared': '1/4', + 'marker_orientation_columns': 512, + 'fixed_central_vector_control_support': 1, + 'wrong_outer_Q_orientation_rejected': True} + + +def inverse_counterexample(): + raw = json.loads((SOURCE / 'inputs/CODE.json').read_text())['A'] + a = [[F(x) for x in row] for row in raw] + n = len(a) + require(n == 112 and all(len(row) == n for row in a), '112 square code') + require(all(a[i][i] == 0 for i in range(n)), 'Zero diagonal') + require(a[0][1] == a[1][0] == F(-1, 2), 'Alternating edge coefficient') + require(all((2*x).denominator == 1 for row in a for x in row), 'Integral doubled code') + b = [[int(2*x) for x in row] for row in a] + # B=2A: B^2+24B=52I checks A(A+12I)/13=I exactly. + for i in range(n): + for j in range(n): + square = sum(b[i][t]*b[t][j] for t in range(n)) + require(square+24*b[i][j] == 52*(i == j), 'Exact inverse polynomial') + ainv = [[F(b[i][j]+24*(i == j), 26) for j in range(n)] for i in range(n)] + # Compile and symbolically execute scalar owner mixing in normalized coordinates. + # A first nonzero term uses COPY+SCALE; each additional term uses one ADD. + adds, row_terms = 0, [] + for row in ainv: + terms = [(j, c) for j, c in enumerate(row) if c] + require(bool(terms), 'Nonempty inverse row') + state = {terms[0][0]: terms[0][1]} + for j, c in terms[1:]: + state[j] = state.get(j, F(0))+c + adds += 1 + require([state.get(j, F(0)) for j in range(n)] == row, 'Exact symbolic ADD program') + row_terms.append(len(terms)) + require(set(row_terms) == {53} and adds == 5824, 'Source sparse inverse bill') + width = (adds+24)//2+1 + alleged = 2*width-24 + require(width == 2925 and alleged == 5826 and alleged > adds, 'Literal inverse contradiction') + # Removing the diagonal term does not invert A: inspect the (0,1) product. + wrong_entry = sum(a[0][t]*a[t][1]/13 for t in range(n)) + require(wrong_entry != 0, 'Omitted 12I inverse term is detected') + c = ainv[0][1] + require(c == F(-1, 26) and c != c*c, 'Owner scalar must not be tensor powered') + return {'scope': 'Unconjugated B_f^-1 at k=1, a_1=1', + 'matrix_polynomial_entries': n*n, + 'inverse_formula': 'A^-1=(A+12I)/13', + 'inverse_nonzero_terms_per_owner': 53, + 'add_count_for_every_positive_tensor_width': adds, + 'witness_tensor_width': width, + 'incorrect_literal_lower_bound': alleged, + 'omitted_diagonal_product_entry_0_1': str(wrong_entry), + 'once_applied_owner_coefficient': str(c), + 'incorrect_tensor_squared_coefficient': str(c*c), + 'large_tensor_materialized': False} + + +def run(): + pins = authenticate() + tables = monomials() + spec = importlib.util.spec_from_file_location('independent_markers', HERE / 'markers.py') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return {'status': 'PASS_INDEPENDENT_FRESH_STAGE_AUDIT_WITH_INVERSE_SCOPE_FINDING', + 'authenticated_inputs': pins, + 'inverse_scope_counterexample': inverse_counterexample(), + 'normalizers_and_conjugation': geometry(tables), + 'marker_audit': module.run(SOURCE), + 'proof_review': 'REVIEW.md; written argument, not formal-kernel acceptance', + 'complete_producer_replayed': False, + 'selected_frontier_changed': False} + + +def main(): + require(sys.argv[1:] in ([], ['--write']), 'Use no arguments or --write') + result = run() + encoded = json.dumps(result, sort_keys=True, indent=2)+'\n' + target = HERE / 'RESULT.json' + if sys.argv[1:]: + require(not target.exists(), 'Refuse to overwrite receipt') + target.write_text(encoded) + else: + require(target.read_text() == encoded, 'Deterministic receipt differs') + print(result['status']) + print(json.dumps(result['inverse_scope_counterexample'], sort_keys=True)) + + +if __name__ == '__main__': + main()