From 14cf51a62d64b0e97785c701ee84babfce01e2c5 Mon Sep 17 00:00:00 2001 From: woklerx <338878655+woklerx@users.noreply.github.com> Date: Wed, 14 Oct 2026 06:14:22 -0700 Subject: [PATCH] Independent audit: exhaustive full-query support hypotheses --- .../EXTERNAL-SOURCES.json | 18 +++ .../OVERLAP.json | 23 +++ .../source-query-finite-field-audit/README.md | 42 +++++ .../RESULT.json | 1 + .../SOURCE-REFRESH.json | 54 +++++++ .../SOURCES.json | 18 +++ .../source-query-finite-field-audit/TASK.json | 68 ++++++++ .../VERIFY.json | 20 +++ .../references/pr1877-PROOF.md | 152 ++++++++++++++++++ .../references/pr1877-README.md | 103 ++++++++++++ .../source-query-finite-field-audit/verify.py | 97 +++++++++++ 11 files changed, 596 insertions(+) create mode 100644 research/source-query-finite-field-audit/EXTERNAL-SOURCES.json create mode 100644 research/source-query-finite-field-audit/OVERLAP.json create mode 100644 research/source-query-finite-field-audit/README.md create mode 100644 research/source-query-finite-field-audit/RESULT.json create mode 100644 research/source-query-finite-field-audit/SOURCE-REFRESH.json create mode 100644 research/source-query-finite-field-audit/SOURCES.json create mode 100644 research/source-query-finite-field-audit/TASK.json create mode 100644 research/source-query-finite-field-audit/VERIFY.json create mode 100644 research/source-query-finite-field-audit/references/pr1877-PROOF.md create mode 100644 research/source-query-finite-field-audit/references/pr1877-README.md create mode 100644 research/source-query-finite-field-audit/verify.py diff --git a/research/source-query-finite-field-audit/EXTERNAL-SOURCES.json b/research/source-query-finite-field-audit/EXTERNAL-SOURCES.json new file mode 100644 index 0000000000..9f8ab8a847 --- /dev/null +++ b/research/source-query-finite-field-audit/EXTERNAL-SOURCES.json @@ -0,0 +1,18 @@ +[ + { + "pr": 1877, + "commit": "4d9fa6016682c910be06e55b1c974d53052aee76", + "path": "research/sourcecode-commutant/README.md", + "local": "references/pr1877-README.md", + "git_blob": "ceb230b0493d9f6ab143b4b3665f086effe6aef1", + "sha256": "3fb74b799b467c7ef80505e5a25ab969b12d9e6b71bdcfab0791fe2b8359a686" + }, + { + "pr": 1877, + "commit": "4d9fa6016682c910be06e55b1c974d53052aee76", + "path": "research/sourcecode-commutant/PROOF.md", + "local": "references/pr1877-PROOF.md", + "git_blob": "cd1362b7da35337224c9dcd1e5d2cf23a55b7117", + "sha256": "476eeab29a1af705ecffd7ba0d36c3ed305db7fdb57df0b861edf05111df6db7" + } +] diff --git a/research/source-query-finite-field-audit/OVERLAP.json b/research/source-query-finite-field-audit/OVERLAP.json new file mode 100644 index 0000000000..038f3355a3 --- /dev/null +++ b/research/source-query-finite-field-audit/OVERLAP.json @@ -0,0 +1,23 @@ +{ + "fetched_at": "2026-10-14T12:56:55.916545+00:00", + "open_prs": 535, + "discussion_records": 517, + "complete_pagination": true, + "scope": "PR bodies and Discussion records; not all code diffs or literature.", + "predecessor": { + "kind": "pr", + "number": 1877, + "title": "Source-query encoder support tradeoff and fixed-frame obstruction", + "body": "An invertible source encoder that logs the complete eight-coordinate query cannot make both endpoints sparse: its changed source fields and required target corrections together cover all **112 ports**. Each support also has at least eight ports. This is a scoped structural result for PR1862's clean-J interface, **not a new supplier or kappa**.\n\nFor Delta=G-I and H=(I-KR)Delta, the logger condition LG=R gives RDelta=(R-L)G. Its full row rank, together with nonzero K rows, proves the support cover. The statement also allows arbitrary finite address-linear encoders. Three explicit counterexamples show why the hypotheses are needed, and a valid three-port toy attains the cover.\n\nFor PR1862's fixed response Z, LZ=I makes the complete logger unique. It cannot commute with the unchanged line or specified output frames; two exact nonzero minors witness that obstruction for every positive tensor power. Changed/conjugated codes, paid transitions and carrying work through later native operations remain open. Endpoint support is not a universal native-child cost; the 112/120 rowwise figures in the report are conditional comparators only.\n\nValidation at `4d9fa6016682c910be06e55b1c974d53052aee76`:\n\n- [Dedicated Linux CI](https://github.com/chafreaky/integer-mult-bounds/actions/runs/38566908597) passes on Python 3.11 and 3.14.\n- Local Python 3.11.15, 3.14.8 and a read-only source export run without Git/private dependencies; all six committed/local/Linux receipts are byte-identical.\n- Source-derived scalar-prefix replay, 512-character census, two rational minors, four mutation controls and three missing-premise examples pass. No pending PR implementation is imported.\n\nOnly the new package and its dedicated workflow change. No full native supplier, global routing, hosting/precision or multiplication-theorem audit is claimed; other repository workflows are separate.\n\nCredit aliromman's [PR1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862) for the valid local encoder and stated interface, plus the pinned PR1042/PR1094 archive and retained E8/gauge44/native lineage. New proof and checker prepared for Chafik Boukhalfa with substantial OpenAI Codex assistance; no independent human review or formal proof assistant.\n", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1877", + "head": "4d9fa6016682c910be06e55b1c974d53052aee76", + "updated_at": "2026-10-14T12:53:23Z", + "draft": false, + "state": "open" + }, + "prior_batches_checked": [ + "integer-mult-20-contributions", + "integer-mult-20-rounds-20261014" + ], + "added_value": "Independent endpoint-support theorem audit over exhaustive small finite-field full-query encoders with rank and invertibility premise removal controls; rational sharp toy and source hypotheses separately pinned." +} diff --git a/research/source-query-finite-field-audit/README.md b/research/source-query-finite-field-audit/README.md new file mode 100644 index 0000000000..9174378f43 --- /dev/null +++ b/research/source-query-finite-field-audit/README.md @@ -0,0 +1,42 @@ +# Exhaustive independent audit of full-query endpoint support + +This audit independently stress-tests the algebraic support theorem in Chafik Boukhalfa / @chafreaky's PR1877. It adds a complete small finite-field census, independently found missing-premise witnesses and a rational sharp example. It does not re-audit the 112-port physical Fourier-frame obstruction or claim that finite fields certify complex rank. + +## Statement being audited + +Let L,R be r-by-n matrices, K be n-by-r, and let G be invertible with LG=R. Put Delta=G-I, J=I-KR, H=J Delta. If rank(R-L)=r and every K row is nonzero, the supports of rows of Delta and H cover all n ports. Indeed + + R Delta=(R-L)G + +has full row rank. If Delta_i=H_i=0, then K_i R Delta=0, contradicting the nonzero row K_i. Further L Delta=R-L gives rank(Delta)>=r. The separate assertion rank(H)>=r needs J invertible; it does not follow from the support cover alone. Right-multiplication by G^-1 shows that G^-1-I has exactly the same nonzero row support as Delta. These arguments work over any field. They are the credited predecessor proof, independently checked here, not inferred from the census. + +## Complete finite domain and new evidence + +Over GF(2), enumerate all 168 invertible 3x3 G, every r-by3 L for r=1 and2, and every 3-by-r K with no zero row. Set R=LG, then retain rank(R-L)=r. This exhausts 1008 rank-one and 117936 rank-two full-query cases. All satisfy the cover. For invertible J, the 432 rank-one and 40560 rank-two cases also satisfy both individual rank floors. The exact attainable (source support,target support) pairs are recorded by the verifier; these are finite GF(2) spectra, not the 112-port complex spectrum. + +The checker independently searches the complete 3-port rank-one matrix domain for witnesses violating the cover after removing exactly one of G invertibility, full rank of R-L, or nonzero K rows, while retaining invertible J. It requires nonzero query/read matrices and at least one nonzero K row, avoiding empty-query controls. A separate actual witness has full hypotheses for the cover but singular J and H=0, demonstrating why the target rank conclusion needs that additional premise. The predecessor's PROOF.md already states this premise; no error in it is alleged. + +A separately multiplied rational sharp example is + + L=[1,0,0], R=[1,1,0], K=[1,1,1]^T, + G=[[1,1,0],[0,1,0],[0,0,1]]. + +Delta has only row0=e1 and H has rows1,2=-e1, so the support sizes 1 and2 attain total 3. RK=2 ensures J invertible over Q. This is not a lift of a finite-field rank claim. It independently tests the original characteristic-zero algebra. + +## Reproduce and limitations + + python3.12 scripts/research_package.py --package research/source-query-finite-field-audit + +Read-only standard-library Python; explicit checks remain active under -O. The unchanged PR1877 README and PROOF are pinned by SHA256 and Git blob; no predecessor executable is imported. The exact head and complete overlap snapshot are recorded. This contribution is intentionally an independent proof-hypothesis audit. The actual112-port source instance, fixed-frame minors, native access costs, carrying the encoder through later work, hosting, precision, cold replay and all-size theorem remain outside this audit. No new supplier or kappa. + +## Source-head refresh + +Before publication, PR1877 advanced from the audited head `4d9fa6016682c910be06e55b1c974d53052aee76` to `6d455d2d71eb35ecf8e562711e5f719b994fe3f3`. The first 2386 bytes of PROOF.md, through “The verifier checks all four examples.”, are identical and include the audited algebraic theorem and hypotheses. SOURCE-REFRESH.json records both full-file Git blob and SHA256 hashes plus the identical section hash. The newer actual 112-port 8+104 sharp construction, generalized fixed-read frame obstruction and additional mutation controls belong to the credited predecessor and were inspected for scope, not independently verified here. The original immutable source pins remain the inputs to this audit. + +## Open next questions + +Can a paid chart transition or changed response space realize a complete useful source encoder? First pin an actual pair of native charts and price transport/restoration. The support theorem alone supplies neither a universal native-cost lower bound nor a construction. + +## Credit + +Chafik Boukhalfa / @chafreaky, PR1877, supplies the support theorem and source/frame proof; @aliromman /PR1862 the valid source encoder. PR1042/1094, E8/gauge44/native lineage retains its attribution in the pinned predecessor. New exhaustive audit and exact controls prepared for woklerx with substantial OpenAI Codex assistance, Apache-2.0. No independent human or formal proof-assistant review. diff --git a/research/source-query-finite-field-audit/RESULT.json b/research/source-query-finite-field-audit/RESULT.json new file mode 100644 index 0000000000..12485fdf1b --- /dev/null +++ b/research/source-query-finite-field-audit/RESULT.json @@ -0,0 +1 @@ +{"GL3": 168, "exhaustive_rows": [{"endpoint_support_pairs": [[1, 2], [2, 1], [2, 2], [2, 3], [3, 2], [3, 3]], "full_query_cases": 1008, "invertible_J_cases": 432, "query_rank": 1}, {"endpoint_support_pairs": [[2, 2], [2, 3], [3, 2], [3, 3]], "full_query_cases": 117936, "invertible_J_cases": 40560, "query_rank": 2}], "missing_J_control": {"G": [2, 1, 7], "H": [0, 0, 0], "K": [1, 1, 1], "L": [1], "R": [2], "r": 1}, "no_new_kappa": true, "premise_controls": {"full_rank_difference": {"Delta": [0, 0, 0], "G": [1, 2, 4], "H": [0, 0, 0], "K": [1, 1, 1], "L": [3], "R": [3]}, "invertible_G": {"Delta": [1, 0, 0], "G": [0, 2, 4], "H": [1, 0, 0], "K": [1, 1, 1], "L": [7], "R": [6]}, "nonzero_K_rows": {"Delta": [0, 0, 1], "G": [1, 2, 5], "H": [0, 1, 1], "K": [0, 1, 0], "L": [4], "R": [5]}}, "rational_sharp_support": [1, 2], "scope": "GF2 exhaustive stress test plus separately proved field-independent cover; no finite-field inference about physical frames", "status": "PASS_SOURCE_QUERY_FINITE_FIELD_AUDIT"} diff --git a/research/source-query-finite-field-audit/SOURCE-REFRESH.json b/research/source-query-finite-field-audit/SOURCE-REFRESH.json new file mode 100644 index 0000000000..15565238ec --- /dev/null +++ b/research/source-query-finite-field-audit/SOURCE-REFRESH.json @@ -0,0 +1,54 @@ +{ + "source_pr": 1877, + "audited_head": "4d9fa6016682c910be06e55b1c974d53052aee76", + "observed_head": "6d455d2d71eb35ecf8e562711e5f719b994fe3f3", + "inspected_at_utc": "2026-10-14T13:26:11.255Z", + "evidence": "Git objects fetched from origin pull/1877/head; exact source files read with git show.", + "files": [ + { + "path": "research/sourcecode-commutant/README.md", + "audited": { + "git_blob": "ceb230b0493d9f6ab143b4b3665f086effe6aef1", + "sha256": "3fb74b799b467c7ef80505e5a25ab969b12d9e6b71bdcfab0791fe2b8359a686", + "bytes": 5602 + }, + "observed": { + "git_blob": "9d236651529a326861d258c741c485f1b8c06232", + "sha256": "afc65ab6a27b93c3a7ad6ade6c8694f7d0f6777fd1cda085cdbc381916671850", + "bytes": 6160 + } + }, + { + "path": "research/sourcecode-commutant/PROOF.md", + "audited": { + "git_blob": "cd1362b7da35337224c9dcd1e5d2cf23a55b7117", + "sha256": "476eeab29a1af705ecffd7ba0d36c3ed305db7fdb57df0b861edf05111df6db7", + "bytes": 7832, + "audited_prefix_sha256": "214d133bf3e6624a45a3c920aab38eb7437b811249e70c4e44aa46d829e251e0", + "audited_prefix_bytes": 2386 + }, + "observed": { + "git_blob": "7c1a95e6fd50634c59051908b1f0d6eadcc48513", + "sha256": "e91bc6879224cc06ea463d2a92a57b8d83c3b20d0c7cdf9980a3fd542bf20a5c", + "bytes": 9707, + "audited_prefix_sha256": "214d133bf3e6624a45a3c920aab38eb7437b811249e70c4e44aa46d829e251e0", + "audited_prefix_bytes": 2386 + } + } + ], + "audited_section": { + "path": "research/sourcecode-commutant/PROOF.md", + "start": "Beginning of file", + "end_inclusive": "The verifier checks all four examples.", + "bytes": 2386, + "sha256": "214d133bf3e6624a45a3c920aab38eb7437b811249e70c4e44aa46d829e251e0", + "unchanged": true + }, + "conclusion": "The algebraic endpoint-support theorem and its hypotheses audited here are unchanged. Retain original exact source pins for reproducibility.", + "new_source_extensions_outside_this_audit": [ + "Actual 112-port sharp 8-source plus 104-target encoder construction", + "Fixed eight-port read obstruction generalized beyond the particular logger Z", + "Additional source-frame mutation controls" + ], + "limitations": "This refresh establishes unchanged theorem text, not independent verification of the new source-frame extensions." +} diff --git a/research/source-query-finite-field-audit/SOURCES.json b/research/source-query-finite-field-audit/SOURCES.json new file mode 100644 index 0000000000..9ad00bf21b --- /dev/null +++ b/research/source-query-finite-field-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + } + ] +} diff --git a/research/source-query-finite-field-audit/TASK.json b/research/source-query-finite-field-audit/TASK.json new file mode 100644 index 0000000000..1e22dc50e4 --- /dev/null +++ b/research/source-query-finite-field-audit/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent endpoint-support theorem audit over exhaustive small finite-field full-query encoders with rank and invertibility premise removal controls; rational sharp toy and source hypotheses separately pinned.", + "scope_change_reason": "Fresh overlap found a directly relevant pending result. Deliberate independently implemented audit adds distinct finite evidence and controls; it does not assert a new physical supplier or repeat the predecessor as an original theorem.", + "bottleneck_link": "Strengthens independently reviewable evidence for a named mathematical boundary; no new kappa or complete supplier claimed.", + "budget_minutes": 60, + "stop_rule": "Stop after the declared exact audit domain, premise controls, optimized replay and source validation.", + "outcome": "completed", + "evidence": "README.md and deterministic verify.py output", + "author": "woklerx with substantial OpenAI Codex assistance", + "ai_assistance": "OpenAI Codex derived and implemented this independent audit; no independent human review.", + "open_questions": [ + { + "question": "Can a paid chart transition or changed response space give a useful complete source encoder?", + "why_it_matters": "The endpoint-support theorem is not a universal native-cost bound.", + "first_step": "Pin two native charts and price transport and restoration before assembly.", + "blocked_by": "No source-bound complete physical transition or precision/hosting invoice is supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18924424", + "selection_nonce": "8251907335fc151d2de2de0b56909bd2" +} diff --git a/research/source-query-finite-field-audit/VERIFY.json b/research/source-query-finite-field-audit/VERIFY.json new file mode 100644 index 0000000000..0696430765 --- /dev/null +++ b/research/source-query-finite-field-audit/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Exact independent mathematical audit, positive fixtures, premise-removal controls, immutable source pins." + } + ] +} diff --git a/research/source-query-finite-field-audit/references/pr1877-PROOF.md b/research/source-query-finite-field-audit/references/pr1877-PROOF.md new file mode 100644 index 0000000000..cd1362b7da --- /dev/null +++ b/research/source-query-finite-field-audit/references/pr1877-PROOF.md @@ -0,0 +1,152 @@ +# Endpoint support and fixed-frame obstructions for complete source queries + +## Every invertible full-query encoder has complete endpoint support + +Let R,L be r-by-n matrices, K be n-by-r, and J=I-KR. Assume R-L has full +row rank and every row K_i is nonzero. For any invertible G satisfying +LG=R, put Delta=G-I and H=J Delta. H is precisely the target correction +needed by the input prelude X+=HY, Y=GY before the retained clean-J word. + +The full-query identity gives + + R Delta=RG-R=(R-L)G. + +Its row rank is r. If Delta_i=0 and H_i=0 at a port i, then +K_i R Delta=0. A full-row-rank matrix has no nonzero left annihilator, +so K_i=0, a contradiction. The changed-source and corrected-target row +supports therefore cover all n ports. Also L Delta=R-L gives +rank(Delta)>=r, so at least r source rows change. If J is invertible, +rank(H)=rank(Delta)>=r, so at least r target rows are corrected. + +For an arbitrary finite address payload, tensor R,L,K with its identity +and allow G to be any invertible complex linear map on all port payloads. +The same proof uses full row rank r times the payload dimension. A nonzero +K_i tensor identity cannot annihilate that surjective map. The covering +statement therefore counts whole port blocks and is not restricted to +scalar source codes. + +In the pinned instance n=112 and r=8. The R-L minor on A has nonzero +determinant, all 112 K_i are nonzero, and RK=14I. The latter implies +J^-1=I-KR/13 over C; no circuit division by 13 is proposed. Thus both +supports contain at least eight ports and their union contains all 112. +Since G^-1-I=-Delta G^-1, the source support is also exactly the support +of the inverse's changed rows. + +If a particular rowwise implementation charges at least one rank-one child +for every active target and source endpoint, it pays at least 112. If its +source normalization and return each cost one such child, it pays at least +112+8=120. These are conditional cost comparators. The support theorem +alone is not a universal native-cost lower bound and does not rule out a +compiler carrying updates through compulsory later work. + +Three literal n=3,r=1 examples show that dropping invertibility, full rank +of R-L, or nonzero K rows can invalidate the cover. Each retains the other +premises, including invertibility of J. A fourth valid example attains +|source support|+|target support|=n. The verifier checks all four examples. + +## The fixed-frame commuting shortcut also fails + +The local source encoder in PR1862 is valid and its unchanged replay passes. +The following argument rules out one shortcut for carrying that code: keeping the same +operator across the individual source output frames. It does not rule out +changed charts, different encoders, paid transports or a complete supplier. +In particular, it is not a lower bound for every zero-native-cost circuit. + +Let V=C^512 be the local nine-bit address space. At port i, write + + C_qi=((1+i)I+(1-i)X_qi)/2, + S_i=F C_qi^-1, F=product_{a=0}^8 C_(2^a). + +The retained source output frame is S=diag(S_i). These are the frames in +PR1862's proof; they must not be replaced by a common full frame. Put +D=diag(C_qi). Its eight-by-112 R, 112-by-eight Z, and eight-port selector L +are those of the pinned PR1862 replay. Every row of Z is a nonzero scalar +multiple of the corresponding row of K=R^T/4: the multiplier is -12 on the +eight compensation ports and one elsewhere. + +Allow B to be an arbitrary eight-by-112 matrix of complex linear operators +on V. Thus this includes address-valued coefficients, not just dyadic scalar +matrices. Consider G=I+ZB. The proposed complete logger condition is + + L G=R tensor I_V. + +There is no such G commuting with D. There is also no such G commuting +with S. Invertibility of G is not needed for this obstruction. + +For this particular Z and L, LZ=I. The logger condition already forces +B=R-L, even when B initially allows address-linear operators. Thus there +is only one full-query logger in this fixed response family. The Fourier +argument below verifies its incompatibility with the fixed frames directly. + +## One Fourier output character suffices + +In the binary Fourier basis indexed by x in F2^9, C_qi has eigenvalue +i^(qi dot x). Fix output character x=1. For either bit b=0 or b=1, the +rows of Z with qi dot x different from b have rank eight. The checker +gives explicit nonzero minors: + +| Excluded eigenbit b | Eight port rows | Determinant of Z minor | +| --- | --- | --- | +| 0 | 0,1,2,3,4,5,6,12 | -3/512 | +| 1 | 25,26,27,28,29,30,31,44 | -3/1024 | + +For fixed input port j and input character y, let b_j(x,y) in C^8 be the +corresponding coefficients of B. Commutation with D requires + + (i^(qi dot x)-i^(qj dot y)) Z_i b_j(x,y)=0 + +for every row i. The eigenbit qj dot y is either zero or one. Its excluded +rows have rank eight, forcing b_j(x,y)=0. This holds for every j and y. +Consequently G-I has no output at character x. + +For S, its eigenvalue at output character x is i^(|x|-qi dot x), hence +either i or 1. The input eigenvalue of S_j is one of 1,i,-1,-i. If it is +1 or i, one of the same two full-rank row sets forces b_j(x,y)=0. For +either other phase, all rows are excluded; they have rank eight as well. +Again G-I has no output at character x. + +Therefore L G equals L, rather than R, on that output character. This +contradicts the required logger identity: query row zero has coefficient +one at source port zero, while L is supported on the eight selected query +ports and has coefficient zero there. The checker records this coefficient +witness directly from the pinned replay. + +## Tensor powers and scope + +For any positive tensor power t, use output character (1,0,...,0). The +output eigenvalues of each tensor-powered C_qi or S_i still have just the +two phases used above. An arbitrary input character gives one of four +phases. The same two minors, or the entire rank-eight row set, again force +every coefficient b_j at that output character to vanish. The obstruction +therefore persists for arbitrary address-linear B on V^tensor t. + +This concerns commutation with the unchanged output operator. A compiler +could instead change the code under a monomial conjugacy, carry it through +later compulsory native work, use a different response space, or pay for +transport. None of those possibilities is priced or excluded here. The +actual PR1862 local construction and its arbitrary-helper restoration are +not contradicted. + +## Reproduce and credit + +`python3 -I -O -B research/sourcecode-commutant/verify.py` reads the frozen +PR1042 archive directly and checks its compressed and decoded member hashes. +It reconstructs R by a separate exact scalar-prefix replay, checks the disjoint +coordinate minors and RZ=LZ=I, and matches canonical to physical line labels. +No PR1862 implementation, local Git database or network is required at runtime. +The rank and determinant computations use separate integer and rational +elimination methods. All 512 characters are inspected as supplementary evidence: +494 have rank eight in both groups, eight have ranks (7,8), eight have (8,7), and +the two constant characters have (0,8) and (8,0). The single explicit witness +already proves the statement. Four actual mutations reject a constant character, +a zeroed matrix row, a false determinant and a changed source archive. + +PR1862 head 7649d9ceecec949541bec4bbde5929344166ba59 supplies the encoder, +fixed-support response space and pinned historical complex supplier. +Its sources and notices retain the PR1042/PR1094, gauge44, E8, frame and +native-checker lineage. This note adds the fixed-frame commutant obstruction; +it claims no independent human review, complete native supplier or kappa. + +The next useful question is a paid or conjugated chart transition with an +explicit invoice. Requiring the original encoder to commute with the line +frames cannot supply that transition. diff --git a/research/source-query-finite-field-audit/references/pr1877-README.md b/research/source-query-finite-field-audit/references/pr1877-README.md new file mode 100644 index 0000000000..ceb230b049 --- /dev/null +++ b/research/source-query-finite-field-audit/references/pr1877-README.md @@ -0,0 +1,103 @@ +# Full-query source codes require complete endpoint support + +PR1862 gives a valid local source encoder that stores the eight-coordinate +centre query in existing source fields. For any invertible full-query encoder +at this interface, the source fields it changes and the target fields it must +correct together cover all 112 ports. Both endpoints cannot be sparse. + +The support theorem allows arbitrary finite address-linear encoders. A second, +narrower result rules out a fixed-response logger commuting with the unchanged +line or specified output-frame operator, for every positive tensor power. +Neither result excludes changed operators, monomial conjugacies, carrying the +code through later native work, or paid chart transitions. Endpoint support is +not a universal native-child charge. No new supplier or kappa is claimed. + +## Result and evidence + +Write J=I-KR, Delta=G-I and H=J Delta. The full-query condition LG=R gives +R Delta=(R-L)G. Since R-L has rank eight and G is invertible, this matrix +has full row rank. If both Delta_i and H_i vanish at a port, then +K_i R Delta=0, contradicting the nonzero K_i. Thus the endpoint supports +cover all 112 ports. Each support also contains at least eight ports. + +This supplies a scoped cost control: a model charging one rank-one child per +active endpoint already pays at least 112. Charging a changed source for both +outward and return transfers gives at least 120. Those prices are conditional +rowwise comparators, not a lower bound for all implementations; the old eight +rank-eight centre queries cost 64 in rank mass. A useful implementation must +beat that per-endpoint charging model. + +For G=I+ZB and the eight-port query read L in PR1862, there is no solution to +LG=R that commutes with diag(C_q), or with diag(F C_q^-1). Here B may contain +arbitrary complex linear maps, although LZ=I already makes the full-query +logger unique: B=R-L. This is a fixed-frame obstruction, not a lower bound +for every zero-native-cost circuit. + +One Fourier output character is enough. At x=1, both excluded-eigenvalue +row sets of Z contain an invertible eight-by-eight minor. Their exact +determinants are -3/512 and -3/1024. Commutation forces the whole output +row of B at that character to vanish, contradicting a nonzero R-L coefficient. +[PROOF.md](PROOF.md) supplies the argument and tensor-power extension. + +[EXPECTED.json](EXPECTED.json) is the exact finite certificate. The verifier +derives R directly from the pinned historical scalar program, checks the +source response identities and physical labels, and checks all 512 characters. +There are 494 full-rank cases in both eigenvalue groups. Four actual mutations +fail: a constant character, a zeroed matrix row, a false determinant and a +changed source archive. Three explicit three-port counterexamples show why +invertibility, rank(R-L) and nonzero K rows are needed. A valid toy attains +the support-cover inequality. Checks remain active under Python optimization. + +The finite certificate and written argument are separate from a complete +native replay, global routing, precision, hosting or multiplication theorem. +The specified output-frame model is the contract stated in PR1862; this +package does not re-audit all of that predecessor's native events or phases. + +## Reproduce + +Python 3.11 or newer, standard library only, from the repository root: + +```sh +python3 -I -O -B research/sourcecode-commutant/verify.py +``` + +Expected output: + +```text +PASS_SOURCECODE_SUPPORT_AND_FRAME endpoint_support>=112 characters=512 full_rank=494 mutations=4 premise_controls=3 no_new_kappa +``` + +The runtime reads only its committed certificate and the frozen input archive +declared in [SOURCES.json](SOURCES.json). It needs no network, Git history, +pending PR implementation or generated predecessor receipt. The dedicated +workflow runs the same check under Python 3.11 and 3.14 and retains receipts. +A local replay is separate from hosted CI completion. + +## Open next questions + +1. **A changed or paid chart transition.** This matters because the local + encoder is useful only if its source data can be restored or its code can + be carried onward. First derive the actual conjugated source map between + two routed charts and price its native transfers. The missing component + is a complete physical access, restoration and precision invoice. +2. **A different response space.** This matters because the obstruction fixes + Z and the eight-port read L. First identify a changed target-support or + query contract and check its excluded-row ranks before searching for a + circuit. No useful alternative response space is constructed here. + +## Credit and review scope + +@aliromman's [PR1862](https://github.com/CrocSwap/integer-mult-bounds/pull/1862), +pinned at 7649d9ceecec949541bec4bbde5929344166ba59, +supplies the encoder, fixed-support response space and exact local construction. +Its valid local result is not contradicted. The E8 unit, PR1042 archive, +PR1094 assembly and retained gauge44/native lineage remain credited to their +authors. The source notices credit icekylinx, Hao Yan / FanPUYen, Jeremy Kothe, +Chafik Boukhalfa, rohanarun and NewBArch for the retained frame and supplier work. +No predecessor code is copied into this package. + +The new contribution is the endpoint-support tradeoff for arbitrary invertible +full-query encoders, the fixed-frame obstruction and its two-minor witness, +and a separate source-derived exact verifier. Prepared +for Chafik Boukhalfa with substantial OpenAI Codex assistance. No independent +human review or formal proof assistant is claimed. New material is Apache-2.0. diff --git a/research/source-query-finite-field-audit/verify.py b/research/source-query-finite-field-audit/verify.py new file mode 100644 index 0000000000..cbb527039d --- /dev/null +++ b/research/source-query-finite-field-audit/verify.py @@ -0,0 +1,97 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact audit by woklerx with substantial OpenAI Codex assistance.""" +from pathlib import Path +from fractions import Fraction as F +from itertools import product, permutations +from math import isqrt +import json, hashlib +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +def require(ok, message): + if not ok: raise ValueError(message) +def source_check(): + for row in json.loads((HERE/'EXTERNAL-SOURCES.json').read_text()): + b=(HERE/row['local']).read_bytes() + require(hashlib.sha256(b).hexdigest()==row['sha256'],'external source bytes') + require(hashlib.sha1(b'blob '+str(len(b)).encode()+b'\0'+b).hexdigest()==row['git_blob'],'external Git blob') + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage']=='input': + require(hashlib.sha256((ROOT/row['path']).read_bytes()).hexdigest()==row['sha256'],'live source bytes') +source_check() + +def mm(A,B): + out=[] + for a in A: + row=0 + for j,b in enumerate(B): + if (a>>j)&1:row^=b + out.append(row) + return tuple(out) +def rank(A): + piv={} + for a in A: + while a: + k=a.bit_length()-1 + if k in piv:a^=piv[k] + else:piv[k]=a;break + return len(piv) +def inv(A): + n=len(A);rows=[a|((1<>i)&1),None) + if p is None:return None + rows[i],rows[p]=rows[p],rows[i] + for j in range(n): + if j!=i and (rows[j]>>i)&1:rows[j]^=rows[i] + return tuple(a>>n for a in rows) +I=(1,2,4);allG=list(product(range(8),repeat=3));GL=[g for g in allG if inv(g) is not None] +require(len(GL)==168,'GL3 cardinality') +rows=[];zeroJexample=None +for r in (1,2): + admitted=jinvertible=0;pairs=set() + for G in GL: + Delta=tuple(a^b for a,b in zip(G,I));ds={i for i,a in enumerate(Delta) if a} + Gi=inv(G);require(ds=={i for i,a in enumerate(Gi) if a!=I[i]},'inverse changed-row support') + for L in product(range(8),repeat=r): + R=mm(L,G);difference=tuple(a^b for a,b in zip(R,L)) + if rank(difference)!=r:continue + require(rank(Delta)>=r,'source rank floor') + for K in product(range(1,1<=r and len(hs)>=r,'target rank floor requires invertible J') + jinvertible+=1;pairs.add((len(ds),len(hs))) + elif rank(H)