From 3d793eade8de2ba49ec08f8d004c1b2f566a78e6 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 20:27:33 +0100 Subject: [PATCH] feat(research): prove exact extreme-rank BIT header densities --- research/projector-header-density/PROOF.md | 129 ++++++++ research/projector-header-density/README.md | 79 +++++ research/projector-header-density/RESULT.json | 300 ++++++++++++++++++ .../projector-header-density/SOURCES.json | 30 ++ research/projector-header-density/TASK.json | 80 +++++ .../projector-header-density/VERIFICATION.md | 50 +++ research/projector-header-density/VERIFY.json | 35 ++ research/projector-header-density/counts.py | 216 +++++++++++++ research/projector-header-density/verify.py | 125 ++++++++ 9 files changed, 1044 insertions(+) create mode 100644 research/projector-header-density/PROOF.md create mode 100644 research/projector-header-density/README.md create mode 100644 research/projector-header-density/RESULT.json create mode 100644 research/projector-header-density/SOURCES.json create mode 100644 research/projector-header-density/TASK.json create mode 100644 research/projector-header-density/VERIFICATION.md create mode 100644 research/projector-header-density/VERIFY.json create mode 100644 research/projector-header-density/counts.py create mode 100644 research/projector-header-density/verify.py diff --git a/research/projector-header-density/PROOF.md b/research/projector-header-density/PROOF.md new file mode 100644 index 0000000000..d434098ed9 --- /dev/null +++ b/research/projector-header-density/PROOF.md @@ -0,0 +1,129 @@ +# Exact extreme-rank header densities + +This is a scoped counting proof. The finite replay corroborates it; the replay +is not a proof for every dimension or a complete multiplication theorem. + +Let F be a finite field of order q, let m >= 2, and fix a split rank-r +projector P0. For a header g in GL_m(F), put P = g P0 g^-1. Call g good +when every leading k-by-k principal minor of P is nonzero, for 1 <= k <= r. +This is the criterion in section 3 of the retained recursive closure. + +Write + + T = q^(m-1) (q^m - 1)/(q-1), + A = q^(m-2) ((q-1) q^(m-1) + 1), + B = (q^2-q+1)^(m-1). + +There are T rank-one projectors and T corank-one projectors. Exactly A +rank-one projectors and B corank-one projectors are good. Therefore the +complete-header good fractions are A/T and B/T, respectively. In particular, +the exact rank-one bad fraction is + + (2q-1)(q^(m-1)-1) / (q(q^m-1)) < 2/q. + +The theorem includes every finite field. The retained caller uses odd prime q. +The executable census uses prime fields only. + +## 1. Why a projector count is a header count + +Every rank-r projector is conjugate to diag(I_r,0), by choosing image and +kernel bases. The stabilizer consists exactly of block-diagonal matrices +with blocks in GL_r(F) and GL_(m-r)(F). Thus every projector has the same +number |GL_r(F)| |GL_(m-r)(F)| of header preimages. Multiplication of g on +the right by any fixed owner chart or image/kernel basis is a bijection. +The fractions do not depend on P0 or that fixed chart. + +This argument uses a complete GL header domain, with equal multiplicity per +header. It is a deterministic count over that domain. A uniformly random +header has the same fraction as a probability. An arbitrary subset need not. + +## 2. Rank one + +A rank-one projector has the form P = u v with u a nonzero column, v a row, +and v u = 1. Exactly q-1 pairs represent the same P, through +(u,v) -> (lambda u, lambda^-1 v). For each of q^m-1 choices of u, the +nonzero linear functional v -> v u has q^(m-1) solutions with value 1. +This gives T. + +The good condition is P[0,0] = u_0 v_0 != 0. Normalize u_0 = 1, which +chooses one representative for each good P. Put z = (u_1,...,u_(m-1)). +When z = 0, v_0 = 1 and the other v coordinates have q^(m-1) choices. +When z != 0, choose any nonzero v_0, and solve + + sum_(i=1)^(m-1) u_i v_i = 1-v_0. + +There are q^(m-2) solutions for each of q-1 nonzero v_0 values and each +of q^(m-1)-1 nonzero z values. Consequently + + A = q^(m-1) + (q^(m-1)-1)(q-1)q^(m-2). + +The displayed closed form and bad fraction follow by expansion. The strict +bound follows since (q^(m-1)-1)/(q^m-1) < 1/q and 2q-1 < 2q. + +## 3. Corank one + +Write P = I-u v with v u = 1. Complementation bijects rank-one and +corank-one projectors, so the total is again T. Put x_i = u_i v_i. +Multilinearity of the determinant gives + + det(I_k-u_[0:k] v_[0:k]) = 1-sum_(i= 1, and R = Z/q^w. Reduction GL_m(R) -> GL_m(F_q) +is onto, and every fiber has q^(m^2(w-1)) elements: lift each entry +arbitrarily, and the determinant remains a unit exactly when its residue +is nonzero. A pivot or minor is a unit in R exactly when its reduction +is nonzero. Therefore every full high-header packet inherits its low +header's good/bad status, and the complete GL_m(R) fractions are unchanged. + +For a fixed split projector over R, the same image/kernel-basis conjugation +argument gives a stabilizer GL_r(R) times GL_(m-r)(R). Combining the group +sizes shows that each residue projector has exactly +q^(2r(m-r)(w-1)) split-projector lifts. This also explains the local-ring +projector counts in the finite replay. No coefficient is truncated to its +low residue when executing the normalizer; only the admission test is low. + +In the source, `prepare` forms P, reverses its columns to form P C, and +at stage k takes column m-1-k. These are the leading-principal pivots of P, +in the opposite column order. With earlier pivots units, the next pivot is +a signed ratio of consecutive leading minors, so the admission criteria +agree. The replay also compares the actual program's accept/reject result. + +## 5. Exact boundary of the consequence + +The retained complete packet model enumerates every low header with the +same number of high lifts for each request. Its per-request bad fraction +is a deterministic counting fraction, without a probabilistic assumption +about the payload or frozen ancestor values. Right-translated fixed charts +preserve that statement. It does not assert that one header works for every +request simultaneously, or that distinct requests have independent tests. + +An adversarial low class can be entirely bad. For rank one, choose P0 with +image coordinate 0 and a header swapping coordinates 0 and m-1. Then P has +P[0,0] = 0. Every high lift of that header is bad. By contrast the identity +header is good. Hence no nontrivial density bound transfers to an arbitrary +header restriction merely because a complete-domain bound holds. + +The selected profile has rank-one requests, so the exact rank-one fraction +can replace a worst-case generic bound in that part of a future audited bill. +Its intermediate ranks and the complete physical recurrence remain separate +obligations. Corank one is a general calibration family, not a claimed +selected request. This package changes no production invoice or frontier. diff --git a/research/projector-header-density/README.md b/research/projector-header-density/README.md new file mode 100644 index 0000000000..63230ead24 --- /dev/null +++ b/research/projector-header-density/README.md @@ -0,0 +1,79 @@ +# Exact extreme-rank BIT header densities + +This package proves exact good-header fractions for rank-one and corank-one +projectors in every dimension m >= 2 over a finite field of order q. The +claim type is a scoped proof with a finite certificate, with no new kappa. + +For the retained normalizer's leading-principal-minor criterion, the total +number of projectors in either family is + + T = q^(m-1)(q^m-1)/(q-1). + +The good counts are + + rank one: q^(m-2)((q-1)q^(m-1)+1), + corank one: (q^2-q+1)^(m-1). + +Divide by T for the good-header fraction. The exact rank-one bad fraction +is `(2q-1)(q^(m-1)-1)/(q(q^m-1)) < 2/q`. The [proof](PROOF.md) passes these +fractions to complete GL headers over Z/q^w, for prime q and every w >= 1. +They are deterministic complete-domain counts. An explicit wholly bad +header class prevents their use on arbitrary restricted header sets. + +The distinction answers the extreme-rank part of #4215's bad-fraction +question with a new counting theorem. It does not repeat the predecessor's +normal-form proof. The current card concerns #4100; [TASK.json](TASK.json) +records the changed scope to the earlier retained normalizer and the reason. + +## Evidence and reproduction + +Use CPython 3.12, standard library only, from the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/projector-header-density/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/projector-header-density +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/projector-header-density --check-source-history +``` + +The replay enumerates canonical rank-one factorizations and their complements, +independently scans all matrices in small field/local-ring domains, enumerates +complete small GL header domains and compares actual source admission tests. +The generated [RESULT.json](RESULT.json) records every domain and counter, +controls and SHA256 of all package files except itself and both live inputs. +The all-matrix census visits 951,417 matrices and finds 2,162 nontrivial +idempotents, with 1,332 good. These aggregates agree numerically with #4215's +reported corpus. The complete-header census visits 315,648 invertible headers. +Normal and optimized registered commands compare that receipt exactly. +To regenerate a candidate outside the checkout, use +`verify.py --write-receipt /new/external/path.json`. It refuses overwrites. + +Controls distinguish the wrong reversal, checking only the final minor, +dropping zero coordinate products and transferring the density to a bad +header subset. A separate direct pair-product dynamic program checks the +corank-one path count without using projector matrices. + +## Limits + +The universal statement rests on the written counting proof, without a formal +kernel or independent human review. The finite implementation uses prime fields. +It does not enumerate GL64, audit intermediate ranks, certify actual selected +residual counts, reprice fallback children or prove the full recursive machine. +No selected source or invoice changes. + +## Open next questions + +Can an exact intermediate-rank density replace the current union bound? +Start at rank two using a canonical image/kernel parametrization, and check +every required leading minor together. The obstacle is their joint distribution, +not another numerical evaluation of an existing root. Before changing an actual +bill, bind all request/header multiplicities and the complete fallback cost. +The structured first steps and blockers are in [TASK.json](TASK.json). + +## Credit + +This result was produced by Nick Petalas. Source527 and commdata2338 retain +the normal-form algebra credit. Jose Manuel retains the recursive closure +and `controlled_normalizer.py` credit. The selected source lineage includes +DreamingOfClouds, eumemic and alephnan, as recorded in the unchanged source +notices. The small-ring normal-form audit in #4215 is a distinct predecessor. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/projector-header-density/RESULT.json b/research/projector-header-density/RESULT.json new file mode 100644 index 0000000000..b8d4ea8581 --- /dev/null +++ b/research/projector-header-density/RESULT.json @@ -0,0 +1,300 @@ +{ + "claim_type": "scoped proof with finite certificate", + "live_input_sha256": { + "research/selected-bit-recursive-closure/PROOF.md": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344", + "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77" + }, + "package_sha256": { + "PROOF.md": "bb69ba3c4a566417cc2ed0227bb7ad48ef69d3368c754fa47600f22b869a6262", + "README.md": "e9f472799d00b1fb956f20efd5f8ac79bd65e14fadbdf371cb89be6a37201d29", + "SOURCES.json": "4639a7d006c6e43d3ec1e291d056ae785d17beb7a3abc9c11a1b92a583f5494f", + "TASK.json": "44ab40fd45865ac1183c67d7732140105f4b015661a6c1f40adf8de5e1016f40", + "VERIFICATION.md": "44aa429999926222435955bae873237629b2376e55515129ee471e5de5ed1dc7", + "VERIFY.json": "ab2eb6ee6720f467b276b833d25bcd0ec0ac20cd59f21f8c995fbab66000e87e", + "counts.py": "d00199bc802f393c50eda0cc2fd30a4fe358810eeabbbe64a9ff174b35426a66", + "verify.py": "9fffbd606ecc502b5e9f53b81d91b97dc0f1b0a89f5de093022605804a693a9d" + }, + "result": { + "all_matrix_census": [ + { + "m": 2, + "matrices": 81, + "q": 3, + "ranks": { + "1": { + "good": 7, + "total": 12 + } + }, + "w": 1 + }, + { + "m": 2, + "matrices": 625, + "q": 5, + "ranks": { + "1": { + "good": 21, + "total": 30 + } + }, + "w": 1 + }, + { + "m": 2, + "matrices": 2401, + "q": 7, + "ranks": { + "1": { + "good": 43, + "total": 56 + } + }, + "w": 1 + }, + { + "m": 2, + "matrices": 6561, + "q": 3, + "ranks": { + "1": { + "good": 63, + "total": 108 + } + }, + "w": 2 + }, + { + "m": 2, + "matrices": 390625, + "q": 5, + "ranks": { + "1": { + "good": 525, + "total": 750 + } + }, + "w": 2 + }, + { + "m": 2, + "matrices": 531441, + "q": 3, + "ranks": { + "1": { + "good": 567, + "total": 972 + } + }, + "w": 3 + }, + { + "m": 3, + "matrices": 19683, + "q": 3, + "ranks": { + "1": { + "good": 57, + "total": 117 + }, + "2": { + "good": 49, + "total": 117 + } + }, + "w": 1 + } + ], + "canonical_projectors": [ + { + "good_corank_one": 7, + "good_rank_one": 7, + "m": 2, + "q": 3, + "total_per_rank": 12 + }, + { + "good_corank_one": 49, + "good_rank_one": 57, + "m": 3, + "q": 3, + "total_per_rank": 117 + }, + { + "good_corank_one": 343, + "good_rank_one": 495, + "m": 4, + "q": 3, + "total_per_rank": 1080 + }, + { + "good_corank_one": 2401, + "good_rank_one": 4401, + "m": 5, + "q": 3, + "total_per_rank": 9801 + }, + { + "good_corank_one": 21, + "good_rank_one": 21, + "m": 2, + "q": 5, + "total_per_rank": 30 + }, + { + "good_corank_one": 441, + "good_rank_one": 505, + "m": 3, + "q": 5, + "total_per_rank": 775 + }, + { + "good_corank_one": 9261, + "good_rank_one": 12525, + "m": 4, + "q": 5, + "total_per_rank": 19500 + }, + { + "good_corank_one": 43, + "good_rank_one": 43, + "m": 2, + "q": 7, + "total_per_rank": 56 + }, + { + "good_corank_one": 1849, + "good_rank_one": 2065, + "m": 3, + "q": 7, + "total_per_rank": 2793 + }, + { + "good_corank_one": 111, + "good_rank_one": 111, + "m": 2, + "q": 11, + "total_per_rank": 132 + } + ], + "complete_header_census": [ + { + "actual_source_admission_checks": 48, + "good": { + "1": 28 + }, + "headers": 48, + "m": 2, + "q": 3, + "w": 1 + }, + { + "actual_source_admission_checks": 480, + "good": { + "1": 336 + }, + "headers": 480, + "m": 2, + "q": 5, + "w": 1 + }, + { + "actual_source_admission_checks": 3888, + "good": { + "1": 2268 + }, + "headers": 3888, + "m": 2, + "q": 3, + "w": 2 + }, + { + "actual_source_admission_checks": 3097, + "good": { + "1": 210000 + }, + "headers": 300000, + "m": 2, + "q": 5, + "w": 2 + }, + { + "actual_source_admission_checks": 22464, + "good": { + "1": 5472, + "2": 4704 + }, + "headers": 11232, + "m": 3, + "q": 3, + "w": 1 + } + ], + "controls": { + "bad_high_lifts": 81, + "bad_restricted_header_subset": true, + "complete_product_paths": 98, + "final_minor_only_rejected": true, + "omitted_zero_product_paths": 8, + "wrong_reversal_rejected": true, + "zero_coordinate_products_retained": true + }, + "independent_product_paths": [ + { + "m": 2, + "pairs_ending_at_one": 14, + "q": 3 + }, + { + "m": 3, + "pairs_ending_at_one": 98, + "q": 3 + }, + { + "m": 4, + "pairs_ending_at_one": 686, + "q": 3 + }, + { + "m": 5, + "pairs_ending_at_one": 4802, + "q": 3 + }, + { + "m": 2, + "pairs_ending_at_one": 84, + "q": 5 + }, + { + "m": 3, + "pairs_ending_at_one": 1764, + "q": 5 + }, + { + "m": 4, + "pairs_ending_at_one": 37044, + "q": 5 + }, + { + "m": 2, + "pairs_ending_at_one": 258, + "q": 7 + }, + { + "m": 3, + "pairs_ending_at_one": 11094, + "q": 7 + }, + { + "m": 2, + "pairs_ending_at_one": 1110, + "q": 11 + } + ], + "small_ring_aggregate": { + "good": 1332, + "projectors": 2162 + } + }, + "schema_version": 1 +} diff --git a/research/projector-header-density/SOURCES.json b/research/projector-header-density/SOURCES.json new file mode 100644 index 0000000000..db41dfe906 --- /dev/null +++ b/research/projector-header-density/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/selected-bit-recursive-closure/PROOF.md", + "usage": "input", + "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531", + "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344" + }, + { + "path": "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py", + "usage": "input", + "git_blob": "3e8a72e7ce705c51ff24e9015ccf6463204ff193", + "sha256": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77" + } + ] +} diff --git a/research/projector-header-density/TASK.json b/research/projector-header-density/TASK.json new file mode 100644 index 0000000000..bfb0bc0417 --- /dev/null +++ b/research/projector-header-density/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact rank-one and corank-one good-header densities for the retained selected BIT normalizer, with complete local-ring packet lifting.", + "scope_change_reason": "The current card targets the #4100 all-size proof, already reserved by another contributor. This takes the new counting question raised by #4215 and derives an all-dimension theorem on the earlier retained normalizer instead of repeating its normal-form audit.", + "bottleneck_link": "A complete-header counting formula sharpens the rank-one fallback fraction and states the exact enumeration premise. Intermediate ranks, a complete fallback bill and supplier admission remain separate.", + "budget_minutes": 60, + "stop_rule": "Stop after the two extreme-rank formulas, their complete-packet lifting and bounded corroboration; do not extend into an intermediate-rank search or reprice a supplier.", + "outcome": "completed", + "evidence": "PROOF.md contains the scoped counting proof. RESULT.json is generated by verify.py and binds all package bytes and both live inputs to exhaustive census counters and source admission checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact joint leading-minor density at intermediate rank, beginning with rank two?", + "why_it_matters": "The selected profile also has intermediate ranks, which the extreme-rank theorem cannot price.", + "first_step": "Parametrize rank-two image/kernel pairs and derive the joint two-minor count before a bounded small-field census.", + "blocked_by": "No joint-distribution formula is provided here." + }, + { + "question": "Can the exact rank-one fraction be used in a complete admitted fallback invoice?", + "why_it_matters": "A density alone does not close the recurrence or the physical supplier.", + "first_step": "Bind request/header multiplicities and the complete fallback-child cost at one retained caller without changing its complete-domain premise.", + "blocked_by": "Intermediate-rank rates, physical costs and supplier admission are outside this package." + } + ] +} diff --git a/research/projector-header-density/VERIFICATION.md b/research/projector-header-density/VERIFICATION.md new file mode 100644 index 0000000000..09dd6ad7aa --- /dev/null +++ b/research/projector-header-density/VERIFICATION.md @@ -0,0 +1,50 @@ +# Verification boundaries and implementation constraints + +The direct verifier authenticates both live inputs before loading the retained +normalizer. It accepts only its exact `nongeneric low class` rejection as an +ordinary bad-header result. Any other exception fails the replay. It does not +invoke Git or fetch sources. The registered metadata/source-history commands +separately authenticate provenance and publication availability. + +The finite domains are fixed constants in `counts.py`. Matrix scanning has at +most 27^4 candidates in one domain. Header scanning has at most 25^4 candidates +in one domain. Matrix dimensions are at most five; the largest retained set of +canonical projectors has 19,500 entries, each with at most 25 field entries. +Every loop ranges over these fixed finite domains, a bounded matrix dimension, +or the finite package manifest/file inventory. No recursive call occurs. +No performance speedup or memory benchmark is claimed. + +The formulas are checked by a canonical factorization census, a separate +all-matrix idempotent census, complete GL header scans and scalar pair-product +paths. The same minor function is used for projector and header classification; +the actual source's elimination independently checks every GL3(F3) header +at both extreme ranks and every header in domains of modulus at most nine. +The modulus-25 domain uses a deterministic index-mod-97 sample. Source checks +are samples where the receipt says so. +No source endpoint/conjugation or complete physical machine is recertified. + +The code uses explicit failure checks, which remain active with `-O`. No test +replaces a failed check with an assertion. There is no repository-wide linter +configuration for this isolated package. Both registered runs enable Python +warnings as errors. A source/receipt mismatch fails closed. + +## Power of Ten deviations + +Rule 3, fixed allocation: CPython allocates tuples, integers and sets during +enumeration. This is a managed-runtime deviation. The fixed domains above bound +live collections; the matrix/header scans stream candidates and discard them. +The canonical seen-set is released after each domain. Static inspection of +these lifetimes is the evidence; no allocation instrumentation is claimed. +A native implementation with fixed arrays is outside this mathematical task. + +Rules 8 and 9, dynamic loading and dispatch: `verify.py:load_source` loads one +SHA256-authenticated, fixed Python source, which imports only standard-library +modules. Dataclass construction and importlib dispatch are CPython mechanisms. +The only variable callback target is that pinned normalizer's `prepare`. +The direct/cold source-bound replays check this exact path. Inlining the source +would duplicate its provenance and weaken the actual-program comparison. + +The other new functions are below the approximately 60-line review ceiling. +All file writes are confined to the explicit exclusive-create receipt command; +the ordinary verifier and registered commands are read-only. The receipt output +must be a new path outside the repository. Files close through a context manager. diff --git a/research/projector-header-density/VERIFY.json b/research/projector-header-density/VERIFY.json new file mode 100644 index 0000000000..109afa688e --- /dev/null +++ b/research/projector-header-density/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/selected-bit-recursive-closure/PROOF.md", + "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact extreme-rank projector/header densities, all-matrix local-ring census, source admission and boundary controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same source-bound certificate with assertions disabled." + } + ] +} diff --git a/research/projector-header-density/counts.py b/research/projector-header-density/counts.py new file mode 100644 index 0000000000..8e3948dabd --- /dev/null +++ b/research/projector-header-density/counts.py @@ -0,0 +1,216 @@ +"""Exact, bounded finite censuses for the extreme-rank counting theorem.""" + +from itertools import product +from math import gcd + + +VECTOR_DOMAINS = ((3, 2), (3, 3), (3, 4), (3, 5), (5, 2), + (5, 3), (5, 4), (7, 2), (7, 3), (11, 2)) +MATRIX_DOMAINS = ((3, 1, 2), (5, 1, 2), (7, 1, 2), (3, 2, 2), + (5, 2, 2), (3, 3, 2), (3, 1, 3)) +HEADER_DOMAINS = ((3, 1, 2), (5, 1, 2), (3, 2, 2), (5, 2, 2), (3, 1, 3)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def matrix(flat, m): + return tuple(tuple(flat[i*m:(i+1)*m]) for i in range(m)) + + +def determinant(rows, q): + a = [list(row) for row in rows] + m = len(a) + value = 1 + for k in range(m): + pivot = next((i for i in range(k, m) if a[i][k] % q), None) + if pivot is None: + return 0 + if pivot != k: + a[k], a[pivot] = a[pivot], a[k] + value = -value + value = value * a[k][k] % q + inverse = pow(a[k][k], -1, q) + for i in range(k+1, m): + factor = a[i][k] * inverse % q + for j in range(k+1, m): + a[i][j] = (a[i][j] - factor*a[k][j]) % q + return value % q + + +def good(projector, rank, q): + return all(determinant(tuple(row[:k] for row in projector[:k]), q) + for k in range(1, rank+1)) + + +def formula(q, m, rank): + need(m >= 2 and rank in (1, m-1), "extreme-rank formula domain") + total = (q**m-1) * q**(m-1) // (q-1) + if rank == 1: + admitted = q**(m-2) * ((q-1)*q**(m-1)+1) + else: + admitted = (q*q-q+1)**(m-1) + return total, admitted + + +def factorizations(q, m): + """One representative per rank-one projector, with first nonzero u equal 1.""" + for pivot in range(m): + for tail in product(range(q), repeat=m-pivot-1): + u = (0,)*pivot + (1,) + tail + for free in product(range(q), repeat=m-1): + v = list(free[:pivot]) + [0] + list(free[pivot:]) + v[pivot] = (1-sum(u[i]*v[i] for i in range(m))) % q + yield u, tuple(v) + + +def outer(u, v, q, complement=False): + m = len(u) + if complement: + return tuple(tuple((int(i == j)-u[i]*v[j]) % q + for j in range(m)) for i in range(m)) + return tuple(tuple(u[i]*v[j] % q for j in range(m)) for i in range(m)) + + +def vector_census(q, m): + seen = set() + counts = [0, 0] + for u, v in factorizations(q, m): + p = outer(u, v, q) + need(p not in seen, "duplicate canonical rank-one projector") + seen.add(p) + counts[0] += int(good(p, 1, q)) + counts[1] += int(good(outer(u, v, q, True), m-1, q)) + for rank, admitted in zip((1, m-1), counts): + need((len(seen), admitted) == formula(q, m, rank), "vector formula mismatch") + return {"q": q, "m": m, "total_per_rank": len(seen), + "good_rank_one": counts[0], "good_corank_one": counts[1]} + + +def idempotent(p, modulus): + m = len(p) + return all((sum(p[i][k]*p[k][j] for k in range(m))-p[i][j]) % modulus == 0 + for i in range(m) for j in range(m)) + + +def field_rank(p, q): + a = [list(row) for row in p] + m, rank = len(a), 0 + for column in range(m): + pivot = next((i for i in range(rank, m) if a[i][column] % q), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + inverse = pow(a[rank][column] % q, -1, q) + a[rank] = [x*inverse % q for x in a[rank]] + for i in range(rank+1, m): + factor = a[i][column] % q + a[i] = [(x-factor*y) % q for x, y in zip(a[i], a[rank])] + rank += 1 + return rank + + +def matrix_census(q, w, m): + modulus = q**w + counts = {r: [0, 0] for r in sorted({1, m-1})} + for flat in product(range(modulus), repeat=m*m): + p = matrix(flat, m) + if not idempotent(p, modulus): + continue + rank = field_rank(p, q) + if rank in counts: + counts[rank][0] += 1 + counts[rank][1] += int(good(p, rank, q)) + for rank, pair in counts.items(): + lift = q**(2*rank*(m-rank)*(w-1)) + need(pair == [x*lift for x in formula(q, m, rank)], "matrix formula mismatch") + return {"q": q, "w": w, "m": m, "matrices": modulus**(m*m), + "ranks": {str(r): {"total": v[0], "good": v[1]} + for r, v in counts.items()}} + + +def inverse(rows, modulus): + m = len(rows) + a = [list(row)+[int(i == j) for j in range(m)] for i, row in enumerate(rows)] + for k in range(m): + pivot = next((i for i in range(k, m) if gcd(a[i][k], modulus) == 1), None) + need(pivot is not None, "invertible header") + a[k], a[pivot] = a[pivot], a[k] + unit = pow(a[k][k], -1, modulus) + a[k] = [x*unit % modulus for x in a[k]] + for i in range(m): + if i != k: + factor = a[i][k] + a[i] = [(x-factor*y) % modulus for x, y in zip(a[i], a[k])] + return tuple(tuple(row[m:]) for row in a) + + +def projector_from_header(g, gi, axes, modulus): + m = len(g) + return tuple(tuple(sum(g[i][k]*gi[k][j] for k in axes) % modulus + for j in range(m)) for i in range(m)) + + +def source_admits(source, g, axes, q, w): + m = len(g) + prefix = source.ParentPrefix(q, w, tuple(tuple(x % q for x in row) for row in g), + tuple(tuple(x // q for x in row) for row in g), + (1,)*m, 1) + try: + # Only acceptance is consumed here; coefficient/operator auditing is separate. + source.prepare(prefix, axes) + except ValueError as error: + if str(error) == "nongeneric low class": + return False + raise + return True + + +def header_census(q, w, m, source): + modulus = q**w + counts = {r: 0 for r in sorted({1, m-1})} + total = source_checks = 0 + for index, flat in enumerate(product(range(modulus), repeat=m*m)): + g = matrix(flat, m) + if not determinant(g, q): + continue + total += 1 + gi = inverse(g, modulus) + for rank in counts: + axes = tuple(range(rank)) + p = projector_from_header(g, gi, axes, modulus) + accepted = good(p, rank, q) + counts[rank] += int(accepted) + if index % 97 == 0 or m == 3 or modulus <= 9: + need(source_admits(source, g, axes, q, w) == accepted, + "actual northeast admission differs from minor criterion") + source_checks += 1 + gl = 1 + for k in range(m): + gl *= q**m-q**k + need(total == gl*q**(m*m*(w-1)), "complete header count") + for rank, admitted in counts.items(): + ptotal, pgood = formula(q, m, rank) + need(admitted*ptotal == total*pgood, "complete header fraction") + return {"q": q, "w": w, "m": m, "headers": total, + "good": {str(r): v for r, v in counts.items()}, + "actual_source_admission_checks": source_checks} + + +def product_path_census(q, m): + """Use actual scalar pairs, without matrix projectors or the closed formula.""" + pairs = tuple(product(range(q), repeat=2)) + weights = [0]*q + weights[0] = 1 + for _ in range(m): + following = [0]*q + for state in range(q): + for u, v in pairs: + endpoint = (state+u*v) % q + if endpoint: + following[endpoint] += weights[state] + weights = following + need(weights[1] == (q-1)*formula(q, m, m-1)[1], "pair-product path mismatch") + return {"q": q, "m": m, "pairs_ending_at_one": weights[1]} diff --git a/research/projector-header-density/verify.py b/research/projector-header-density/verify.py new file mode 100644 index 0000000000..8ad52f7efc --- /dev/null +++ b/research/projector-header-density/verify.py @@ -0,0 +1,125 @@ +#!/usr/bin/env python3 +"""Replay exact header counts; compare a generated receipt bound to source bytes.""" + +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +import counts + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +SOURCE = "research/selected-bit-recursive-closure/vendor/controlled_normalizer.py" + + +def digest(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def authenticate(): + pins = json.loads((PACKAGE/"SOURCES.json").read_text()) + live = {} + for row in pins["files"]: + if row["usage"] == "input": + path = ROOT/row["path"] + counts.need(digest(path) == row["sha256"], "live source digest mismatch") + live[row["path"]] = row["sha256"] + counts.need(SOURCE in live, "normalizer is not a live source") + return live + + +def load_source(): + spec = importlib.util.spec_from_file_location("header_density_normalizer", ROOT/SOURCE) + counts.need(spec is not None and spec.loader is not None, "source loader") + module = importlib.util.module_from_spec(spec) + sys.modules[spec.name] = module + spec.loader.exec_module(module) + return module + + +def controls(source): + identity = ((1, 0), (0, 1)) + swap = ((0, 1), (1, 0)) + p = ((1, 0), (0, 0)) + counts.need(counts.good(p, 1, 3), "positive leading-minor fixture") + counts.need(not counts.good(tuple(row[::-1] for row in p), 1, 3), + "wrong-reversal control did not distinguish criteria") + counts.need(counts.source_admits(source, identity, (0,), 3, 1), "identity header") + counts.need(not counts.source_admits(source, swap, (0,), 3, 1), "bad header subset") + p3 = counts.outer((1, 1, 1), (1, 1, 2), 3, True) + counts.need(counts.determinant(tuple(row[:2] for row in p3[:2]), 3) != 0 + and not counts.good(p3, 2, 3), "final-minor-only control") + bad_order_header = ((1, 2, 1), (1, 0, 1), (1, 2, 2)) + counts.need(not counts.source_admits(source, bad_order_header, (1, 2), 3, 1), + "source must reject the earlier zero minor") + pairs = tuple((u, v) for u in range(3) for v in range(3) if u*v % 3) + dropped_zero_paths = 0 + for path in counts.product(pairs, repeat=3): + state, admitted = 0, True + for u, v in path: + state = (state+u*v) % 3 + admitted = admitted and state != 0 + dropped_zero_paths += int(admitted and state == 1) + complete_paths = counts.product_path_census(3, 3)["pairs_ending_at_one"] + counts.need(dropped_zero_paths != complete_paths, "zero-product omission went undetected") + bad_lifts = 0 + for high in counts.product(range(3), repeat=4): + flat = tuple(x+3*y for x, y in zip((0, 1, 1, 0), high)) + g = counts.matrix(flat, 2) + counts.need(not counts.source_admits(source, g, (0,), 3, 2), "bad high lift") + bad_lifts += 1 + return {"wrong_reversal_rejected": True, "final_minor_only_rejected": True, + "bad_restricted_header_subset": True, "bad_high_lifts": bad_lifts, + "zero_coordinate_products_retained": True, + "omitted_zero_product_paths": dropped_zero_paths, + "complete_product_paths": complete_paths} + + +def scientific_result(source): + vectors = [counts.vector_census(q, m) for q, m in counts.VECTOR_DOMAINS] + matrices = [counts.matrix_census(q, w, m) for q, w, m in counts.MATRIX_DOMAINS] + headers = [counts.header_census(q, w, m, source) for q, w, m in counts.HEADER_DOMAINS] + paths = [counts.product_path_census(q, m) for q, m in counts.VECTOR_DOMAINS] + aggregate_total = sum(v["total"] for row in matrices for v in row["ranks"].values()) + aggregate_good = sum(v["good"] for row in matrices for v in row["ranks"].values()) + return {"canonical_projectors": vectors, "all_matrix_census": matrices, + "complete_header_census": headers, "independent_product_paths": paths, + "small_ring_aggregate": {"projectors": aggregate_total, "good": aggregate_good}, + "controls": controls(source)} + + +def receipt(): + live = authenticate() + source = load_source() + result = scientific_result(source) + files = {path.name: digest(path) for path in sorted(PACKAGE.iterdir()) + if path.is_file() and path.name != "RESULT.json"} + return {"schema_version": 1, "claim_type": "scoped proof with finite certificate", + "package_sha256": files, "live_input_sha256": live, "result": result} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + if args.write_receipt: + output = args.write_receipt.resolve() + counts.need(not output.exists(), "receipt output already exists") + counts.need(not output.is_relative_to(ROOT), "receipt output must be outside checkout") + result = receipt() + if args.write_receipt: + with args.write_receipt.open("x") as handle: + handle.write(json.dumps(result, indent=2, sort_keys=True)+"\n") + else: + expected = json.loads((PACKAGE/"RESULT.json").read_text()) + counts.need(result == expected, "receipt differs from recomputed source-bound result") + summary = result["result"]["small_ring_aggregate"] + print("PASS_PROJECTOR_HEADER_DENSITY", json.dumps(summary, sort_keys=True)) + + +if __name__ == "__main__": + main()