Prove E8 span inputs over every odd-characteristic field (no new κ)

research/e8-odd-characteristic-spans/PROOF.md

@@ -0,0 +1,132 @@
+# E8 span lemmas over every field of odd characteristic
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Let L be the 120 standard norm-two E8 root lines, with representatives in
+Z[1/2]^8. For a line u write O_u for the root lines orthogonal to u. Evaluate
+these representatives in a field K of characteristic different from two.
+The ambient dot product is the ordinary nondegenerate form on K^8.
+
+The following four facts hold over every such field, including characteristic
+zero. There is no exceptional odd prime.
+
+1. **S1.** The roots in O_f span f-perp, of dimension seven.
+2. **S2.** For distinct root lines f,u, the roots in O_f intersect O_u span
+   span(f,u)-perp, of dimension six.
+3. **S3prime.** Suppose u,v are distinct root lines nonorthogonal to f, neither
+   equal to f, and f,u,v are independent over Q. The roots in O_f intersect
+   O_u intersect O_v span span(f,u,v)-perp, of dimension five. The three
+   anchors remain independent over K.
+4. **W2.** Project the 56 lines nonorthogonal to f, other than f itself, onto
+   f-perp by w_u = r_u - (r_u dot r_f) r_f/2. Their projective images are
+   exactly 28 distinct directions. Every three distinct directions are
+   linearly independent over K. Consequently a two-dimensional subspace
+   contains at most two of them.
+
+The S3prime admissibility condition uses the rational root configuration.
+The conclusion proves that its admissible triples remain independent after
+reduction. It does not silently change the domain at a special prime.
+
+These are the span inputs named in DreamingOfClouds's PR2819 and its PR2784
+lineage. PR2819 establishes them in characteristic zero and explicitly leaves
+positive characteristic outside its classification. This proof supplies the
+new field range of those inputs. It does not assert the full rank-nine
+classification in positive characteristic.
+
+## Integer certificates
+
+Use doubled roots R_u = 2 r_u. Their entries are integral, their squared norm
+is eight, and distinct root-line products are 0 or +/-4. All those nonzero
+products remain nonzero over every odd-characteristic field, so the
+orthogonality pattern itself does not change.
+
+For an integer matrix A, a k-by-k minor with determinant +/-2^a certifies
+rank(A) >= k over every field of characteristic different from two. This
+follows because its determinant is a unit in Z[1/2], hence is nonzero in K.
+The same certificate also applies to characteristic zero. No extrapolation
+from finitely many primes is involved.
+
+The verifier fixes f = e_0+e_1. It constructs the entire root inventory
+explicitly and generates one such minor for each of the following matrices.
+
+| Matrix family | Matrices | Certified lower rank |
+| --- | ---: | ---: |
+| R[O_f] | 1 | 7 |
+| Two anchors (f,u) | 119 | 2 |
+| R[O_f intersect O_u] | 119 | 6 |
+| Admissible three anchors (f,u,v) | 1512 | 3 |
+| R[O_f intersect O_u intersect O_v] | 1512 | 5 |
+| Three distinct projected directions | 3276 | 3 |
+
+There are 6539 minors. Their absolute determinants are powers of two between
+2 and 256. `select_minor` uses elimination modulo three only to choose row
+and column indices. `determinant` then evaluates the selected original
+integer square matrix by fraction-free elimination, checking every division.
+Only that exact integer determinant establishes the all-field claim.
+
+All rows of the first, third and fifth families are orthogonal to their
+respective anchor rows. The certified anchor ranks and nondegeneracy of the
+ambient dot product bound their ranks above by seven, six and five. Thus the
+lower bounds give the exact spans in S1, S2 and S3prime.
+
+For W2 the verifier forms integer projected rows
+
+    D_u = 2 R_u - (R_u dot R_f)/4 R_f = 4 w_u.
+
+It divides each by its positive coordinate gcd and chooses its sign by its
+first nonzero coordinate. Every divisor is a power of two. These operations
+remain invertible over every K in the statement. The 56 rows form 28 rational
+directions with two rows per direction. Their 3276 triples have certified
+rank three. This also proves nonvanishing and pairwise distinction after
+reduction, since any pair belongs to such a triple. No extra direction can
+arise by reducing two proportional vectors.
+
+For the S3prime inventory, f,u,v are rationally dependent precisely when
+the two nonzero projections have the same projective direction. The verifier
+omits exactly those pairs and certifies every other anchor triple separately.
+This accounts for every rationally admissible pair in its stated domain.
+
+## Transport to every anchor
+
+For a doubled root a, the reflection is
+
+    H_a = I - a a^T/4.
+
+Since a^T a = 8, direct multiplication gives H_a^T H_a = I and H_a^2 = I.
+Its coefficients are in Z[1/2], so these identities hold over every K under
+consideration. On a doubled root R its image is
+
+    R - (a dot R)/4 a.
+
+The verifier checks all 14400 root images, including divisibility by four
+and membership in the signed root set. Each reflection gives a permutation
+of the 120 root lines. A bounded traversal of these permutations proves
+that the orbit of f contains all 120 lines. Each resulting product is an
+invertible isometry over Z[1/2], hence over K.
+
+These products transport root orthogonality, anchor independence, spans and
+orthogonal projection. Therefore the complete fixed-anchor certificates
+prove S1, S2, S3prime and W2 for every root line f. Multiplication by any
+representative sign has no effect on these assertions.
+
+## Scope and remaining obligations
+
+This is a scoped algebraic proof supported by an exhaustive finite integer
+certificate. The executable certificate and the written transport argument
+jointly establish the quantified field statement. The executable is not a
+formal proof-kernel check.
+
+The rank-nine pinning/classification argument, its sign logic, SAT encodings,
+refutations and other finite facts are inherited research and were not
+replayed. Applying this new lemma to a positive-characteristic classification
+still requires checking all remaining characteristic assumptions in that
+argument. No decoder COPY floor, native operation, physical caller, signed
+invoice, new kappa or complete multiplication theorem follows here.
+
+Power-of-two minors and integral root-reflection transport are established
+methods. CubeJerry's PR3095 and conorholds's PR3755 use them for different
+root/character span statements. They retain that methodological credit.
+The new result here is the complete all-odd-field S1/S2/S3prime/W2 input set
+and its explicit bounded integer certificates.

research/e8-odd-characteristic-spans/README.md

@@ -0,0 +1,95 @@
+# E8 span inputs have no exceptional odd prime
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Scoped proof with an exhaustive finite integer certificate. No new kappa.**
+The E8 facts S1, S2, S3prime and W2 used by DreamingOfClouds's
+[PR2819](https://github.com/CrocSwap/integer-mult-bounds/pull/2819) hold over
+**every field of characteristic different from two**. This supplies a new
+field range for the span inputs that its section 7 leaves open. The existing
+characteristic-zero classification and SAT work are cited, not audited.
+
+[PROOF.md](PROOF.md) states the exact domains. Orthogonal roots span the
+seven-, six- and five-dimensional complements of the specified one-, two-
+and three-root anchor sets. The 56 nonorthogonal neighbors of any root
+project to 28 distinct directions, with every three independent. No odd
+prime changes those conclusions.
+
+The new verifier constructs 6539 integer minors with absolute determinants
+in {2,4,8,16,32,64,128,256}. Each remains nonzero over every odd-characteristic
+field. Its complete fixed-anchor domain consists of one S1 matrix, 119 S2
+matrices and their 119 anchor pairs, 1512 S3prime matrices and their 1512
+anchor triples, and all 3276 projected-direction triples. It checks all
+14400 root images under the 120 integral reflections and verifies a
+120-line orbit to transport the result to every anchor.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/e8-odd-characteristic-spans/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-odd-characteristic-spans
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-odd-characteristic-spans --check-source-history
+```
+
+Local checks used CPython 3.12.15 on macOS 27.0.1 arm64. The two registered
+commands took 0.13 and 0.14 seconds locally, below their 60-second limits.
+
+The principal marker is `PASS_E8_ODD_CHARACTERISTIC_SPANS`. The verifier
+writes a JSON receipt to stdout, binding its certificate digest to SHA256
+hashes of the package and declared input files. Redirect outputs outside the
+checkout. It writes no files and executes no predecessor program.
+
+Modular elimination only selects minors. Exact fraction-free determinants
+supply the proof certificates. The checks include 673 comparisons with an
+independent Leibniz determinant formula, rejection of a singular matrix and
+odd-torsion matrices at three and five, and two dyadic-unit/power controls.
+All checks remain active under `-O`.
+
+## Limitations
+
+This does not extend the complete rank-nine classification to positive
+characteristic. Its remaining sign logic, pinning implications, other finite
+facts, SAT encodings and refutations were not assessed or replayed here.
+There is no decoder floor, native supplier, caller, signed invoice or
+selected-frontier change. The five selected framework assumptions remain.
+Independent human and formal proof-kernel review are unclaimed.
+
+The executable uses bounded exact integer arithmetic, without recursion.
+Every matrix has at most 63 rows and eight columns; every determinant has
+order at most seven. Managed Python allocation is a documented deviation
+from fixed-capacity allocation. Finite inventories bound live data. The
+certificate digest is generated, not a hand-written receipt. Historical
+source checks are byte bindings only.
+
+## Open next questions
+
+- Which remaining PR2819 classification implications require a further
+  characteristic restriction? Start by listing those implications and their
+  denominators. This matters because the new span inputs alone cannot admit
+  the classification in a new field; those implications remain the blocker.
+- Does an explicitly missing span input for P112 or P104 admit dyadic-unit
+  minors? First identify its exact incidence domain in a source package.
+  This could help the supplier geometries, but is blocked by that distinct
+  target specification. No punctured-unit result is claimed here.
+
+The same questions are structured in [TASK.json](TASK.json).
+
+## Credit and related work
+
+DreamingOfClouds retains PR2819's classification, naming and characteristic-zero
+span inputs, with its PR2784 lineage. The standard E8 root coordinates are
+also retained there. No predecessor source or credit line is changed.
+CubeJerry's [PR3095](https://github.com/CrocSwap/integer-mult-bounds/pull/3095)
+and conorholds's [PR3755](https://github.com/CrocSwap/integer-mult-bounds/pull/3755)
+use power-of-two minors and integral reflection transport for different
+root/character span questions. Those methods are established background.
+The new contribution is the all-odd-field S1/S2/S3prime/W2 input set and its
+complete bounded certificate. No literature-priority claim is made.
+
+The overlap check covered all 310 open PR bodies and complete Discussion
+pagination at the recorded snapshot, targeted merged-PR searches, and
+canonical-main README searches for the facts, their field range and more
+general formulations. The sparse local-note corpus was incomplete. No
+matching open PR was found. Unpublished work remains outside that coverage.

research/e8-odd-characteristic-spans/SOURCES.json

@@ -0,0 +1,54 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/e8-rank9-realisations/README.md",
+      "usage": "input",
+      "git_blob": "62c6efd17a3439e79c2eb4f260df00ef8c22eba8",
+      "sha256": "dd4d1f54ec6e0f41da85c5862304d8bcb8b252f50425f13467f230b69098568a"
+    },
+    {
+      "path": "research/e8-rank9-realisations/checks/e8lib.py",
+      "usage": "input",
+      "git_blob": "d802266a2850fe2d4941bd49154e5ae976443289",
+      "sha256": "b1a0339383cc4ae6957caec6a9feffb9fb344679cceeff8eca49996ff21bcf4d"
+    },
+    {
+      "path": "research/e8-rank9-realisations/checks/spans.py",
+      "usage": "input",
+      "git_blob": "1c2f7615972a06e45f57e72f19b8e4c1e8d6655d",
+      "sha256": "780d373d518e6c1830594d550f408cc7eac9da32a1527504efb6c32afd9e5e0a"
+    },
+    {
+      "path": "research/e8-rank9-realisations/checks/spans3.py",
+      "usage": "input",
+      "git_blob": "db00d69635acb9a973764fb6b273515c96b88bfa",
+      "sha256": "8d5b0c0270c916e9ce5136a2d95f06c4eff4769008534b8d2d83c402694e1d2d"
+    },
+    {
+      "path": "research/one-sided-padding-audit/README.md",
+      "usage": "provenance",
+      "git_blob": "f5a61bd2c3f30d24b6926667a015229c132671c3",
+      "sha256": "6291af467140df3cb9ca701c9f02e92b25b99869818589dc5b544a5d60eaff80"
+    },
+    {
+      "path": "research/e8-one-coset-deficiency/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "89c328853b8a7a49dbbd9d8e4a842e1e209974df",
+      "sha256": "d3dcc35205225547c13f8bc0ec3175da7aab41e54c7adc06f0c35c86f00b93e4"
+    }
+  ]
+}

research/e8-odd-characteristic-spans/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "All-odd-characteristic E8 orthogonal-complement span facts S1, S2, S3prime and projected-direction fact W2, certified by integral dyadic-unit minors.",
+  "scope_change_reason": "Answer PR2819 section 7 positive-characteristic boundary for its finite span inputs. This is an arithmetic side result rather than a physical decoder or signed-moment improvement.",
+  "bottleneck_link": "Removes the field-transfer obstacle for four algebraic inputs used in rank-nine decoder classification. It supplies no physical decoder or improvement to the binding complex invoice.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first all-odd-field span certificate; leave classification, SAT and physical realization obligations open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the all-field implication and reflection transport; verify.py generates 6539 exact power-of-two minors and a file-hash-bound JSON receipt without writing files.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Do all remaining PR2819 classification steps hold over every odd characteristic?",
+      "why_it_matters": "The new span theorem alone does not extend the rank-nine classification.",
+      "first_step": "List each remaining field assumption in the pinning and sign-logic arguments before any new finite run.",
+      "blocked_by": "The remaining algebraic implications and finite proof obligations have not been assessed in that field range."
+    },
+    {
+      "question": "Can the same integer-unit approach cover span inputs for punctured P112 or P104 classification?",
+      "why_it_matters": "Those geometries are closer to the productive suppliers but have different available root sets.",
+      "first_step": "Identify one explicitly missing span proposition in an existing punctured-unit package.",
+      "blocked_by": "A distinct valid target and its complete incidence domain must first be specified."
+    }
+  ],
+  "environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS 27.0.1 arm64",
+    "dependencies": "standard library only",
+    "playbook": "Autonomous local run"
+  }
+}