From 2b954ed2442a14c12b1e21a7ab795edd3b76876b Mon Sep 17 00:00:00 2001 From: Sricharan Vagvala Date: Mon, 12 Oct 2026 22:23:35 -0700 Subject: [PATCH 1/2] Audit selected binary cover order and finite invoice guards --- .../CERTIFICATE.json | 221 +++++++++++++++ .../orthogonal-cover-invoice-audit/CLAIM.md | 61 ++++ .../orthogonal-cover-invoice-audit/README.md | 203 +++++++++++++ .../SOURCES.json | 30 ++ .../VALIDATION.json | 67 +++++ .../test_verify.py | 136 +++++++++ .../orthogonal-cover-invoice-audit/verify.py | 266 ++++++++++++++++++ 7 files changed, 984 insertions(+) create mode 100644 research/orthogonal-cover-invoice-audit/CERTIFICATE.json create mode 100644 research/orthogonal-cover-invoice-audit/CLAIM.md create mode 100644 research/orthogonal-cover-invoice-audit/README.md create mode 100644 research/orthogonal-cover-invoice-audit/SOURCES.json create mode 100644 research/orthogonal-cover-invoice-audit/VALIDATION.json create mode 100644 research/orthogonal-cover-invoice-audit/test_verify.py create mode 100644 research/orthogonal-cover-invoice-audit/verify.py diff --git a/research/orthogonal-cover-invoice-audit/CERTIFICATE.json b/research/orthogonal-cover-invoice-audit/CERTIFICATE.json new file mode 100644 index 0000000000..6e673b8b51 --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/CERTIFICATE.json @@ -0,0 +1,221 @@ +{ + "status": "PASS_ORTHOGONAL_COVER_INVOICE_AUDIT", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 65, + "scope": "Binary dot-product cover order and finite invoice only; no new kappa or full theorem proof.", + "selected_kappa_unchanged": "51110230636731/31250000000000000", + "enumeration": [ + { + "dimension": 1, + "complete_bases": 1, + "prefix_counts": [ + 1, + 1 + ], + "first_column_completion_histogram": { + "1": 1 + }, + "characteristic_vector_completions": 1 + }, + { + "dimension": 2, + "complete_bases": 2, + "prefix_counts": [ + 1, + 2, + 2 + ], + "first_column_completion_histogram": { + "1": 2 + }, + "characteristic_vector_completions": null + }, + { + "dimension": 3, + "complete_bases": 6, + "prefix_counts": [ + 1, + 4, + 6, + 6 + ], + "first_column_completion_histogram": { + "0": 1, + "2": 3 + }, + "characteristic_vector_completions": 0 + }, + { + "dimension": 4, + "complete_bases": 48, + "prefix_counts": [ + 1, + 8, + 32, + 48, + 48 + ], + "first_column_completion_histogram": { + "6": 8 + }, + "characteristic_vector_completions": null + }, + { + "dimension": 5, + "complete_bases": 720, + "prefix_counts": [ + 1, + 16, + 120, + 480, + 720, + 720 + ], + "first_column_completion_histogram": { + "0": 1, + "48": 15 + }, + "characteristic_vector_completions": 0 + }, + { + "dimension": 6, + "complete_bases": 23040, + "prefix_counts": [ + 1, + 32, + 512, + 3840, + 15360, + 23040, + 23040 + ], + "first_column_completion_histogram": { + "720": 32 + }, + "characteristic_vector_completions": null + }, + { + "dimension": 7, + "complete_bases": 1451520, + "prefix_counts": [ + 1, + 64, + 2016, + 32256, + 241920, + 967680, + 1451520, + 1451520 + ], + "first_column_completion_histogram": { + "0": 1, + "23040": 63 + }, + "characteristic_vector_completions": 0 + } + ], + "dimension_73": { + "exact_group_order": "88055447129748213099772773138986247571255042612072591674225283308028684371120843328012160052393152527232914014288489818688809961936816670640083409439382433171031243906547760371818869073538416126076656782695792682453482806912643430535775039142420588510522358113551513811666116187287324377802034479488864420323400940604907630584384722731975858354648334415461784223587007406274343722056702999013519051565035640715216081796349147473651840479245483695654253901532871494454113952288727044052531881069342514232455091429630737092047517685965106058714054953066900424219349387329299169409559363267460270558762270126564878116036572334698547529778107107730613024527066352193202984895478814351821651183238272958917221207575904540573250955207812277015748415513176772283677218766323712000000000000000000000", + "group_bits": 2628, + "finite": { + "physical_stock_bits": 2641, + "router_bits": 7985, + "literal_bits": 35282, + "physical_row_coefficient": 16467, + "retained_row_coefficient": 20161, + "required_C0_bits": 200012, + "halving_integer_inequality": [ + 5329, + 4608 + ], + "G_exponent": 30000, + "E_exponent": 100000, + "C0_exponent": 210000 + }, + "strict_checks": { + "local_primitive_bound": true, + "logical": true, + "router": true, + "literal": true, + "mass": true, + "precision": true, + "tape": true, + "row": true, + "halving": true + }, + "guard_bits": { + "local_primitive_bound": { + "actual_bits": 44, + "bound_exponent": 48 + }, + "logical": { + "actual_bits": 2680, + "bound_exponent": 6050 + }, + "router": { + "actual_bits": 7985, + "bound_exponent": 30000 + }, + "literal": { + "actual_bits": 35282, + "bound_exponent": 100000 + }, + "mass": { + "actual_bits": 100001, + "bound_exponent": 100001 + }, + "precision": { + "actual_bits": 200012, + "bound_exponent": 210000 + }, + "tape": { + "actual_bits": 100002, + "bound_exponent": 210000 + } + } + }, + "negative_controls": { + "omit_cover_multiplicity": { + "cover_binding_rejected": true, + "group_bits": 1, + "failed_guards": [], + "physical_row_coefficient": 11211 + }, + "use_even_dimension_72": { + "cover_binding_rejected": true, + "group_bits": 2556, + "failed_guards": [], + "physical_row_coefficient": 16323 + }, + "omit_last_symplectic_pair": { + "cover_binding_rejected": true, + "group_bits": 2485, + "failed_guards": [], + "physical_row_coefficient": 16181 + }, + "omit_powers_of_two": { + "cover_binding_rejected": true, + "group_bits": 1332, + "failed_guards": [], + "physical_row_coefficient": 13875 + }, + "use_all_invertible_matrices": { + "cover_binding_rejected": true, + "group_bits": 5328, + "failed_guards": [ + "row" + ], + "physical_row_coefficient": 21867 + } + }, + "cover_only_inflation": { + "last_passing_power_of_two": 1846, + "last_passing_row_coefficient": 20159, + "first_failing_power_of_two": 1847, + "first_failing_row_coefficient": 20161, + "first_failed_guards": [ + "row" + ], + "scope": "All other admitted invoice quantities fixed; not a construction or supplier improvement." + } +} diff --git a/research/orthogonal-cover-invoice-audit/CLAIM.md b/research/orthogonal-cover-invoice-audit/CLAIM.md new file mode 100644 index 0000000000..120c71a2df --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/CLAIM.md @@ -0,0 +1,61 @@ +# Sprint claim — seed 65 + +- Track: adversarial mathematical audit (60–74). +- OS-random assignment seed: **65**, from `secrets.randbelow(100)` at + 2026-10-13 05:09:06 UTC (2026-10-12 22:09 PDT). +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +- Branch: `codex/orthogonal-cover-invoice-seed65`. +- Budget: 60 minutes, with the final 15 minutes reserved for verification + and handoff; expected finish 2026-10-13 06:09 UTC (October 12, 23:09 PDT). + +## Three narrow candidates + +0. Cold-helper compensation admission in the selected #626 source; deferred + because #702 and #729 already cover related wrapper/frame obligations. +1. Arbitrary private-center restoration in a selected scalar orientation; + deferred because #734/#745 already cover it by distinct forward/reverse methods. +2. The order of the binary dot-product isometry group used in #626's finite + routing invoice, and the propagation of its multiplicity into finite guards. + +The seed selects candidate `65 % 3 = 2`. The other candidates are already +crowded. The chosen mathematical object is the *bilinear* dot-product group, +not a quadratic-form orthogonal group; in odd dimension its characteristic +vector splits off and the complement is symplectic. + +## Exact scope and method + +Audit the group factor in `code/invoice_allcold.py` and `code/assemble.py` +of `research/complex-k492-owner-repair`, bound to the reviewed #626 invoice. +Derive the odd-dimensional order by counting symplectic bases; independently +count complete binary orthonormal bases in dimensions 1 through 7 without +using that formula. Recompute the group-dependent finite guards with integer +arithmetic, and supply controls for a wrong group family or missing cover +multiplicity. No new kappa, search for a new supplier, or selected-frontier +edit is planned. Expected deliverable: a scoped proof, exact certificate, +standalone verifier, source pins and meaningful negative controls. + +## Coordination and overlap + +GitHub reports no pinned issues; the sole open issue is #650 (Discussions), +so this is the local claim. No separate reservation issue was opened. +The full open queue was inspected (578 PRs), then latest arrivals through +#762 were checked immediately before this claim. #717 studies moment/invoice +sensitivity and pair-preserving program permutations, not the ambient cover +cardinality and finite routing guards. Its scope was inspected. The selected +review and prior negative-results index were read; no closed supplier search +is reopened here. No pending PR supplies code or inputs to this audit. + +## Completed result and final overlap check + +The group factor and all nine finite invoice guards are corroborated. +Exhaustive basis enumeration covers dimensions 1–7. Five wrong-order controls +are rejected explicitly; four undercounts still pass every upper-bound guard, +whereas using GL(73,2) violates the row cap. Exact cover-only inflation reaches +its first failed guard at a factor of 2^1847. No construction defect or new +kappa is claimed. See README.md, CERTIFICATE.json and VALIDATION.json. + +The final full-queue check covered 586 open PRs through #767; no ambient +cover-cardinality audit was found. #717 remains distinct (moment/invoice +sensitivity and finite program permutations). Upstream main is still the +recorded base. No coordination issue exists, so the completion link is recorded +here after submission. diff --git a/research/orthogonal-cover-invoice-audit/README.md b/research/orthogonal-cover-invoice-audit/README.md new file mode 100644 index 0000000000..ed825b8efa --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/README.md @@ -0,0 +1,203 @@ +# Audit of the binary cover order in the selected #626 finite invoice + +**Adversarial mathematical audit; no new κ.** The selected invoice uses the +correct order of the group preserving the standard binary **bilinear** dot +product in dimension 73. A self-contained counting argument and an independent +exhaustive implementation agree. Recomputing the nine finite guards reproduces +the committed receipt exactly. + +This audit also establishes a concrete scope limit: replacing this group by +all of `GL(73,2)` exceeds the retained physical-row coefficient, **21,867 > +20,161**, although the other eight guards still pass. Conversely, four +incorrect smaller group factors pass all nine upper-bound guards; they must +be rejected by the group definition, not by those inequalities. The intact +production code computes the correct factor. These controls are **not** +counterexamples to the selected construction or evidence of acceptance by +its full verifier. + +## Reproduce + +From the repository root, with Python 3.11+ and no third-party dependencies: + +```sh +python3 -I -B research/orthogonal-cover-invoice-audit/verify.py +python3 -I -B research/orthogonal-cover-invoice-audit/test_verify.py +``` + +Expected verifier output: + +```text +PASS_ORTHOGONAL_COVER_INVOICE_AUDIT dimensions=1..7 guards=9 controls=5 kappa=unchanged +``` + +The second command runs eight tests. Verification checks source hashes and +receipt bindings, recomputes every certificate field, and compares the whole +result with [CERTIFICATE.json](CERTIFICATE.json). To regenerate only this +package's certificate, add `--write-certificate /tmp/cover-certificate.json`. +No repository file is changed during ordinary verification. Assertions are +not used, so the checks also execute under `-O`. + +## Object and provenance + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. OS-random assignment seed: **65**. +The [claim](CLAIM.md) records three candidates and overlap checks. +[SOURCES.json](SOURCES.json) pins the consumed bytes, the reviewed #626/#623/ +#622/#543 heads, and the selected-record/assembly/invoice/owner chain. The +selected source manifest independently binds both production files audited: + +- `research/complex-k492-owner-repair/code/invoice_allcold.py`, function `run`; +- `research/complex-k492-owner-repair/code/assemble.py`, finite-invoice checks. + +The consumed invoice is the maintainer's +`research/community-k492-audit/pr626/replay/mixed-global/audit/PREFIX-AND-INVOICE.json`. +Its admitted scalar costs, physical stock and owner profile are inputs here; +this audit does not regenerate or independently admit the supplier. + +## Counting argument + +Write `B(x,y) = Σ x_i y_i` over `F₂`, and let `Ω=(1,…,1)`. Then +`B(x,x)=B(x,Ω)`. Nondegeneracy makes Ω the unique vector with this property, +so every isometry fixes it. + +For odd `n=2r+1`, `B(Ω,Ω)=1`. Thus the whole space is the orthogonal direct +sum of `⟨Ω⟩` and `U=Ω⊥`. On U, the form is alternating and nondegenerate, +of dimension `2r`. Restriction gives an isomorphism from the dot-product +isometry group to `Sp(U)`: every isometry fixes Ω, and every symplectic map +of U extends by fixing Ω. + +In a nondegenerate alternating space of dimension `d=2r`, choose the first +nonzero basis vector in `2^d−1` ways. Its partner with pairing one has +`2^(d−1)` choices, because pairing against a nonzero vector is a nonzero +linear functional. Their plane is nondegenerate, leaving an alternating +orthogonal complement of dimension `d−2`. A symplectic map is uniquely +determined by its ordered symplectic basis images. Consequently + +```text +S(0) = 1 +S(d) = (2^d − 1) 2^(d−1) S(d−2) +|Iso(F₂^(2r+1), B)| = S(2r) = 2^(r²) ∏[j=1..r] (2^(2j)−1). +``` + +For the even-dimensional comparison, choose e with `B(e,Ω)=1`. +Now Ω is isotropic, the plane `⟨Ω,e⟩` is nondegenerate, and its complement +U is alternating of dimension `n−2`. Every isometry has uniquely the form + +```text +Ω ↦ Ω +e ↦ e + u + cΩ +v ↦ Sv + B(u,Sv)Ω (v ∈ U), +``` + +where `S ∈ Sp(U)`, `u ∈ U`, and `c ∈ F₂`. Directly checking all pairings +proves these maps are isometries; the decomposition and preservation of Ω +give the converse. Hence the even order is `2^(n−1) S(n−2)`. +This agrees with the existing even-dimensional discussion in +`notes/three-stage-cover-complex.tex`, rather than applying the odd formula +to an even space. + +These are standard group facts, not new group theory. See Daniel Dugger, +[Involutions in the topologists' orthogonal group, Propositions 2.3–2.4](https://pages.uoregon.edu/ddugger/invto121616.pdf), +for the distinction from quadratic-form orthogonal groups and these orders. +That reference is not needed at runtime. The proof above supplies the +all-dimensional order argument; the finite enumeration below is a separate +check, not a formal proof of the general formula. + +## Independent finite evidence + +The enumerator appends every odd-weight vector orthogonal to the existing +prefix. Its identity Gram matrix makes the prefix linearly independent, +and its complete length-n leaves are exactly the ordered orthonormal bases. +No order formula, orbit representative, memoization or symmetry quotient is +used to obtain the counts. Every prefix count and first-column completion +histogram is recorded in the certificate. + +| Dimension | Complete ordered orthonormal bases | +|---:|---:| +| 1 | 1 | +| 2 | 2 | +| 3 | 6 | +| 4 | 48 | +| 5 | 720 | +| 6 | 23,040 | +| 7 | 1,451,520 | + +For odd n > 1 the apparently legal unit vector Ω has no complete extension: +its complement contains only even-weight vectors. This catches the tempting +but incorrect step of treating every unit first column as extendable. The +test suite independently enumerates **all** binary matrices through dimension +4 using scalar Gram entries, checks that every isometry fixes Ω, and exhibits +64 matrices with unit columns but only 6 isometries in dimension 3. + +Completed domain: every ordered orthonormal prefix in dimensions 1–7, +including all 1,475,337 complete bases across these dimensions. Stopping rule: +finish dimension 7, with no randomized search or extrapolation. The assignment +seed selects the audited object, not a subset of bases. + +## Exact invoice arithmetic and controls + +Put `g=|Iso(F₂^73,B)|`, `W=7670g`, `s=520704g`, `L=4711738180507680g+64`, +and `C=64·74³=25934336`. The audited expressions are + +```text +router = C (L+1) (W+1)² +literal = 2·2^30000 W² + 8s + 4W + 4 + 32·73 +mass = s + 2^100000 +precision = 32·73·mass² +tape = 2·mass + 18 +row = 2·bit_length(W) + 9909 + 252 + 1024. +``` + +The new engine uses exact integers and imports no production code. It derives +g by the pair-count recurrence, also checks the algebraically equivalent +product `2^36 ∏[j=0..35](2^72−2^(2j))`, and binds the scalar inputs to the +selected receipt. Results include: + +| Quantity | Recomputed value | Retained condition | +|---|---:|---| +| g bits | 2,628 | Exact order above | +| W bits | 2,641 | Exact stock above | +| Router bits | 7,985 | router < 2^30000 | +| Literal bits | 35,282 | literal < 2^100000 | +| Precision bits | 200,012 | precision < 2^210000 | +| Row coefficient | 16,467 | row < 20,161 | + +The certificate also records logical, mass, tape, local-primitive and halving +checks. These are the **nine finite invoice guards**, not the full set of +47 assembly inequalities or an independent moment computation. + +Five controls replace g by 1, the dimension-72 bilinear order, `S(70)`, the +odd part of g, or `|GL(73,2)|=∏[j=0..72](2^73−2^j)`. All five are rejected +by the exact group check. The first four pass all upper-bound guards; GL fails +only the row guard. Separately, with all other inputs held fixed, inflation +`g ↦ 2^t g` has its last passing integer t at **1846** (row 20,159), and +first failure at **1847** (row 20,161). Since bit length increases by t and +all guards are monotone in g, the two endpoint checks certify the whole +nonnegative integer-t range. This is a sensitivity result for this invoice, +not a paid replacement cover, a revised constant proposal or a new κ. + +## Scope, validation and credit + +No defect was found in the selected group factor or its finite arithmetic. +The result adds independent evidence for one accounting obligation and +explicit wrong-model controls. See [VALIDATION.json](VALIDATION.json) for +commands actually run. The source/code/receipt integrity checks, implementation +mutations, strict-boundary controls and isolated relocated replay complement +the mathematical enumeration. + +All supplier correctness, owner geometry, right-translation realization, +uniform compilation, common-label/mutable-basis realization, whole-call +hosting, normalized residuals, semantic precision, fixed-tape/exact recovery, +bit-supplier H1–H5 and analytic-transfer assumptions remain inherited. No +full cold replay, full repository suite, Linux CI, Lean proof or practical +speedup is claimed. The selected certificate and `upstream/` are unchanged. + +Credit: Jeremy Kothe's #622/#623 construction and finite accounting; Chafik +Boukhalfa's #626 owner map and replay; icekylinx's compiler/invoice lineage; +DreamingOfClouds' finite helper audits; Rohan Arun's #559 recurrence review; +eumemic's #543 bit supplier; the maintainer review and all retained predecessor +notices. #717 independently explores moment/invoice sensitivity and program +permutations; none of its code or results is imported here. + +Prepared for **Sricharan Vagvala (@theon199)** with substantial **OpenAI Codex** assistance +in task selection, mathematical analysis, code, verification and writing. +Apache-2.0, matching the repository. No independent human peer review is claimed. diff --git a/research/orthogonal-cover-invoice-audit/SOURCES.json b/research/orthogonal-cover-invoice-audit/SOURCES.json new file mode 100644 index 0000000000..c73c592d6d --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/SOURCES.json @@ -0,0 +1,30 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "reviewed_heads": { + "626": "660de893d27bb7abd1d5b01b1640207528a5c851", + "623": "e39a615ca601ce5d62abeb24f3fcdb8644ca1005", + "622": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "543": "2065fe4f72a914d907f1046603f5a36f17018535" + }, + "sha256": { + "certificates/selected-result.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53", + "docs/research/community-k492-review.md": "3b731d30e80010b15408a289b0b32192700885474c8b36d48ee3320a7a8c5c47", + "research/community-k492-audit/SELECTED-SOURCE.json": "36e9e421230c4cb7b6a537d76a4bdfb6f667730d383e56062d4e45957484ab9e", + "research/community-k492-audit/pr626/replay/ASSEMBLY.json": "6127732e2fcdd470dab349c1c51d03cd9f0787ad0309b1b4a7c811a908028f4e", + "research/community-k492-audit/pr626/replay/mixed-global/audit/PREFIX-AND-INVOICE.json": "367a73f744ea9b7dd6cca5fa3fda47175f560aa3d37e708c9fa1294dbd4b56eb", + "research/community-k492-audit/pr626/replay/mixed-global/audit/OWNERS-AND-PROFILE.json": "ec7bc4157e7ab1707bddf99994149c932b51365de7e742508fd182051ca57fc1", + "research/complex-k492-owner-repair/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "research/complex-k492-owner-repair/code/assemble.py": "1b1a9024ac910dc9b9d9e30150684e1fa9cb228a4c1c275b75ab04b57fdef1dd", + "notes/three-stage-cover-complex.tex": "1c5b638aa9b75365b8addec9c8eeee6bc5e499722901079b94c65fce033fde8a" + }, + "external_reference": { + "author": "Daniel Dugger", + "title": "Involutions in the topologists\u2019 orthogonal group", + "url": "https://pages.uoregon.edu/ddugger/invto121616.pdf", + "anchors": [ + "Proposition 2.3", + "Proposition 2.4" + ], + "role": "Background cross-check only; not a runtime dependency. Proof and exact counting are included here." + } +} diff --git a/research/orthogonal-cover-invoice-audit/VALIDATION.json b/research/orthogonal-cover-invoice-audit/VALIDATION.json new file mode 100644 index 0000000000..a247bc2f94 --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/VALIDATION.json @@ -0,0 +1,67 @@ +{ + "status": "PASS_SCOPED_LOCAL_VALIDATION", + "environment": { + "python": "3.14.5", + "implementation": "CPython", + "system": "Darwin", + "machine": "arm64" + }, + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "commands": [ + { + "command": "python3 -I -B research/orthogonal-cover-invoice-audit/verify.py", + "result": "PASS_ORTHOGONAL_COVER_INVOICE_AUDIT dimensions=1..7 guards=9 controls=5 kappa=unchanged" + }, + { + "command": "python3 -I -B research/orthogonal-cover-invoice-audit/test_verify.py", + "result": "8 tests passed" + }, + { + "command": "python3 -I -B -O research/orthogonal-cover-invoice-audit/verify.py", + "result": "Same PASS and exact certificate under optimized isolated Python" + }, + { + "command": "make selected-record-check", + "result": "PASS selected record, exact kappa, original source inventory and proof supplement" + } + ], + "coverage": { + "complete_ordered_orthonormal_bases": 1475337, + "enumeration_dimensions": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "independent_all_binary_matrix_dimensions": [ + 1, + 2, + 3, + 4 + ], + "finite_invoice_guards": 9, + "wrong_cover_order_controls": 5, + "implementation_mutations": [ + "missing symplectic factor of two", + "omitted 1024-bit row prefix reserve" + ], + "integrity_controls": [ + "invoice bytes changed", + "production source bytes changed", + "certificate router-bit field changed" + ], + "portability": "Minimal relocated repository containing only package and nine pinned files, path with spaces, Python -I -B -O", + "strict_boundary": "g*2^1846 passes; g*2^1847 reaches forbidden row equality; g*2^1848 also fails" + }, + "not_run": [ + "Full make verify (regenerates unrelated historical artifacts)", + "Full cold supplier replay (supplier unchanged)", + "Full set of 47 assembly inequalities and the exact moment engines", + "Linux CI", + "Lean" + ], + "limitations": "No production construction or selected-frontier changes. Group theorem is a written mathematical argument with finite checks, not a formal proof of multiplication. All supplier/compiler/hosting/precision/tape/analytic assumptions remain." +} diff --git a/research/orthogonal-cover-invoice-audit/test_verify.py b/research/orthogonal-cover-invoice-audit/test_verify.py new file mode 100644 index 0000000000..ab5727ac1b --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/test_verify.py @@ -0,0 +1,136 @@ +#!/usr/bin/env python3 +"""Independent small-matrix and adversarial checks for this scoped audit.""" + +import importlib.util +import itertools +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest import mock + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +spec = importlib.util.spec_from_file_location("cover_audit", HERE / "verify.py") +audit = importlib.util.module_from_spec(spec) +spec.loader.exec_module(audit) + + +def brute_matrices(n, check_cross_terms=True): + """Enumerate all 2^(n*n) matrices, independently of prefix pruning.""" + count = 0 + for columns in itertools.product(range(1 << n), repeat=n): + gram = [[sum(((u >> k) & 1) * ((v >> k) & 1) for k in range(n)) % 2 + for v in columns] for u in columns] + pairs = itertools.product(range(n), repeat=2) if check_cross_terms else ((i, i) for i in range(n)) + if all(gram[i][j] == int(i == j) for i, j in pairs): + count += 1 + if check_cross_terms: + image = 0 + for v in columns: + image ^= v + if image != (1 << n) - 1: + raise ValueError("isometry moved characteristic vector") + return count + + +class AuditTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.result = audit.run(ROOT) + _, cls.invoice, cls.owners = audit.load_sources(ROOT) + + def test_full_matrix_enumeration(self): + for n in range(1, 5): + with self.subTest(n=n): + self.assertEqual(brute_matrices(n), self.result["enumeration"][n-1]["complete_bases"]) + + def test_norms_alone_are_not_isometry(self): + # Unit columns can be duplicated and need not be pairwise orthogonal. + self.assertEqual(brute_matrices(3, check_cross_terms=False), 64) + self.assertEqual(brute_matrices(3), 6) + + def test_odd_characteristic_vector_cannot_start_a_basis(self): + for row in self.result["enumeration"]: + if row["dimension"] in (3, 5, 7): + self.assertEqual(row["characteristic_vector_completions"], 0) + self.assertEqual(row["first_column_completion_histogram"]["0"], 1) + + def test_actual_group_order_mutation_is_detected(self): + original = audit.symplectic_order + # Drop a factor 2 in every positive-dimensional group computation. + with mock.patch.object(audit, "symplectic_order", side_effect=lambda n: original(n) // (2 if n else 1)): + with self.assertRaisesRegex(ValueError, "enumeration/order disagreement"): + audit.run(ROOT) + + def test_actual_row_cost_mutation_is_detected(self): + original = audit.invoice_metrics + + def omit_prefix_reserve(*args): + result = original(*args) + result["finite"]["physical_row_coefficient"] -= 1024 + return result + + with mock.patch.object(audit, "invoice_metrics", side_effect=omit_prefix_reserve): + with self.assertRaisesRegex(ValueError, "finite receipt mismatch"): + audit.run(ROOT) + + def test_strict_row_boundary_and_gl_substitution(self): + g = audit.dot_group_order(73) + for t, row, accepted in ((1846, 20159, True), (1847, 20161, False), (1848, 20163, False)): + measured = audit.invoice_metrics(g << t, self.invoice, self.owners) + self.assertEqual(measured["finite"]["physical_row_coefficient"], row) + self.assertEqual(all(measured["strict_checks"].values()), accepted) + self.assertEqual(self.result["negative_controls"]["use_all_invertible_matrices"]["failed_guards"], ["row"]) + + def test_invalid_dimensions_and_orders(self): + for n in (True, -1, 0, 1.5): + with self.assertRaises(ValueError): + audit.dot_group_order(n) + for n in (True, -2, 1, 2.5): + with self.assertRaises(ValueError): + audit.symplectic_order(n) + for n in (0, 8, True): + with self.assertRaises(ValueError): + audit.enumerate_bases(n) + for g in (0, -1, True): + with self.assertRaises(ValueError): + audit.invoice_metrics(g, self.invoice, self.owners) + + def test_relocation_optimized_execution_and_corruption(self): + pins = json.loads((HERE / "SOURCES.json").read_text()) + with tempfile.TemporaryDirectory(prefix="orthogonal audit with spaces ") as tmp: + root = Path(tmp) + target = root / "research" / HERE.name + shutil.copytree(HERE, target, ignore=shutil.ignore_patterns("__pycache__")) + for name in pins["sha256"]: + destination = root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, destination) + command = [sys.executable, "-I", "-B", "-O", str(target / "verify.py")] + passed = subprocess.run(command, capture_output=True, text=True, cwd=tmp, timeout=30) + self.assertEqual(passed.returncode, 0, passed.stderr) + self.assertIn("PASS_ORTHOGONAL_COVER_INVOICE_AUDIT", passed.stdout) + for source in (audit.INVOICE, audit.CODE + "invoice_allcold.py"): + path = root / source + original = path.read_bytes() + path.write_bytes(original + b"\n") + failed = subprocess.run(command, capture_output=True, text=True, cwd=tmp, timeout=30) + self.assertNotEqual(failed.returncode, 0) + self.assertIn("source hash mismatch", failed.stderr) + path.write_bytes(original) + certificate = target / "CERTIFICATE.json" + changed = json.loads(certificate.read_text()) + changed["dimension_73"]["finite"]["router_bits"] -= 1 + certificate.write_text(json.dumps(changed)) + failed = subprocess.run(command, capture_output=True, text=True, cwd=tmp, timeout=30) + self.assertNotEqual(failed.returncode, 0) + self.assertIn("certificate mismatch", failed.stderr) + + +if __name__ == "__main__": + unittest.main(verbosity=2) diff --git a/research/orthogonal-cover-invoice-audit/verify.py b/research/orthogonal-cover-invoice-audit/verify.py new file mode 100644 index 0000000000..f6d25bf5cb --- /dev/null +++ b/research/orthogonal-cover-invoice-audit/verify.py @@ -0,0 +1,266 @@ +#!/usr/bin/env python3 +"""Exact, scoped audit of the binary dot-product cover in the #626 invoice. + +Prepared for theon199 with substantial OpenAI Codex assistance. Apache-2.0. +Standard library only; no construction or production verifier is imported. +""" + +import argparse +from collections import Counter +import hashlib +import json +from pathlib import Path +import sys + + +HERE = Path(__file__).resolve().parent +BASE = "66849e1475c930fd7732b1a0067ffee7e1e95f60" +REPLAY = "research/community-k492-audit/pr626/replay/" +SELECTED = "certificates/selected-result.json" +ASSEMBLY = REPLAY + "ASSEMBLY.json" +INVOICE = REPLAY + "mixed-global/audit/PREFIX-AND-INVOICE.json" +OWNERS = REPLAY + "mixed-global/audit/OWNERS-AND-PROFILE.json" +MANIFEST = "research/community-k492-audit/SELECTED-SOURCE.json" +CODE = "research/complex-k492-owner-repair/code/" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def load_sources(root): + pins = json.loads((HERE / "SOURCES.json").read_text()) + require(pins["base_commit"] == BASE, "unexpected base commit") + raw = {} + for name, digest in pins["sha256"].items(): + data = (root / name).read_bytes() + require(sha256(data) == digest, "source hash mismatch: " + name) + raw[name] = data + selected = json.loads(raw[SELECTED]) + assembly, invoice, owners = (json.loads(raw[p]) for p in (ASSEMBLY, INVOICE, OWNERS)) + manifest = json.loads(raw[MANIFEST]) + require(selected["certificate"] == ASSEMBLY, "selected certificate path") + require(selected["certificate_sha256"] == sha256(raw[ASSEMBLY]), "selected assembly hash") + require(selected["source_manifest"] == MANIFEST, "selected source manifest") + require(selected["audited_source_head"] == pins["reviewed_heads"]["626"], "selected source head") + for pr, head in pins["reviewed_heads"].items(): + require(selected["reviewed_dependency_heads"][pr] == head, "reviewed head: " + pr) + for name in (CODE + "invoice_allcold.py", CODE + "assemble.py"): + require(manifest["files"][name] == sha256(raw[name]), "selected code binding: " + name) + require(assembly["input_sha256"]["fresh_invoice"] == sha256(raw[INVOICE]), "assembly invoice binding") + require(assembly["input_sha256"]["owner_audit"] == sha256(raw[OWNERS]), "assembly owner binding") + require(invoice["owner_audit_sha256"] == sha256(raw[OWNERS]), "invoice owner binding") + require(assembly["template_sha256"] == invoice["template_sha256"] == owners["template_sha256"], "template binding") + require(assembly["kappa"] == selected["kappa"], "selected kappa binding") + return selected, invoice, owners + + +def symplectic_order(dimension): + """Count ordered hyperbolic bases by the successive pair choices.""" + require(type(dimension) is int and dimension >= 0 and dimension % 2 == 0, + "symplectic dimension must be a nonnegative even integer") + count = 1 + for remaining in range(2, dimension + 1, 2): + count *= ((1 << remaining) - 1) * (1 << (remaining - 1)) + return count + + +def dot_group_order(dimension): + require(type(dimension) is int and dimension >= 1, "positive integer dimension required") + if dimension % 2: + return symplectic_order(dimension - 1) + # The even characteristic line has 2^(dimension-1) orthogonal lifts. + return (1 << (dimension - 1)) * symplectic_order(dimension - 2) + + +def enumerate_bases(dimension): + """Visit every ordered orthonormal prefix, with no group/order formula. + + Bits of `available` index actual binary vectors. Appending v intersects + with its orthogonal complement. Unit norm makes v exclude itself; the + identity Gram matrix makes every prefix linearly independent. + """ + require(type(dimension) is int and 1 <= dimension <= 7, "enumeration domain is 1..7") + unit_vectors = [v for v in range(1 << dimension) if v.bit_count() % 2] + orthogonal = { + v: sum(1 << w for w in unit_vectors if (v & w).bit_count() % 2 == 0) + for v in unit_vectors + } + initial = sum(1 << v for v in unit_vectors) + prefixes = [0] * (dimension + 1) + prefixes[0] = 1 + + def visit(depth, available): + prefixes[depth] += 1 + if depth == dimension: + return 1 + total, siblings = 0, available + while siblings: + bit = siblings & -siblings + siblings -= bit + v = bit.bit_length() - 1 + total += visit(depth + 1, available & orthogonal[v]) + return total + + completions = {v: visit(1, initial & orthogonal[v]) for v in unit_vectors} + return { + "dimension": dimension, + "complete_bases": sum(completions.values()), + "prefix_counts": prefixes, + "first_column_completion_histogram": { + str(k): v for k, v in sorted(Counter(completions.values()).items()) + }, + "characteristic_vector_completions": completions.get((1 << dimension) - 1), + } + + +def audit_inputs(invoice, owners): + for name in ("physical", "live", "compiler", "local_primitive_bound", "conservative_pervertex_used"): + require(type(invoice[name]) is int and invoice[name] > 0, "invalid invoice field: " + name) + require(invoice["physical"] == owners["physical"] == 7670, "physical stock") + require(invoice["live"] == owners["live"] == 7168, "live stock") + require(invoice["compiler"] == 64 * 74**3, "compiler charge") + profile = {int(r): count for r, count in owners["paid_profile"].items()} + require(all(0 < r < 73 and type(c) is int and c > 0 for r, c in profile.items()), "rank domain") + require(sum(r * c for r, c in profile.items()) == owners["rank_mass"] == 520704, "rank mass") + require(73 * owners["live"] - owners["rank_mass"] == owners["deficit"] == 2560, "deficit") + require(invoice["charged_prefix_bits"] == 512 and invoice["row_prefix_extra"] == 1024, "prefix reserve") + return profile + + +def invoice_metrics(group, invoice, owners): + """Re-evaluate only the finite guards, holding the admitted invoice fixed.""" + require(type(group) is int and group > 0, "positive integer group order required") + stock = group * invoice["physical"] + streamed = group * owners["rank_mass"] + logical = group * invoice["conservative_pervertex_used"] + 64 + router = invoice["compiler"] * (logical + 1) * (stock + 1)**2 + literal = (1 << 30001) * stock**2 + 8 * streamed + 4 * stock + 4 + 32 * 73 + mass = streamed + (1 << 100000) + precision = 32 * 73 * mass**2 + tape = 2 * mass + 18 + row = 2 * stock.bit_length() + 9909 + 252 + 1024 + maxchild = max(map(int, owners["paid_profile"])) + guards = { + "local_primitive_bound": (invoice["local_primitive_bound"], 48), + "logical": (logical, 6050), "router": (router, 30000), + "literal": (literal, 100000), "mass": (mass, 100001), + "precision": (precision, 210000), "tape": (tape, 210000), + } + checks = {name: value < (1 << exponent) for name, (value, exponent) in guards.items()} + checks.update(row=row < 20161, halving=73**2 > 2 * maxchild**2) + finite = { + "physical_stock_bits": stock.bit_length(), "router_bits": router.bit_length(), + "literal_bits": literal.bit_length(), "physical_row_coefficient": row, + "retained_row_coefficient": 20161, "required_C0_bits": precision.bit_length(), + "halving_integer_inequality": [73**2, 2 * maxchild**2], + "G_exponent": 30000, "E_exponent": 100000, "C0_exponent": 210000, + } + return { + "group_bits": group.bit_length(), "finite": finite, "strict_checks": checks, + "guard_bits": {name: {"actual_bits": value.bit_length(), "bound_exponent": exponent} + for name, (value, exponent) in guards.items()}, + } + + +def require_correct_cover(group): + require(group == dot_group_order(73), "wrong binary dot-product cover order") + + +def run(root): + selected, invoice, owners = load_sources(root) + audit_inputs(invoice, owners) + small = [enumerate_bases(n) for n in range(1, 8)] + for row in small: + require(row["complete_bases"] == dot_group_order(row["dimension"]), "enumeration/order disagreement") + group = dot_group_order(73) + # A different exact product, plus the direct enumeration above. No floats. + classical_product = (1 << 36) + for j in range(36): + classical_product *= (1 << 72) - (1 << (2 * j)) + require(group == classical_product, "alternative order product") + actual = invoice_metrics(group, invoice, owners) + require(actual["finite"] == invoice["finite"], "finite receipt mismatch") + require(actual["strict_checks"] == invoice["strict_checks"], "strict receipt mismatch") + require(all(actual["strict_checks"].values()), "selected guard failed") + + # These are intentionally invalid models; they do not mutate production. + mutants = { + "omit_cover_multiplicity": 1, + "use_even_dimension_72": dot_group_order(72), + "omit_last_symplectic_pair": symplectic_order(70), + "omit_powers_of_two": group >> (36 * 36), + "use_all_invertible_matrices": 1, + } + for j in range(73): + mutants["use_all_invertible_matrices"] *= (1 << 73) - (1 << j) + controls = {} + for name, wrong_group in mutants.items(): + try: + require_correct_cover(wrong_group) + except ValueError: + rejected = True + else: + rejected = False + require(rejected, "group control escaped: " + name) + metrics = invoice_metrics(wrong_group, invoice, owners) + controls[name] = { + "cover_binding_rejected": rejected, + "group_bits": wrong_group.bit_length(), + "failed_guards": [k for k, ok in metrics["strict_checks"].items() if not ok], + "physical_row_coefficient": metrics["finite"]["physical_row_coefficient"], + } + require(all(not controls[name]["failed_guards"] for name in mutants if name != "use_all_invertible_matrices"), + "undercount control should demonstrate guards alone are insufficient") + + # Monotone one-parameter stress test: this changes only cover multiplicity. + last = (20160 - actual["finite"]["physical_row_coefficient"]) // 2 + before = invoice_metrics(group << last, invoice, owners) + after = invoice_metrics(group << (last + 1), invoice, owners) + require(all(before["strict_checks"].values()), "last safe inflation failed") + failures = [k for k, ok in after["strict_checks"].items() if not ok] + require(failures == ["row"], "first inflation failure is not row-only") + return { + "status": "PASS_ORTHOGONAL_COVER_INVOICE_AUDIT", + "base_commit": BASE, "assignment_seed": 65, + "scope": "Binary dot-product cover order and finite invoice only; no new kappa or full theorem proof.", + "selected_kappa_unchanged": selected["kappa"], + "enumeration": small, + "dimension_73": {"exact_group_order": str(group), **actual}, + "negative_controls": controls, + "cover_only_inflation": { + "last_passing_power_of_two": last, + "last_passing_row_coefficient": before["finite"]["physical_row_coefficient"], + "first_failing_power_of_two": last + 1, + "first_failing_row_coefficient": after["finite"]["physical_row_coefficient"], + "first_failed_guards": failures, + "scope": "All other admitted invoice quantities fixed; not a construction or supplier improvement.", + }, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--root", type=Path, default=HERE.parents[1]) + parser.add_argument("--write-certificate", type=Path) + args = parser.parse_args() + result = run(args.root) + if args.write_certificate: + args.write_certificate.write_text(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(result == expected, "certificate mismatch") + print(result["status"] + " dimensions=1..7 guards=9 controls=5 kappa=unchanged") + + +if __name__ == "__main__": + try: + main() + except (ValueError, KeyError, OSError, TypeError) as exc: + print("FAIL_ORTHOGONAL_COVER_INVOICE_AUDIT: " + str(exc), file=sys.stderr) + sys.exit(1) From 340bedf9f0e65bb0e00ee6edb55d8fed11fcb7c7 Mon Sep 17 00:00:00 2001 From: Sricharan Vagvala Date: Mon, 12 Oct 2026 22:24:49 -0700 Subject: [PATCH 2/2] Record audit completion and PR handoff --- research/orthogonal-cover-invoice-audit/CLAIM.md | 11 ++++++++--- .../orthogonal-cover-invoice-audit/VALIDATION.json | 7 ++++++- 2 files changed, 14 insertions(+), 4 deletions(-) diff --git a/research/orthogonal-cover-invoice-audit/CLAIM.md b/research/orthogonal-cover-invoice-audit/CLAIM.md index 120c71a2df..09622b82a4 100644 --- a/research/orthogonal-cover-invoice-audit/CLAIM.md +++ b/research/orthogonal-cover-invoice-audit/CLAIM.md @@ -54,8 +54,13 @@ whereas using GL(73,2) violates the row cap. Exact cover-only inflation reaches its first failed guard at a factor of 2^1847. No construction defect or new kappa is claimed. See README.md, CERTIFICATE.json and VALIDATION.json. -The final full-queue check covered 586 open PRs through #767; no ambient +The final full-queue check covered 586 open PRs through #767, followed by +an immediate pre-submission latest-arrival check through #769; no ambient cover-cardinality audit was found. #717 remains distinct (moment/invoice sensitivity and finite program permutations). Upstream main is still the -recorded base. No coordination issue exists, so the completion link is recorded -here after submission. +recorded base. No coordination issue exists, so the result is recorded locally. + +Submitted: https://github.com/CrocSwap/integer-mult-bounds/pull/771 +Completion recorded: 2026-10-13 05:24:47 UTC. +The contribution finished early; verification and packaging occupied the final +portion of the session. No work remains on the claimed mathematical scope. diff --git a/research/orthogonal-cover-invoice-audit/VALIDATION.json b/research/orthogonal-cover-invoice-audit/VALIDATION.json index a247bc2f94..82cb25a93a 100644 --- a/research/orthogonal-cover-invoice-audit/VALIDATION.json +++ b/research/orthogonal-cover-invoice-audit/VALIDATION.json @@ -23,6 +23,10 @@ { "command": "make selected-record-check", "result": "PASS selected record, exact kappa, original source inventory and proof supplement" + }, + { + "command": "git diff --cached --check", + "result": "PASS, no whitespace errors" } ], "coverage": { @@ -63,5 +67,6 @@ "Linux CI", "Lean" ], - "limitations": "No production construction or selected-frontier changes. Group theorem is a written mathematical argument with finite checks, not a formal proof of multiplication. All supplier/compiler/hosting/precision/tape/analytic assumptions remain." + "limitations": "No production construction or selected-frontier changes. Group theorem is a written mathematical argument with finite checks, not a formal proof of multiplication. All supplier/compiler/hosting/precision/tape/analytic assumptions remain.", + "upstream_unchanged": "Verified no changes to upstream/, certificates/, docs/, scripts/ or Makefile against the exact base." }