From 640b43bb13d3d476a2d83b74ef0d33f14d1b5711 Mon Sep 17 00:00:00 2001 From: mightyOil <82899331+mightyOil@users.noreply.github.com> Date: Tue, 13 Oct 2026 21:53:41 +0200 Subject: [PATCH] Research: certify one-sided E8 masked decoder rigidity --- .../CERTIFICATE.json | 41 + .../complex-masked-rigidity-seed28/CLAIM.md | 23 + .../complex-masked-rigidity-seed28/NOTICE.md | 15 + .../complex-masked-rigidity-seed28/OVERLAP.md | 74 + .../complex-masked-rigidity-seed28/PROOF.md | 184 ++ .../complex-masked-rigidity-seed28/README.md | 111 + .../SOURCES.json | 24 + .../TENSOR-CERTIFICATE.json | 1882 +++++++++++++++++ .../VALIDATION.md | 47 + .../tensor_oracle.py | 301 +++ .../complex-masked-rigidity-seed28/verify.py | 197 ++ 11 files changed, 2899 insertions(+) create mode 100644 research/complex-masked-rigidity-seed28/CERTIFICATE.json create mode 100644 research/complex-masked-rigidity-seed28/CLAIM.md create mode 100644 research/complex-masked-rigidity-seed28/NOTICE.md create mode 100644 research/complex-masked-rigidity-seed28/OVERLAP.md create mode 100644 research/complex-masked-rigidity-seed28/PROOF.md create mode 100644 research/complex-masked-rigidity-seed28/README.md create mode 100644 research/complex-masked-rigidity-seed28/SOURCES.json create mode 100644 research/complex-masked-rigidity-seed28/TENSOR-CERTIFICATE.json create mode 100644 research/complex-masked-rigidity-seed28/VALIDATION.md create mode 100644 research/complex-masked-rigidity-seed28/tensor_oracle.py create mode 100644 research/complex-masked-rigidity-seed28/verify.py diff --git a/research/complex-masked-rigidity-seed28/CERTIFICATE.json b/research/complex-masked-rigidity-seed28/CERTIFICATE.json new file mode 100644 index 0000000000..a9d0e33b22 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/CERTIFICATE.json @@ -0,0 +1,41 @@ +{ + "geometry": { + "coordinate_convention": "doubled; first nonzero positive; lexicographic", + "covariance_entries_checked": 7744, + "geometric_cover_limit": 8, + "orthogonal_counts": [ + 63 + ], + "perpendicular_covariance": "72 I_8 - 9 q q^T", + "root_lines": 120, + "roots_sha256": "f848266f7356ccc0ca5ac421805de254ac2f3100480e732b2a39dec77e9deab0", + "two_set_lower_margins_doubled": { + "perpendicular": 56, + "whole": 104 + }, + "whole_covariance": "120 I_8" + }, + "independent_certificate_sha256": "48e61dcfedcfdf57e87677ec6bde3573626636358adabd473955236791b64a3e", + "semantic_evidence": { + "controls": [ + "missing diagonal admits nonzero Gram error", + "unrestricted factors admit odd singleton error", + "singleton is outside the root column space", + "masked coefficient corruption rejected", + "conjugate transpose changes the identity", + "corrupt root rejected", + "wrong covariance constant rejected" + ], + "odd_singleton": [ + 0, + 1 + ], + "positive_all_pair_entries": 12544, + "positive_one_sided_terms": 9 + }, + "sources": { + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "proof_source_count": 3 + }, + "status": "PASS_ONE_SIDED_MASK_RIGIDITY_S28" +} diff --git a/research/complex-masked-rigidity-seed28/CLAIM.md b/research/complex-masked-rigidity-seed28/CLAIM.md new file mode 100644 index 0000000000..c97eb96cf7 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/CLAIM.md @@ -0,0 +1,23 @@ +# Local sprint claim — seed 28 + +- Track: complex supplier (20–39); OS randomness returned 28. +- Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. +- Started: 2026-10-13 19:38 UTC; expected finish: 20:19 UTC. +- No pinned coordination issue exists (live GraphQL check); the three discussion-board starter threads have no claims. Claim is local under the supplied sprint instructions. +- Three narrow candidates considered: (1) one additional fixed-reader lift on P112 (overlaps #845/#998/#1133); (2) delivery of asymmetric P104 centres (overlaps #1071/#1125); (3) root-linear masked decoders on P112, its 112 one-line punctures, and the 1260 frame-pair P104 punctures. Choose (3). +- Exact question: can replacing the all-pairs identity by the even-inner-product mask improve a decoder whose two factors remain in the rational/complex span of the root-coordinate columns, with any number of terms? +- Method/domain: exact rank of the 64-column tensor-constraint matrix on P112, all 112 P111 deletions, and all 1260 second orthogonal frames in P112; seek small exact certificates and a written linear-algebra proof. Seed 28 determines deterministic row ordering for witness selection. A stronger universal argument may replace repeated elimination if separately justified. +- Optimistic cost screen: first give mask relaxation every possible implementation saving. If the masked and all-pairs feasible products coincide in this class, it has no copied-information headroom even with free mask enforcement. No physical supplier or new kappa will be claimed from this test. +- Expected deliverable: one scoped obstruction or exact escape example; deterministic standard-library checker, positive and semantic negative controls, source pins, proof/scope/credit, and one focused PR. +- Stop after this specified domain and one evidence-driven pivot at most; reserve the last ten minutes for independent review and packaging. +- Nearest predecessors: DreamingOfClouds #717 (B14 model), PR968 frame-pair decoders, @woklerx #1077 complex extension. They exclude masked identities from their stated coverage; this investigation keeps the root-linear factor restriction explicit. Open PR titles and bodies were searched for masked, root-linear and bilinear overlap; no matching task found in the 786-PR snapshot. + +## Evidence-driven refinement + +The covariance argument establishes the stronger one-sided condition on exactly the same live-set domain: one factor is root-linear, while the opposite factor and the term count are unrestricted. The independent implementation therefore checks 143,584 local masked-neighbour spans, which is stronger evidence than the initially proposed 64-column tensor rank alone. The general written lemma also covers deletions contained in at most eight orthogonal sets; no enumeration of that larger domain is claimed. + +## DONE — local result update + +Completed: a one-sided root-linear mask-rigidity theorem for the full claimed domain, plus the stated orthogonal-cover extension. Exact covariance evidence and a separate implementation certify all 1373 domains and 143584 local spans. No new kappa or physical supplier. All relevant local checks and the five selected-record integrity tests pass. + +Result: [proof and reproduction](README.md). Publication artifact: [focused branch package](https://github.com/mightyOil/integer-mult-bounds/tree/research/complex-masked-rigidity-seed28/research/complex-masked-rigidity-seed28). The submission handoff records the eventual PR URL. The final overlap check includes the complementary PR1180; its cost theorem is not imported. diff --git a/research/complex-masked-rigidity-seed28/NOTICE.md b/research/complex-masked-rigidity-seed28/NOTICE.md new file mode 100644 index 0000000000..8a14560900 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/NOTICE.md @@ -0,0 +1,15 @@ +# Attribution and license + +New material: copyright 2026 Philipp (`@mightyOil`), under Apache-2.0, +the repository license. Substantial assistance from OpenAI Codex covered +the mathematical investigation, proof, code, documentation and review. +Independent implementations and peer review were performed by separate +AI agents, not independent human reviewers. + +Predecessor credit and exact source pins are retained in README.md, +OVERLAP.md and SOURCES.json. In particular, the E8 decoder/copy model is +from DreamingOfClouds (#717/#595); the exact frame-pair census and +eight-term all-pairs floor are from themilkman216 (#968); the complex +extension is from woklerx (#1077). Joel Pulikkan / GamingPuzzled (#620) +and icekylinx's P112 work are retained predecessors. No predecessor code +or data archive is overwritten or relabeled as this contribution. diff --git a/research/complex-masked-rigidity-seed28/OVERLAP.md b/research/complex-masked-rigidity-seed28/OVERLAP.md new file mode 100644 index 0000000000..1c0d9075a4 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/OVERLAP.md @@ -0,0 +1,74 @@ +# Scoped overlap and model audit + +Reviewed at base `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` by a separate +Codex research agent. This is an AI-assisted source and scope audit, not +independent human mathematical review. + +## Evidence inspected + +- The coordinator's 786-open-PR title/body snapshot, SHA-256 + `9315dea89e7fe7c2339ea1a9c213aa22de01603bcc0d7fc0748fbc7f166e2d9f`. + Searches covered `masked`, `root-linear`, `bilinear`, `E-graph`, and + decoder titles; relevant bodies were read. This does not inspect all + code in every open PR and does not establish universal novelty. +- The coordinator's discussion snapshot, SHA-256 + `930b7951464c5934dec7ca32b847f78493a84bdcdecfe8f65b904b73fdf9ddc7`, + contains the three starter discussions #1163/#1166/#1167 and no comments. +- Local PR968 and PR1077 proof, README, source records and relevant notices; + the PR717 open body; the relevant PR620 decoder research files; and + incorporated-head entries in the central ledger/disposition records. + +## Closest predecessors and precise difference + +| Predecessor | Pinned head | Relation | +|---|---|---| +| DreamingOfClouds, [PR717](https://github.com/CrocSwap/integer-mult-bounds/pull/717) | `4a97676294f9fa413b65986e9984fddeda71e4cc` | B14 label-pairing/decoder model, P112 floor research and P111/P104 examples. Its mixed-beta overcomplete problem is not closed by this package. | +| themilkman216, [PR968](https://github.com/CrocSwap/integer-mult-bounds/pull/968) | `6a99e7240b961ac5e115ae6aa0301ec7c4a45d77` | Exact **all-pairs**, eight-term real decoder floor and complete 1260-frame / 7168-decoder census. Its proof explicitly excludes E-graph-only exactness and nine or more terms. The new claim compares masked and all-pairs feasible products within an explicitly root-linear class. | +| woklerx, [PR1077](https://github.com/CrocSwap/integer-mult-bounds/pull/1077) | `1459f58a829e616ddf32a3da2782e166700e3218` | Arbitrary-complex extension of the eight-term all-pairs floor; explicitly excludes masked and overcomplete decoders. The new restriction is root-linearity of at least one factor, with the opposite factor unrestricted and arbitrary term count. | +| Josie Elliston, [PR1071](https://github.com/CrocSwap/integer-mult-bounds/pull/1071) | `ce9531beba1ce115fdcdc44925ded995a29b8bac` | Physical delivery lower bounds for specified frame-pair centers; does not decide the masked identity. | +| Ali Romman, [PR1125](https://github.com/CrocSwap/integer-mult-bounds/pull/1125) | `9f7c0679d64bab954b7161d8586dc626a59b92ee` | Asynchronous delivery bound across the 7168 mixed P104 decoders, with physical path restrictions; distinct from an identity constraint. | +| 3xcalibur-tech, [PR1171](https://github.com/CrocSwap/integer-mult-bounds/pull/1171) | `ab74c73b5b512f459b9be97680f41390d45a3bf3` | All-puncture root-only **star label-decoder** ratio exclusion and p=56 classification; a different decoder/cost model. | + +The incorporated PR968 and PR1077 heads above come respectively from +`research/community-batch970-audit/DISPOSITIONS.json` and +`research/community-batch1099-audit/DISPOSITIONS.json`. The open heads come +from the coordinator's snapshot. Attribution also retains Joel Pulikkan / +GamingPuzzled PR620, icekylinx's P112 construction, and DreamingOfClouds PR595 +as recorded in PR968/PR1077. + +No matching masked, root-linear feasible-product rigidity result was found +among the inspected evidence. This is a bounded overlap finding. + +## Model checks that materially affect the claim + +1. The label pairing is `N_ij=(+1) mod 2`. Thus the constrained + entries are the **even** inner products, including diagonals. The odd + inner-product entries have label pairing zero and are the potential + cost-zero correction locations discussed by the predecessors. +2. Diagonals are essential: if only distinct orthogonal pairs were + constrained, `M=I` would be a nonzero invisible bilinear form. A checker + must include `(i,i)`, where `N_ii=1` and `(2G)_ii=4` for norm-two roots. +3. Use ordinary transpose over the complex numbers. Hermitian transpose + is a different decoder model. +4. For arbitrary term count, at least one of `D=RA` or `T=RB` is an explicit restriction. + Masked exactness does not establish it. Even an all-pairs product with + more than eight terms can contain cancelling factors outside `col(R)`. + The covariance proof strengthens the initial both-factor claim to this + one-sided statement; the independent oracle checks its stronger local span condition. +5. Equality of the masked and all-pairs feasible products closes only the + mask relaxation within this class. It does not prove the eight-term cost + floor for nine or more terms, exclude unrestricted masked decoders, or + construct/admit a physical supplier. + +Recommended semantic controls are diagonal deletion (the identity matrix +survives) and an unrestricted label-orthogonal singleton correction outside +the root-linear class. These distinguish the claimed result from the two +most tempting overstatements. + +## Pre-submission refresh + +On 2026-10-13, immediately before submission, refreshed metadata contained 798 open PRs; main remained at the recorded base. The discussion board had one unrelated PR279 provenance claim. No matching masked-neighbour rigidity claim was found. + +A new, complementary contribution is woklerx [PR1180](https://github.com/CrocSwap/integer-mult-bounds/pull/1180), head `75b408646d558147a4eb250fc407d1fbfcb8df4e`. Its proof and README were inspected: it extends the all-pairs copy floor to arbitrary term count when **both** factors stay in the root code, and explicitly excludes graph-only masked identities. Our contribution instead equates masked and all-pairs feasibility when **one** factor stays in the root code, using covariance and local spans. The results are distinct. We do not import, certify, or rely on PR1180's new cost theorem. The cancellation fixture used here has a transposed analogue in PR1180; it is a scope control, not a claimed new cancellation mechanism. + +Refresh snapshot SHA-256: `bbe11beaa4062fb6faa2137ae1c7418d8d24e04b433a5cc06f450134c9a83a1c`. diff --git a/research/complex-masked-rigidity-seed28/PROOF.md b/research/complex-masked-rigidity-seed28/PROOF.md new file mode 100644 index 0000000000..d4b6942f70 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/PROOF.md @@ -0,0 +1,184 @@ +# The even-pair mask is rigid with one root-linear factor + +The conclusion requires at least one factor to lie in the root-coordinate +column space. It does **not** assume that an arbitrary masked decoder has +that property. + +## 1. Statement and concrete domain + +Let \(\mathcal L\) be the 120 E8 root lines, with one representative \(r_i\) +of squared norm 2 on each line. In standard coordinates these are the lines of + +\[ + \{\pm e_a\pm e_b:a0\quad(x\ne0). \tag{5} +\] + +Thus the live roots perpendicular to \(r\) span the full seven-dimensional +space \(r^\perp\). Moreover, (1) and (4) give + +\[ + \sum_{i\notin P}(r_i^Tx)^2\ge(30-2k)\|x\|^2>0\quad(x\ne0), \tag{6} +\] + +so the live roots span \(\mathbb R^8\). For our concrete domain, \(k=1\) for +P112 and \(k=2\) for P111 and P104; a singleton is an orthogonal set. The +respective perpendicular-space lower bounds are 16 and 14, and the +whole-space lower bounds are 28 and 26. + +This proves a modest geometric extension as well: the theorem holds whenever +the deleted lines are covered by at most eight orthogonal sets. No census of +those larger deletion domains is claimed. + +## 4. From the mask to the full product + +First assume \(D=RA\) for some \(A\in\mathbb C^{8\times m}\), leaving +\(T\) arbitrary. Let \(t_j\in\mathbb C^m\) be the transpose of row \(j\) +of \(T\), and define + +\[ + c_j=A t_j-2r_j. +\] + +Column \(j\) of the product error \(DT^T-2RR^T\) equals \(Rc_j\). +The masked equations say that \(r_i^Tc_j=0\) for every live \(r_i\perp r_j\) +and for \(i=j\). The perpendicular live roots span \(r_j^\perp\) by (5), +and adjoining \(r_j\) spans \(\mathbb R^8\). This real spanning statement +also holds after complexification. Therefore \(c_j=0\), for every \(j\), +and the entire product error vanishes. If instead \(T\) is root-linear, +transpose the error and apply the same argument; the mask is symmetric. + +If both factors are root-linear, the result gives +\(R(AB^T-2I_8)R^T=0\). Since \(R\) has rank eight by (6), multiplication +by a left inverse of \(R\) and its transpose gives \(AB^T=2I_8\). +The converse is immediate. + +Equivalently, every live vertex has masked neighbours whose root-coordinate +rows span eight dimensions. This local spanning condition proves the +one-sided assertion; it is stronger information than a 64-column tensor-rank +calculation alone supplies. The both-factor corollary also implies that the +ordered even-pair tensors \(r_i\otimes r_j\) span all 64 dimensions. + +The diagonal equations are essential. If only orthogonal off-diagonal pairs +were imposed, the zero product would satisfy those zero target entries but +fail every target diagonal. Likewise, the homogeneous tensor equations on +orthogonal pairs alone annihilate \(K=I_8\). + +## 5. Scope and the omitted hypothesis + +This is a statement about factors with at least one root-linear side, of any +finite term count. It +does not establish a copy-cost minimum for nine or more terms, a realizable +physical supplier, a new exponent, or a result for arbitrary masked factors. +Existing all-pairs results can only be transferred with their other +hypotheses intact. In particular, an existing eight-term result does not +become an arbitrary-term result through this theorem. + +Requiring a root-linear side is essential. Choose a live odd pair \((i,j)\) +and form \(M=2RR^T+E_{ij}\), where \(E_{ij}\) is the corresponding matrix unit. +Then \(M\) satisfies every masked equation but differs on that odd pair. +Writing \(v=|L|\), the unrestricted factors \(D=I_v\) and \(T=M^T\) satisfy +\(DT^T=M\). Such factors are outside the theorem: neither side satisfies (H). In +particular, \(I_v\) cannot have its columns in the eight-dimensional +root-coordinate column space when \(v>8\); if the other side satisfied +(H), the theorem would contradict the nonzero product error. The checker +includes this semantic negative control. diff --git a/research/complex-masked-rigidity-seed28/README.md b/research/complex-masked-rigidity-seed28/README.md new file mode 100644 index 0000000000..55d6b96bb1 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/README.md @@ -0,0 +1,111 @@ +# One root-linear factor makes the E8 mask rigid + +**Research note / scoped negative result. No new supplier or kappa.** + +On P112, all 112 additional single-line punctures P111, and all 1260 +frame-pair P104 sets, requiring a complex decoder to be exact only on the +even-inner-product entries already forces exactness on **every** entry, +provided at least one factor is root-linear. The opposite factor is +unrestricted, and the number of terms can be arbitrary. + +Precisely, let `R` contain the live norm-two E8 root representatives. If +`D = R A` **or** `T = R B`, and `D T^transpose = 2 R R^transpose` on the +orthogonal pairs and diagonals, then the same equality holds on all pairs. +Transpose is ordinary complex transpose. The proof also applies whenever +the deleted root lines can be covered by at most eight orthogonal sets; +only the stated 1373 live sets are enumerated. + +## What this adds and what it costs + +PR968 and PR1077 explicitly leave masked identities outside their +eight-term all-pairs theorems. This result rules out a particular route +through that opening: changing only the required entries while keeping +one root-linear factor. It uses elementary covariance identities and a +local spanning argument, without the predecessors' hyperplane-flat +classification premise. See [PROOF.md](PROOF.md). + +For each fixed term count, the masked and all-pairs feasible factor pairs +in this class are identical. Therefore their minima under the same +support-pair copy-cost function are identical too. Even an optimistic +budget with free mask enforcement cannot save copied information **from +this relaxation alone**. This is the stopping criterion; there is no new +helper word to price or adopt. It does not exclude better scheduling or +better all-pairs factorizations. + +For exactly eight terms, the inherited PR1077 floor consequently applies: +64 on P112, 63 on these P111 sets, and at least 56 on these P104 sets. +This is a transfer of the predecessors' scoped floor, not a new numerical +bound. No such eight-term floor is asserted for nine or more terms. +Concurrent [PR1180](https://github.com/CrocSwap/integer-mult-bounds/pull/1180) +by woklerx addresses arbitrary-term **all-pairs cost** with both factors +root-linear; it explicitly leaves masked identities open. Its new floor is +not a dependency of this package. The similar cancellation fixture is +credited as a shared scope control, not a new decoder mechanism. +To escape this mask rigidity on these live sets, **both** factors must +leave the root-coordinate column space. That is a necessary condition, +not a construction or a guarantee of a favorable completed budget. + +## Reproduce + +From the repository root, Python 3.10+ and the standard library: + +```sh +python3 -I -B research/complex-masked-rigidity-seed28/verify.py +``` + +Expected final line, exit status zero: + +```text +PASS_ONE_SIDED_MASK_RIGIDITY_S28 sets=1373 local_spans=143584 controls=7 +``` + +The command checks pinned proof/model sources, all 7744 covariance +entries, the semantic controls, and the independently implemented local +span certificate. It compares both deterministic receipts to their +committed JSON. `verify.py --write` regenerates only `CERTIFICATE.json`; +the independent oracle has its own regeneration command. + +The two methods have different proof dependencies: + +- `verify.py` checks integer covariance identities. The written Bessel + inequality argument turns them into uniform spanning statements. +- `tensor_oracle.py` independently enumerates the roots and frames and + supplies exact local basis witnesses for every one of the 143,584 + `(live set, target)` pairs. It does not rely on the covariance identity. + +A nine-term positive fixture has a root-linear first factor and genuinely +non-root-linear cancelling columns in the second factor. Controls also +exhibit the failures caused by deleting diagonals or dropping both +root-linearity assumptions, detect a coefficient error and corrupted +geometry, and distinguish ordinary from conjugate transpose. These are +exact finite checks, not a formal proof of the full multiplication theorem. + +## Scope, sources and attribution + +The base is `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`, assignment seed +**28**, complex-supplier track. [CLAIM.md](CLAIM.md) records the three +candidates, bounded domain and refinement; [OVERLAP.md](OVERLAP.md) +records the inspected competing work; [SOURCES.json](SOURCES.json) +records exact predecessor heads, source hashes and selected context. + +The selected result at that base is PR1094's conditional +`kappa = 836330098538459/500000000000000000`. It is orientation context, +not a result of this experiment. This package changes neither the +selected record nor any existing supplier, archive or `upstream/` file. +No native construction, hosting, source access, restoration, precision, +all-size compiler, analytic transfer or complete selected-frontier replay +is claimed or newly discharged. + +Credit DreamingOfClouds (#717 and #595) for the decoder/copy model, +themilkman216 (#968) for the frame-pair construction/census and all-pairs +floor, woklerx (#1077) for its complex extension, Joel Pulikkan / +GamingPuzzled (#620) for prior decoder-floor work, and icekylinx for P112. +The selected packing context credits Rohan Arun (#1094), Jeremy Kothe, +Hao Yan and the retained supplier lineage. This scoped result does not +claim their constructions or cost floors as new. + +Prepared for Philipp / `@mightyOil` with substantial OpenAI Codex +assistance in the research, proof, implementation and review. Separate +AI agents supplied the independent oracle and adversarial review; no +independent human review or proof-assistant verification is claimed. +New material is Apache-2.0; see [NOTICE.md](NOTICE.md). diff --git a/research/complex-masked-rigidity-seed28/SOURCES.json b/research/complex-masked-rigidity-seed28/SOURCES.json new file mode 100644 index 0000000000..ada50171c0 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/SOURCES.json @@ -0,0 +1,24 @@ +{ + "assignment_seed": 28, + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "predecessor_heads": { + "1077": "1459f58a829e616ddf32a3da2782e166700e3218", + "717": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "968": "6a99e7240b961ac5e115ae6aa0301ec7c4a45d77" + }, + "proof_sources": { + "research/complex-decoder-field-extension-seed44/PROOF.md": "a89530576d8a5e1ae8778d601b37140d954212cd46e06b87a3f565294ee251a2", + "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74", + "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395" + }, + "selected_context_at_base": { + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "kappa": "836330098538459/500000000000000000", + "note": "Orientation context only; this package does not modify, reprice or reverify the selected supplier. The moving selected-result.json path is not a runtime dependency.", + "reproduce": "make frontier1094-verify", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json" + }, + "source_use": "Proof/model references only. Both executable implementations are new and do not import predecessor modules." +} diff --git a/research/complex-masked-rigidity-seed28/TENSOR-CERTIFICATE.json b/research/complex-masked-rigidity-seed28/TENSOR-CERTIFICATE.json new file mode 100644 index 0000000000..7b7cde4b0c --- /dev/null +++ b/research/complex-masked-rigidity-seed28/TENSOR-CERTIFICATE.json @@ -0,0 +1,1882 @@ +{ + "assignment_count": 143584, + "assignment_encoding": "one compact ASCII JSON [domain_name,target_root_id,witness_index] per line, LF terminated; domain order P112, increasing P111 deleted root, lexicographic P104 deleted frame; increasing live target", + "assignments_sha256": "96cfcf6f2c95a7b5a1f3c43aef96cd82a3ef50e5bc9082957da3f6187f19f6f9", + "controls": { + "diagonal_free_frame_neighborhood_rank": 7, + "diagonal_free_kernel_checked_ordered_pairs": 6608, + "duplicate_basis_row_determinant_mod_3": 0, + "duplicate_basis_row_rank": 7, + "omitted_diagonal_residual": 8, + "omitted_reverse_pair_residual": 64, + "ordered_frame_tensor_determinant_mod_3": 1, + "ordered_frame_tensor_rank": 64, + "positive_neighborhood_rank": 8, + "upper_triangle_only_frame_tensor_rank": 36 + }, + "domain_counts": { + "P104": 1260, + "P111": 112, + "P112": 1 + }, + "domains_sha256": "b0ed6f369ec4050daed2efe6545d38a123c0d64fed1198a2013cf2394053abe6", + "doubled_roots_sha256": "499909f15616b21ed34b704054685a0c90c244fb81819ba458e076b8dd97308c", + "fixed_deleted_frame": [ + 0, + 1, + 6, + 11, + 20, + 29, + 106, + 119 + ], + "live_target_counts": { + "P104": 131040, + "P111": 12432, + "P112": 112 + }, + "mask_convention": "dot(q_i,q_j) divisible by 8; diagonal included", + "method": "independent orthogonality-clique enumeration and exact modular minors", + "prime": 3, + "root_convention": "lexicographic doubled E8 roots; first nonzero coordinate positive", + "root_count": 120, + "schema": 2, + "scope": "Exact allowed-neighborhood rank 8 at every live target in P112, all 112 P111 deletions, and all 1260 fixed-frame-pair P104 deletions; no supplier or kappa claim", + "second_frames_sha256": "9f4794b9b10349aa5e4e095547b75fd08c4e895c08980db020c79c525a9a3924", + "seed": 28, + "witness_use_counts": [ + 6912, + 6912, + 6351, + 6912, + 4312, + 4477, + 4939, + 5147, + 5788, + 6350, + 5265, + 5160, + 3216, + 5778, + 2609, + 1864, + 4458, + 3798, + 4045, + 3099, + 2546, + 3097, + 3566, + 2990, + 2817, + 2110, + 1359, + 1987, + 2318, + 965, + 1320, + 1165, + 1045, + 1542, + 539, + 1304, + 1044, + 643, + 961, + 588, + 1354, + 544, + 808, + 1275, + 671, + 500, + 501, + 199, + 498, + 477, + 134, + 289, + 285, + 321, + 227, + 425, + 372, + 255, + 214, + 155, + 232, + 121, + 259, + 117, + 195, + 14, + 72, + 51, + 44, + 124, + 71, + 58, + 37, + 44, + 82, + 75, + 33, + 129, + 112, + 90, + 85, + 54, + 100, + 17, + 53, + 24, + 65, + 15, + 29, + 4, + 15, + 22, + 46, + 6, + 9, + 18, + 12, + 43, + 16, + 20, + 5, + 45, + 11, + 11, + 8, + 19, + 2, + 14, + 7, + 6, + 11, + 7, + 6, + 3, + 2, + 3, + 1, + 2, + 2, + 1, + 1, + 2 + ], + "witnesses": [ + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 2, + 21, + 31, + 45, + 62, + 82, + 105, + 112 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 3, + 23, + 39, + 48, + 63, + 74, + 93, + 117 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 4, + 21, + 37, + 51, + 73, + 84, + 102, + 108 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 5, + 16, + 32, + 59, + 68, + 96, + 103, + 107 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 4, + 7, + 41, + 66, + 73, + 84, + 87, + 108 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 8, + 27, + 31, + 48, + 58, + 84, + 102, + 114 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 9, + 23, + 31, + 42, + 63, + 86, + 99, + 115 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 10, + 16, + 30, + 45, + 56, + 96, + 101, + 110 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 12, + 25, + 37, + 57, + 61, + 76, + 104, + 110 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 13, + 24, + 32, + 43, + 69, + 89, + 95, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 8, + 9, + 14, + 17, + 33, + 38, + 107, + 118 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 15, + 27, + 34, + 52, + 58, + 77, + 99, + 116 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 8, + 18, + 37, + 61, + 71, + 96, + 98, + 107 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 19, + 26, + 36, + 47, + 66, + 83, + 94, + 115 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 16, + 22, + 37, + 47, + 73, + 86, + 96, + 109 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 28, + 31, + 47, + 61, + 89, + 99, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 17, + 27, + 35, + 49, + 70, + 88, + 95, + 109 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 3, + 10, + 40, + 67, + 72, + 93, + 94, + 107 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 44, + 54, + 59, + 73, + 79, + 85, + 96, + 98 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 46, + 57, + 59, + 68, + 76, + 83, + 97, + 102 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 48, + 50, + 59, + 73, + 77, + 87, + 94, + 100 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 13, + 26, + 32, + 53, + 58, + 79, + 104, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 52, + 55, + 59, + 64, + 74, + 81, + 101, + 102 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 49, + 54, + 60, + 67, + 75, + 84, + 94, + 105 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 42, + 56, + 65, + 67, + 79, + 85, + 92, + 102 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 23, + 40, + 56, + 71, + 78, + 97, + 109 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 23, + 32, + 42, + 61, + 80, + 95, + 117 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 14, + 27, + 39, + 48, + 71, + 85, + 90, + 112 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 17, + 25, + 38, + 45, + 68, + 82, + 91, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 8, + 26, + 31, + 43, + 62, + 87, + 98, + 115 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 8, + 26, + 40, + 53, + 72, + 81, + 92, + 110 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 10, + 22, + 40, + 51, + 72, + 78, + 93, + 112 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 7, + 16, + 30, + 42, + 55, + 95, + 98, + 115 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 15, + 28, + 34, + 46, + 66, + 87, + 91, + 115 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 8, + 9, + 14, + 17, + 30, + 41, + 110, + 115 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 42, + 53, + 65, + 70, + 80, + 87, + 91, + 100 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 5, + 25, + 32, + 51, + 68, + 88, + 103, + 108 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 51, + 56, + 58, + 65, + 77, + 78, + 100, + 103 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 18, + 24, + 39, + 49, + 71, + 83, + 93, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 15, + 16, + 23, + 26, + 33, + 38, + 109, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 12, + 30, + 44, + 54, + 90, + 104, + 114 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 12, + 34, + 42, + 56, + 77, + 87, + 118 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 43, + 54, + 64, + 69, + 76, + 89, + 95, + 98 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 19, + 23, + 33, + 50, + 63, + 80, + 101, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 14, + 22, + 35, + 55, + 64, + 78, + 105, + 109 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 12, + 27, + 36, + 57, + 59, + 77, + 103, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 2, + 16, + 30, + 45, + 50, + 90, + 101, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 17, + 27, + 39, + 56, + 63, + 77, + 98, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 10, + 25, + 38, + 48, + 61, + 75, + 94, + 117 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 4, + 19, + 41, + 62, + 68, + 80, + 82, + 114 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 5, + 16, + 30, + 47, + 56, + 96, + 103, + 109 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 13, + 25, + 39, + 57, + 63, + 75, + 101, + 111 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 42, + 49, + 67, + 72, + 85, + 86, + 92, + 95 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 19, + 24, + 37, + 49, + 69, + 84, + 96, + 110 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 2, + 8, + 40, + 50, + 57, + 77, + 78, + 118 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 43, + 56, + 60, + 71, + 81, + 82, + 94, + 101 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 12, + 27, + 35, + 44, + 70, + 88, + 90, + 114 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 10, + 18, + 41, + 64, + 67, + 77, + 86, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 3, + 23, + 40, + 50, + 69, + 76, + 91, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 49, + 51, + 60, + 70, + 78, + 84, + 91, + 105 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 5, + 19, + 36, + 48, + 51, + 79, + 84, + 118 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 3, + 4, + 7, + 10, + 31, + 40, + 107, + 118 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 17, + 21, + 38, + 52, + 65, + 75, + 102, + 112 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 49, + 52, + 62, + 67, + 75, + 86, + 92, + 105 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 14, + 22, + 36, + 51, + 60, + 74, + 101, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 16, + 27, + 39, + 48, + 70, + 84, + 90, + 114 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 49, + 54, + 60, + 67, + 74, + 85, + 95, + 104 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 10, + 25, + 31, + 45, + 64, + 88, + 101, + 110 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 13, + 25, + 37, + 47, + 73, + 88, + 94, + 109 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 8, + 22, + 34, + 54, + 68, + 83, + 105, + 108 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 47, + 53, + 64, + 66, + 76, + 86, + 91, + 105 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 10, + 15, + 30, + 43, + 54, + 94, + 99, + 115 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 13, + 23, + 35, + 56, + 63, + 78, + 105, + 109 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 5, + 21, + 31, + 43, + 64, + 84, + 103, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 44, + 54, + 59, + 73, + 81, + 83, + 94, + 100 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 9, + 23, + 38, + 56, + 69, + 82, + 103, + 108 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 21, + 37, + 53, + 71, + 82, + 104, + 108 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 19, + 25, + 33, + 47, + 67, + 85, + 97, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 3, + 14, + 30, + 46, + 57, + 96, + 103, + 109 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 4, + 28, + 40, + 54, + 68, + 80, + 90, + 114 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 44, + 55, + 65, + 66, + 75, + 88, + 94, + 101 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 46, + 53, + 59, + 72, + 81, + 82, + 92, + 103 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 10, + 24, + 33, + 46, + 59, + 77, + 96, + 117 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 19, + 24, + 34, + 46, + 66, + 83, + 95, + 115 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 5, + 24, + 39, + 55, + 72, + 84, + 99, + 108 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 5, + 15, + 30, + 43, + 52, + 92, + 99, + 116 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 7, + 10, + 22, + 27, + 35, + 36, + 108, + 117 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 12, + 24, + 38, + 56, + 60, + 74, + 102, + 114 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 17, + 22, + 35, + 50, + 61, + 75, + 100, + 116 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 13, + 23, + 36, + 42, + 69, + 84, + 91, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 45, + 54, + 64, + 67, + 79, + 84, + 90, + 105 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 46, + 53, + 60, + 71, + 75, + 88, + 97, + 98 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 12, + 26, + 33, + 43, + 70, + 89, + 92, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 3, + 26, + 31, + 43, + 60, + 85, + 98, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 5, + 24, + 32, + 44, + 59, + 79, + 96, + 117 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 14, + 28, + 35, + 46, + 67, + 87, + 90, + 115 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 10, + 16, + 30, + 48, + 53, + 93, + 104, + 110 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 2, + 25, + 39, + 54, + 73, + 85, + 98, + 108 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 19, + 27, + 37, + 53, + 63, + 80, + 98, + 113 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 12, + 27, + 36, + 45, + 71, + 89, + 91, + 111 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 17, + 24, + 33, + 43, + 66, + 84, + 93, + 116 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 9, + 18, + 30, + 45, + 55, + 97, + 99, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 47, + 50, + 61, + 72, + 76, + 89, + 94, + 99 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 2, + 16, + 39, + 65, + 70, + 90, + 101, + 107 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 15, + 22, + 32, + 43, + 69, + 87, + 97, + 111 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 17, + 28, + 33, + 47, + 66, + 88, + 93, + 112 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 49, + 52, + 59, + 70, + 74, + 87, + 96, + 101 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 7, + 27, + 35, + 44, + 63, + 81, + 90, + 117 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 49, + 50, + 62, + 69, + 76, + 87, + 91, + 104 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 51, + 56, + 61, + 62, + 74, + 81, + 100, + 103 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 15, + 28, + 33, + 54, + 58, + 80, + 100, + 114 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 7, + 16, + 41, + 65, + 68, + 76, + 89, + 110 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 2, + 21, + 40, + 53, + 70, + 74, + 97, + 113 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 18, + 23, + 32, + 44, + 67, + 86, + 97, + 113 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 44, + 51, + 63, + 72, + 78, + 89, + 93, + 98 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 18, + 28, + 37, + 55, + 61, + 80, + 98, + 113 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 3, + 21, + 31, + 43, + 65, + 85, + 103, + 111 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 9, + 23, + 40, + 56, + 69, + 76, + 97, + 110 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 52, + 55, + 58, + 65, + 77, + 78, + 99, + 104 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 15, + 22, + 34, + 46, + 72, + 87, + 97, + 109 + ] + }, + { + "determinant_mod_3": 2, + "rank_mod_3": 8, + "root_ids": [ + 42, + 53, + 64, + 71, + 81, + 86, + 91, + 100 + ] + }, + { + "determinant_mod_3": 1, + "rank_mod_3": 8, + "root_ids": [ + 3, + 4, + 12, + 19, + 34, + 37, + 107, + 118 + ] + } + ] +} diff --git a/research/complex-masked-rigidity-seed28/VALIDATION.md b/research/complex-masked-rigidity-seed28/VALIDATION.md new file mode 100644 index 0000000000..a2e2b1829c --- /dev/null +++ b/research/complex-masked-rigidity-seed28/VALIDATION.md @@ -0,0 +1,47 @@ +# Local validation receipt + +Date: 2026-10-13. Environment: macOS 27.0.1 arm64, CPython 3.14.7. +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. + +Completed: + +```sh +python3 -I -B research/complex-masked-rigidity-seed28/verify.py +python3 -I -O -B research/complex-masked-rigidity-seed28/verify.py +python3 -I -O -B research/complex-masked-rigidity-seed28/tensor_oracle.py +python3 -B -m unittest discover -s tests -p test_selected_result.py +git diff --check +``` + +Both checker modes pass with identical deterministic receipts. The main +command checks 7744 covariance entries, a 12544-entry nine-term positive +identity, seven semantic controls, and the independent certificate. The +oracle enumerates all 1260 second frames and all 1373 domains and checks +143584 local spans using 122 nonsingular integer minors. Its three further +controls cover diagonal deletion, ordered-pair orientation and a duplicate +basis row. Nonzero determinant modulo 3 certifies nonzero integer +determinant; no probabilistic rank inference is used. + +An additional subprocess test replaced one row of the first saved witness +with a duplicate and invoked `tensor_oracle.py --check` under `-I -O -B`. +It exited nonzero at `saved certificate differs from exact regeneration`. +Verification uses explicit exceptions and remains enabled under `-O`. + +The unchanged selected-record integrity suite passes all five tests. +This is a metadata/source integrity check, not the selected construction's +cold replay. Only the new scoped directory is added. + +One measured main replay took 0.43 seconds wall time (0.40 user, 0.01 +system), including the independent oracle. This is a single local runtime +observation, not a comparative performance claim. + +A separate AI agent reviewed the written proof and main checker and found +no actionable mathematical defect. Another review independently rebuilt +the roots, checked every witness's coverage and evaluated all 122 integer +determinants with Bareiss elimination: every absolute determinant was +4096 and its residue agreed with the oracle. These reviews are not +independent human review or proof-assistant verification. + +Not run or claimed: full selected-frontier cold replay, unrelated historical +suites, native supplier admission, hosted Linux CI, or an all-size integer +multiplication proof. No changed supplier is proposed. diff --git a/research/complex-masked-rigidity-seed28/tensor_oracle.py b/research/complex-masked-rigidity-seed28/tensor_oracle.py new file mode 100644 index 0000000000..e4c10dc624 --- /dev/null +++ b/research/complex-masked-rigidity-seed28/tensor_oracle.py @@ -0,0 +1,301 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent exact neighborhood-rank oracle for the specified E8 punctures. + +Python >= 3.10, standard library only; no imports from the main checker. +Representatives q are twice the usual norm-squared-two E8 roots. They are +lexicographically sorted after identifying q and -q by first-nonzero-positive. +The mask is q_i.q_j == 0 (mod 8), INCLUDING i == j. + +For every target j in every live domain, an eight-row minor of its allowed +neighbors is certified nonsingular modulo the fixed prime 3. Its INTEGER +determinant therefore cannot vanish: the rank is exactly eight over Q and C. +This is an exact certificate, not a randomized finite-field rank estimate. +Seed 28 only fixes deterministic SHA-256 tie-breaking between root frames. + +All 143584 domain/target assignments are recomputed and checked. The artifact +stores the 122 reused minors and a canonical digest of assignments, rather +than 143584 repetitive records. run() builds and validates the complete data. +Without options the CLI also compares it to TENSOR-CERTIFICATE.json. Use +--write PATH to write JSON, or --check PATH to compare a different artifact. +""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +PRIME = 3 +SEED = 28 +DIM = 8 +HERE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def dot(left, right): + return sum(a * b for a, b in zip(left, right)) + + +def canonical(value): + return json.dumps(value, separators=(",", ":"), ensure_ascii=True).encode("ascii") + + +def digest(value): + return hashlib.sha256(canonical(value)).hexdigest() + + +def doubled_root_lines(): + """Build the 56 D8 and 64 half-integral lines, without a source data file.""" + lines = set() + for a, b in itertools.combinations(range(DIM), 2): + for sign in (-1, 1): + root = [0] * DIM + root[a], root[b] = 2, 2 * sign + lines.add(tuple(root)) + for tail in itertools.product((-1, 1), repeat=DIM - 1): + root = (1,) + tail + if sum(value < 0 for value in root) % 2 == 0: + lines.add(root) + roots = sorted(lines) + require(len(roots) == 120, "root-line count") + require(all(dot(q, q) == 8 for q in roots), "root lengths") + require(all(dot(q, r) in (-4, 0, 4) + for i, q in enumerate(roots) for r in roots[i + 1:]), + "off-diagonal true-root inner products") + return roots + + +def fixed_frame(roots): + """The eight lines 2(e_0 +/- e_1), ..., 2(e_6 +/- e_7).""" + frame = [] + for a in range(0, DIM, 2): + for sign in (-1, 1): + root = [0] * DIM + root[a], root[a + 1] = 2, 2 * sign + frame.append(roots.index(tuple(root))) + return tuple(sorted(frame)) + + +def enumerate_frames(roots, live): + """Exhaust all increasing size-eight cliques of the orthogonality graph.""" + neighbors = {} + for i in live: + neighbors[i] = sum(1 << j for j in live + if j > i and dot(roots[i], roots[j]) == 0) + frames = [] + + def extend(prefix, candidates): + needed = DIM - len(prefix) + if not needed: + frames.append(prefix) + return + while candidates.bit_count() >= needed: + bit = candidates & -candidates + candidates ^= bit + vertex = bit.bit_length() - 1 + extend(prefix + (vertex,), candidates & neighbors[vertex]) + + extend((), sum(1 << i for i in live)) + require(len(frames) == 1260, "second-frame census must contain 1260 frames") + require(frames == sorted(set(frames)), "duplicate or unordered frames") + return frames + + +def geometry(): + roots = doubled_root_lines() + first = fixed_frame(roots) + live = tuple(i for i in range(len(roots)) if i not in first) + frames = enumerate_frames(roots, live) + domains = [("P112", ())] + domains += [(f"P111-{i:03d}", (i,)) for i in live] + domains += [(f"P104-{k:04d}", frame) for k, frame in enumerate(frames)] + require(len(domains) == 1373, "finite domain size") + return roots, first, live, frames, domains + + +def rank_and_determinant(rows, width): + """Ordinary exact Gaussian elimination modulo the fixed prime 3.""" + matrix = [[x % PRIME for x in row] for row in rows] + require(all(len(row) == width for row in matrix), "matrix width") + rank = 0 + determinant = 1 + for column in range(width): + pivot = next((r for r in range(rank, len(matrix)) + if matrix[r][column]), None) + if pivot is None: + continue + if pivot != rank: + matrix[rank], matrix[pivot] = matrix[pivot], matrix[rank] + determinant = -determinant + value = matrix[rank][column] + determinant = determinant * value % PRIME + inverse = pow(value, -1, PRIME) + row = matrix[rank] + for c in range(column, width): + row[c] = row[c] * inverse % PRIME + for r in range(rank + 1, len(matrix)): + value = matrix[r][column] + if value: + other = matrix[r] + for c in range(column, width): + other[c] = (other[c] - value * row[c]) % PRIME + rank += 1 + if rank == len(matrix): + break + determinant = determinant % PRIME if len(matrix) == width and rank == width else 0 + return rank, determinant + + +def controls(roots, live, frame): + """Semantic failures: losing diagonals, orientation, or row independence.""" + rows = [roots[i] for i in frame] + require(rank_and_determinant(rows, DIM)[0] == DIM, "positive control") + + # For every target j, the nonzero coefficient vector q_j annihilates + # EVERY allowed off-diagonal row. This also holds in all live subsets. + all_off_diagonal = [(i, j) for i in live for j in live + if i != j and dot(roots[i], roots[j]) % 8 == 0] + require(all(dot(roots[i], roots[j]) == 0 for i, j in all_off_diagonal), + "q_j must lie in the diagonal-free neighborhood kernel") + no_diagonal_rank = rank_and_determinant(rows[1:], DIM)[0] + require(no_diagonal_rank == 7 and dot(rows[0], rows[0]) == 8, + "diagonal-free rank and detected diagonal residual") + + # Secondary tensor control: ordered constraints matter for arbitrary, + # non-symmetric bilinear coefficients. B=q_b q_a^T, b>a in this frame, + # vanishes on every i<=j frame pair, but has residual 64 at (b,a). + # This is a control on the frame witness, not a rank claim about the + # complete upper-triangle-only mask on all 112 roots. + def tensor(i, j): + return [a * b for a in roots[i] for b in roots[j]] + + a, b = frame[0], frame[1] + upper_pairs = [(i, j) for i in frame for j in frame if i <= j] + upper_rank = rank_and_determinant([tensor(i, j) for i, j in upper_pairs], 64)[0] + ordered_rank, ordered_determinant = rank_and_determinant( + [tensor(i, j) for i in frame for j in frame], 64) + upper_residuals = [dot(roots[i], roots[b]) * dot(roots[a], roots[j]) + for i, j in upper_pairs] + reverse_residual = dot(roots[b], roots[b]) * dot(roots[a], roots[a]) + require(upper_rank == 36 and all(x == 0 for x in upper_residuals) + and reverse_residual == 64 and ordered_rank == 64 + and ordered_determinant != 0, "ordered-pair control") + + corrupt_rank, corrupt_determinant = rank_and_determinant(rows[:-1] + [rows[0]], DIM) + require(corrupt_rank == 7 and corrupt_determinant == 0, + "duplicate-row corruption must be rejected") + return { + "positive_neighborhood_rank": 8, + "diagonal_free_kernel_checked_ordered_pairs": len(all_off_diagonal), + "diagonal_free_frame_neighborhood_rank": no_diagonal_rank, + "omitted_diagonal_residual": 8, + "ordered_frame_tensor_rank": ordered_rank, + "ordered_frame_tensor_determinant_mod_3": ordered_determinant, + "upper_triangle_only_frame_tensor_rank": upper_rank, + "omitted_reverse_pair_residual": reverse_residual, + "duplicate_basis_row_rank": corrupt_rank, + "duplicate_basis_row_determinant_mod_3": corrupt_determinant, + } + + +def run(): + """Reconstruct all geometry and verify every live-target span exactly.""" + roots, first, live, frames, domains = geometry() + ranked = sorted(frames, key=lambda frame: hashlib.sha256( + (str(SEED) + ":" + ",".join(map(str, frame))).encode("ascii")).digest()) + by_target = {i: [frame for frame in ranked if i in frame] for i in live} + require(all(len(by_target[i]) == 90 for i in live), "frames per live root") + allowed = {j: sum(1 << i for i in live if dot(roots[i], roots[j]) % 8 == 0) + for j in live} + bank = [] + bank_bits = [] + available = {i: [] for i in live} + uses = [] + assignment_hash = hashlib.sha256() + target_counts = {"P112": 0, "P111": 0, "P104": 0} + # The census determines every deletion explicitly; no sampled domains. + for name, deleted in domains: + removed = set(deleted) + removed_bits = sum(1 << i for i in deleted) + for target in live: + if target in removed: + continue + chosen = next((k for k in available[target] + if not (bank_bits[k] & removed_bits)), None) + if chosen is None: + survivor = next((frame for frame in by_target[target] + if removed.isdisjoint(frame)), None) + require(survivor is not None, f"no surviving basis for {name}/{target}") + chosen = len(bank) + rank, determinant = rank_and_determinant([roots[i] for i in survivor], DIM) + require(rank == DIM and determinant != 0, "singular neighborhood minor") + bank.append({"root_ids": list(survivor), "rank_mod_3": rank, + "determinant_mod_3": determinant}) + bank_bits.append(sum(1 << i for i in survivor)) + uses.append(0) + for i in survivor: + available[i].append(chosen) + # Each target receives eight actual, live, allowed rows. Rank of + # every reused minor was checked on creation, above. + witness = bank_bits[chosen] + require(witness.bit_count() == DIM, "witness distinctness") + require(witness & (1 << target), "witness must contain its target") + require(not (witness & removed_bits), "witness contains a deleted root") + require(not (witness & ~allowed[target]), "witness uses a forbidden mask pair") + uses[chosen] += 1 + target_counts[name.split("-")[0]] += 1 + assignment_hash.update(canonical([name, target, chosen]) + b"\n") + require(target_counts == {"P112": 112, "P111": 12432, "P104": 131040}, + "incomplete live-target coverage") + require(sum(uses) == 143584 and all(uses), "unused basis or incomplete assignment count") + return { + "schema": 2, + "scope": "Exact allowed-neighborhood rank 8 at every live target in P112, all 112 P111 deletions, and all 1260 fixed-frame-pair P104 deletions; no supplier or kappa claim", + "method": "independent orthogonality-clique enumeration and exact modular minors", + "seed": SEED, + "prime": PRIME, + "root_convention": "lexicographic doubled E8 roots; first nonzero coordinate positive", + "mask_convention": "dot(q_i,q_j) divisible by 8; diagonal included", + "root_count": len(roots), + "doubled_roots_sha256": digest(roots), + "fixed_deleted_frame": list(first), + "second_frames_sha256": digest(frames), + "domain_counts": {"P112": 1, "P111": 112, "P104": 1260}, + "domains_sha256": digest(domains), + "live_target_counts": target_counts, + "assignment_count": sum(uses), + "assignment_encoding": "one compact ASCII JSON [domain_name,target_root_id,witness_index] per line, LF terminated; domain order P112, increasing P111 deleted root, lexicographic P104 deleted frame; increasing live target", + "assignments_sha256": assignment_hash.hexdigest(), + "witnesses": bank, + "witness_use_counts": uses, + "controls": controls(roots, live, bank[0]["root_ids"]), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + action = parser.add_mutually_exclusive_group() + action.add_argument("--write", type=Path, help="write deterministic JSON certificate") + action.add_argument("--check", type=Path, help="compare another saved certificate") + args = parser.parse_args() + generated = run() + if args.write: + args.write.write_text(json.dumps(generated, indent=2, sort_keys=True) + "\n", encoding="utf-8") + else: + path = args.check or HERE / "TENSOR-CERTIFICATE.json" + supplied = json.loads(path.read_text(encoding="utf-8")) + require(supplied == generated, "saved certificate differs from exact regeneration") + print("PASS_TENSOR_ORACLE: 120 root lines; 1260 second frames; " + f"1373 live domains; {generated['assignment_count']} target spans; " + f"{len(generated['witnesses'])} exact 8-row minors; rank_Q=rank_C=8; " + "3 semantic controls; no new kappa") + + +if __name__ == "__main__": + main() diff --git a/research/complex-masked-rigidity-seed28/verify.py b/research/complex-masked-rigidity-seed28/verify.py new file mode 100644 index 0000000000..30c20e0adf --- /dev/null +++ b/research/complex-masked-rigidity-seed28/verify.py @@ -0,0 +1,197 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact covariance evidence and semantic controls for one-sided mask rigidity. + +Python 3.10+, standard library; no floating point or disabled-assertion checks. +The separately written tensor_oracle.py checks every concrete local span. +""" +import argparse +import hashlib +import importlib.util +import itertools +import json +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, indent=2) + "\n" + + +def digest(value): + return hashlib.sha256(canonical(value).encode()).hexdigest() + + +def roots(): + """One first-nonzero-positive representative per line, doubled coordinates.""" + result = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + result.add(tuple(row)) + for tail in itertools.product((-1, 1), repeat=7): + row = (1,) + tail + if sum(x < 0 for x in row) % 2 == 0: + result.add(row) + return sorted(result) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def covariance(rows): + return [[sum(r[a] * r[b] for r in rows) for b in range(8)] + for a in range(8)] + + +def rank_q(rows): + pivots = {} + for row in rows: + v = [Fraction(x) for x in row] + for col, basis in sorted(pivots.items()): + if v[col]: + scalar = v[col] + v = [x - scalar * y for x, y in zip(v, basis)] + pivot = next((i for i, x in enumerate(v) if x), None) + if pivot is not None: + scalar = v[pivot] + pivots[pivot] = [x / scalar for x in v] + return len(pivots) + + +def check_geometry(lines, perpendicular_constant=72): + require(len(lines) == 120 and len(set(lines)) == 120, "120 distinct root lines required") + require(all(len(r) == 8 and dot(r, r) == 8 for r in lines), "wrong root norm") + require(covariance(lines) == [[120 * (a == b) for b in range(8)] for a in range(8)], + "whole-root covariance mismatch") + counts = [] + for r in lines: + perpendicular = [s for s in lines if dot(r, s) == 0] + require(len(perpendicular) == 63, "orthogonal-neighbour count mismatch") + expected = [[perpendicular_constant * (a == b) - 9 * r[a] * r[b] + for b in range(8)] for a in range(8)] + require(covariance(perpendicular) == expected, "perpendicular covariance mismatch") + counts.append(len(perpendicular)) + require(all(dot(r, s) % 4 == 0 for r in lines for s in lines), "nonintegral true Gram") + return {"root_lines": 120, "coordinate_convention": "doubled; first nonzero positive; lexicographic", + "roots_sha256": digest(lines), "whole_covariance": "120 I_8", + "perpendicular_covariance": "72 I_8 - 9 q q^T", "orthogonal_counts": sorted(set(counts)), + "covariance_entries_checked": 64 * 121, + "geometric_cover_limit": 8, + "two_set_lower_margins_doubled": {"perpendicular": 56, "whole": 104}} + + +def reject(action, message): + try: + action() + except ValueError: + return + raise ValueError("control failed to reject: " + message) + + +def semantic_controls(lines): + frame = set() + for i in range(0, 8, 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[i + 1] = 2, 2 * sign + frame.add(tuple(row)) + live = [q for q in lines if q not in frame] + require(len(live) == 112, "P112 size") + pairs = [(i, j) for i, r in enumerate(live) for j, s in enumerate(live)] + mask = lambda i, j: (dot(live[i], live[j]) // 4) % 2 == 0 + gram2 = lambda i, j: Fraction(dot(live[i], live[j]), 2) + require(all(mask(i, i) for i in range(112)), "diagonals must be masked") + + # Omitting diagonals admits X=G, whose remaining even entries vanish. + require(all(dot(live[i], live[j]) == 0 for i, j in pairs if i != j and mask(i, j)), + "off-diagonal control premise") + require(dot(live[0], live[0]) != 0, "diagonal deletion must leave a nonzero error") + + # A singleton error at an odd pair passes the mask but fails full equality. + odd_i, odd_j = next((i, j) for i, j in pairs if not mask(i, j)) + require(all((i, j) != (odd_i, odd_j) for i, j in pairs if mask(i, j)), + "unrestricted singleton must be invisible on the mask") + require(rank_q(live) == 8 and rank_q(live[:odd_i] + live[odd_i + 1:]) == 8, + "singleton's column lies outside the root column space") + # X=2G+E can be realized as D=I, T=X^T; no supplier cost is asserted. + + # Positive nine-term case: D is root-linear, T has cancelling non-root-linear columns. + D = [list(r) + [r[0]] for r in live] + T = [] + for j, r in enumerate(live): + z = int(j == odd_i) + T.append([Fraction(r[k], 2) - (z if k == 0 else 0) for k in range(8)] + [Fraction(z)]) + require(all(sum(x * y for x, y in zip(D[i], T[j])) == gram2(i, j) for i, j in pairs), + "one-sided nine-term positive identity failed") + # The final column of T is e_odd_i, proven outside col(R) by the rank check above. + + # Wrong scaling is detected on the mask, including its diagonals. + wrong = [row[:] for row in T] + wrong[0][0] += 1 + require(any(sum(x * y for x, y in zip(D[i], wrong[j])) != gram2(i, j) + for i, j in pairs if mask(i, j)), "coefficient mutation went undetected") + + # Ordinary transpose is material: i * (-i)=1; i * conjugate(-i)=-1. + # Integer Gaussian pairs avoid floating-point complex arithmetic entirely. + mul = lambda z, w: (z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0]) + require(mul((0, 1), (0, -1)) == (1, 0) and mul((0, 1), (0, 1)) == (-1, 0), + "ordinary-versus-conjugate transpose control") + require(gram2(0, 0) != -gram2(0, 0), "conjugate model must fail on diagonal") + + damaged = lines.copy() + damaged[0] = tuple(x + (i == 0) for i, x in enumerate(damaged[0])) + reject(lambda: check_geometry(damaged), "corrupt root") + reject(lambda: check_geometry(lines, 71), "wrong covariance normalization") + return {"positive_one_sided_terms": 9, "positive_all_pair_entries": len(pairs), + "controls": ["missing diagonal admits nonzero Gram error", + "unrestricted factors admit odd singleton error", + "singleton is outside the root column space", + "masked coefficient corruption rejected", + "conjugate transpose changes the identity", + "corrupt root rejected", "wrong covariance constant rejected"], + "odd_singleton": [odd_i, odd_j]} + + +def check_sources(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for rel, expected in sources["proof_sources"].items(): + require(hashlib.sha256((ROOT / rel).read_bytes()).hexdigest() == expected, + "source pin mismatch: " + rel) + return {"base_commit": sources["base_commit"], "proof_source_count": len(sources["proof_sources"])} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate this package's certificate only") + args = parser.parse_args() + result = {"status": "PASS_ONE_SIDED_MASK_RIGIDITY_S28", "sources": check_sources(), + "geometry": check_geometry(roots()), "semantic_evidence": semantic_controls(roots())} + oracle_path = HERE / "tensor_oracle.py" + spec = importlib.util.spec_from_file_location("independent_mask_oracle", oracle_path) + oracle = importlib.util.module_from_spec(spec) + spec.loader.exec_module(oracle) + independent = oracle.run() + require(independent == json.loads((HERE / "TENSOR-CERTIFICATE.json").read_text()), + "independent certificate mismatch") + result["independent_certificate_sha256"] = digest(independent) + path = HERE / "CERTIFICATE.json" + if args.write: + path.write_text(canonical(result)) + else: + require(result == json.loads(path.read_text()), "certificate mismatch; inspect before regenerating") + print("PASS_ONE_SIDED_MASK_RIGIDITY_S28 sets=1373 local_spans=143584 controls=7") + + +if __name__ == "__main__": + main()