Skip to content

Prove the uniform E8 one-coset budget and two-sided rank-nine floor #3755

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 20, 2026
Merged

Prove the uniform E8 one-coset budget and two-sided rank-nine floor #3755

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
117 changes: 117 additions & 0 deletions research/e8-one-coset-deficiency/CERTIFICATE.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,117 @@
{
"schema_version": 1,
"model": "Standard E8 roots scaled by 2; A8 label order",
"single_types": [
{"weight":1,"normal":1,"rows":[8,9,10,11,12,13,14,36],"determinant":-512},
{"weight":2,"normal":3,"rows":[1,2,3,4,5,6,7,43],"determinant":-256},
{"weight":3,"normal":7,"rows":[0,1,21,22,23,24,36,49],"determinant":512},
{"weight":4,"normal":15,"rows":[3,4,5,6,7,10,16,36],"determinant":-256},
{"weight":5,"normal":31,"rows":[0,1,2,3,30,31,32,36],"determinant":-1024},
{"weight":6,"normal":63,"rows":[5,6,7,12,18,23,27,36],"determinant":-256},
{"weight":7,"normal":127,"rows":[0,1,2,3,4,5,35,36],"determinant":-512},
{"weight":8,"normal":255,"rows":[7,14,20,25,29,32,34,36],"determinant":-256},
{"weight":9,"normal":511,"rows":[0,1,2,3,4,5,6,36],"determinant":256}
],
"forbidden_pairs": [
{"counts":[0,0,2,7],"a":511,"b":508,"rows":[0,15,16,17,18,19,20,36],"determinant":1024},
{"counts":[0,0,4,5],"a":511,"b":496,"rows":[0,1,2,26,27,28,29,38],"determinant":512},
{"counts":[0,0,6,3],"a":511,"b":448,"rows":[0,1,2,3,4,33,40,119],"determinant":-512},
{"counts":[0,0,8,1],"a":511,"b":256,"rows":[0,1,2,3,4,5,6,42],"determinant":-512},
{"counts":[0,1,1,7],"a":510,"b":509,"rows":[0,85,86,87,88,89,90,100],"determinant":512},
{"counts":[0,1,3,5],"a":510,"b":497,"rows":[0,1,2,65,66,67,68,69],"determinant":512},
{"counts":[0,1,5,3],"a":510,"b":449,"rows":[0,1,2,3,4,67,68,119],"determinant":-512},
{"counts":[0,1,7,1],"a":510,"b":257,"rows":[0,1,2,3,4,5,6,69],"determinant":-512},
{"counts":[0,2,0,7],"a":508,"b":511,"rows":[0,15,16,17,18,19,20,36],"determinant":1024},
{"counts":[0,2,2,5],"a":508,"b":499,"rows":[0,15,26,27,28,29,38,85],"determinant":-1024},
{"counts":[0,2,4,3],"a":508,"b":451,"rows":[0,15,16,17,33,34,40,119],"determinant":2048},
{"counts":[0,2,6,1],"a":508,"b":259,"rows":[0,15,16,17,18,19,42,89],"determinant":1024},
{"counts":[0,3,1,5],"a":504,"b":503,"rows":[2,9,15,38,39,40,41,42],"determinant":512},
{"counts":[0,3,3,3],"a":504,"b":455,"rows":[2,3,4,9,15,40,41,119],"determinant":-512},
{"counts":[0,3,5,1],"a":504,"b":263,"rows":[2,3,4,5,6,9,15,42],"determinant":-512},
{"counts":[0,4,0,5],"a":496,"b":511,"rows":[0,1,2,26,27,28,29,38],"determinant":512},
{"counts":[0,4,2,3],"a":496,"b":463,"rows":[0,1,2,26,33,34,40,119],"determinant":1024},
{"counts":[0,4,4,1],"a":496,"b":271,"rows":[0,1,2,26,27,28,42,112],"determinant":1024},
{"counts":[0,5,1,3],"a":480,"b":479,"rows":[4,11,17,22,26,40,41,119],"determinant":-512},
{"counts":[0,5,3,1],"a":480,"b":287,"rows":[4,5,6,11,17,22,26,42],"determinant":-512},
{"counts":[0,6,0,3],"a":448,"b":511,"rows":[0,1,2,3,4,33,40,119],"determinant":-512},
{"counts":[0,6,2,1],"a":448,"b":319,"rows":[0,1,2,3,4,33,42,119],"determinant":1024},
{"counts":[0,7,1,1],"a":384,"b":383,"rows":[6,13,19,24,28,31,33,42],"determinant":-512},
{"counts":[0,8,0,1],"a":256,"b":511,"rows":[0,1,2,3,4,5,6,42],"determinant":-512},
{"counts":[1,0,1,7],"a":510,"b":508,"rows":[0,85,86,87,88,89,90,100],"determinant":512},
{"counts":[1,0,3,5],"a":510,"b":496,"rows":[0,1,2,65,66,67,68,69],"determinant":512},
{"counts":[1,0,4,4],"a":510,"b":480,"rows":[4,5,6,7,66,71,75,86],"determinant":512},
{"counts":[1,0,5,3],"a":510,"b":448,"rows":[0,1,2,3,4,67,68,119],"determinant":-512},
{"counts":[1,0,7,1],"a":510,"b":256,"rows":[0,1,2,3,4,5,6,69],"determinant":-512},
{"counts":[1,1,0,7],"a":508,"b":510,"rows":[0,85,86,87,88,89,90,100],"determinant":512},
{"counts":[1,1,2,5],"a":508,"b":498,"rows":[0,16,17,18,19,20,21,36],"determinant":1024},
{"counts":[1,1,4,3],"a":508,"b":450,"rows":[0,18,19,20,23,27,30,36],"determinant":1024},
{"counts":[1,1,6,1],"a":508,"b":258,"rows":[0,20,25,29,32,34,35,36],"determinant":1024},
{"counts":[1,2,1,5],"a":504,"b":502,"rows":[2,10,11,12,13,14,16,37],"determinant":1024},
{"counts":[1,2,2,4],"a":504,"b":486,"rows":[4,5,6,7,9,10,15,37],"determinant":-512},
{"counts":[1,2,3,3],"a":504,"b":454,"rows":[2,3,4,12,13,14,18,37],"determinant":512},
{"counts":[1,2,5,1],"a":504,"b":262,"rows":[2,3,4,5,6,14,37,69],"determinant":512},
{"counts":[1,2,6,0],"a":504,"b":6,"rows":[9,10,11,12,13,14,15,37],"determinant":512},
{"counts":[1,3,0,5],"a":496,"b":510,"rows":[0,1,2,65,66,67,68,69],"determinant":512},
{"counts":[1,3,2,3],"a":496,"b":462,"rows":[0,1,2,27,28,29,30,38],"determinant":512},
{"counts":[1,3,4,1],"a":496,"b":270,"rows":[0,1,2,29,32,34,35,38],"determinant":512},
{"counts":[1,4,0,4],"a":480,"b":510,"rows":[4,5,6,7,66,71,75,86],"determinant":512},
{"counts":[1,4,1,3],"a":480,"b":478,"rows":[4,12,13,14,18,23,27,39],"determinant":1024},
{"counts":[1,4,3,1],"a":480,"b":286,"rows":[4,5,6,14,20,25,29,39],"determinant":512},
{"counts":[1,4,4,0],"a":480,"b":30,"rows":[11,12,13,14,17,22,26,39],"determinant":512},
{"counts":[1,5,0,3],"a":448,"b":510,"rows":[0,1,2,3,4,67,68,119],"determinant":-512},
{"counts":[1,5,2,1],"a":448,"b":318,"rows":[0,1,2,3,4,34,40,119],"determinant":512},
{"counts":[1,6,1,1],"a":384,"b":382,"rows":[6,14,20,25,29,32,34,41],"determinant":1024},
{"counts":[1,6,2,0],"a":384,"b":126,"rows":[13,14,19,24,28,31,33,41],"determinant":512},
{"counts":[1,7,0,1],"a":256,"b":510,"rows":[0,1,2,3,4,5,6,69],"determinant":-512},
{"counts":[2,0,2,5],"a":508,"b":496,"rows":[0,15,26,27,28,29,38,85],"determinant":-1024},
{"counts":[2,0,4,3],"a":508,"b":448,"rows":[0,15,16,17,33,34,40,119],"determinant":2048},
{"counts":[2,0,6,1],"a":508,"b":256,"rows":[0,15,16,17,18,19,42,89],"determinant":1024},
{"counts":[2,1,1,5],"a":504,"b":500,"rows":[3,4,5,6,7,10,15,38],"determinant":-512},
{"counts":[2,1,3,3],"a":504,"b":452,"rows":[5,6,7,12,15,16,17,40],"determinant":-1024},
{"counts":[2,1,5,1],"a":504,"b":260,"rows":[7,14,15,16,17,18,42,43],"determinant":512},
{"counts":[2,2,0,5],"a":496,"b":508,"rows":[0,15,26,27,28,29,38,85],"determinant":-1024},
{"counts":[2,2,2,3],"a":496,"b":460,"rows":[0,15,26,33,34,40,44,87],"determinant":1024},
{"counts":[2,2,4,1],"a":496,"b":268,"rows":[0,15,26,27,28,42,44,89],"determinant":1024},
{"counts":[2,3,1,3],"a":480,"b":476,"rows":[5,6,7,12,17,22,26,40],"determinant":-1024},
{"counts":[2,3,3,1],"a":480,"b":284,"rows":[7,14,17,18,19,22,42,45],"determinant":-512},
{"counts":[2,4,0,3],"a":448,"b":508,"rows":[0,15,16,17,33,34,40,119],"determinant":2048},
{"counts":[2,4,2,1],"a":448,"b":316,"rows":[0,15,16,17,33,42,46,119],"determinant":-1024},
{"counts":[2,5,1,1],"a":384,"b":380,"rows":[7,14,19,24,28,31,42,47],"determinant":-512},
{"counts":[2,6,0,1],"a":256,"b":508,"rows":[0,15,16,17,18,19,42,89],"determinant":1024},
{"counts":[3,0,1,5],"a":504,"b":496,"rows":[2,9,15,38,39,40,41,42],"determinant":512},
{"counts":[3,0,3,3],"a":504,"b":448,"rows":[2,3,4,9,15,40,41,119],"determinant":-512},
{"counts":[3,0,4,2],"a":504,"b":384,"rows":[6,7,13,19,41,102,105,107],"determinant":512},
{"counts":[3,0,5,1],"a":504,"b":256,"rows":[2,3,4,5,6,9,15,42],"determinant":-512},
{"counts":[3,1,0,5],"a":496,"b":504,"rows":[2,9,15,38,39,40,41,42],"determinant":512},
{"counts":[3,1,2,3],"a":496,"b":456,"rows":[2,9,15,27,28,29,30,40],"determinant":512},
{"counts":[3,1,4,1],"a":496,"b":264,"rows":[2,9,15,29,32,34,35,42],"determinant":512},
{"counts":[3,2,1,3],"a":480,"b":472,"rows":[4,11,17,23,24,25,27,40],"determinant":512},
{"counts":[3,2,2,2],"a":480,"b":408,"rows":[6,7,13,19,22,23,26,41],"determinant":1024},
{"counts":[3,2,3,1],"a":480,"b":280,"rows":[4,5,6,11,17,25,42,103],"determinant":512},
{"counts":[3,3,0,3],"a":448,"b":504,"rows":[2,3,4,9,15,40,41,119],"determinant":-512},
{"counts":[3,3,2,1],"a":448,"b":312,"rows":[2,3,4,9,15,34,42,119],"determinant":512},
{"counts":[3,4,0,2],"a":384,"b":504,"rows":[6,7,13,19,41,102,105,107],"determinant":512},
{"counts":[3,4,1,1],"a":384,"b":376,"rows":[6,13,19,25,29,32,34,42],"determinant":512},
{"counts":[3,5,0,1],"a":256,"b":504,"rows":[2,3,4,5,6,9,15,42],"determinant":-512},
{"counts":[4,0,2,3],"a":496,"b":448,"rows":[0,1,2,26,33,34,40,119],"determinant":1024},
{"counts":[4,0,4,1],"a":496,"b":256,"rows":[0,1,2,26,27,28,42,112],"determinant":1024},
{"counts":[4,1,1,3],"a":480,"b":464,"rows":[5,6,7,12,18,23,26,40],"determinant":-512},
{"counts":[4,1,3,1],"a":480,"b":272,"rows":[7,14,20,25,26,27,28,42],"determinant":-1024},
{"counts":[4,2,0,3],"a":448,"b":496,"rows":[0,1,2,26,33,34,40,119],"determinant":1024},
{"counts":[4,2,2,1],"a":448,"b":304,"rows":[0,1,2,26,33,42,112,119],"determinant":2048},
{"counts":[4,3,1,1],"a":384,"b":368,"rows":[7,14,20,25,28,31,33,42],"determinant":-1024},
{"counts":[4,4,0,1],"a":256,"b":496,"rows":[0,1,2,26,27,28,42,112],"determinant":1024},
{"counts":[5,0,1,3],"a":480,"b":448,"rows":[4,11,17,22,26,40,41,119],"determinant":-512},
{"counts":[5,0,3,1],"a":480,"b":256,"rows":[4,5,6,11,17,22,26,42],"determinant":-512},
{"counts":[5,1,0,3],"a":448,"b":480,"rows":[4,11,17,22,26,40,41,119],"determinant":-512},
{"counts":[5,1,2,1],"a":448,"b":288,"rows":[4,11,17,22,26,34,42,119],"determinant":512},
{"counts":[5,2,1,1],"a":384,"b":352,"rows":[6,13,19,24,28,32,42,117],"determinant":512},
{"counts":[5,2,2,0],"a":384,"b":96,"rows":[31,32,33,59,80,95,105,111],"determinant":-512},
{"counts":[5,3,0,1],"a":256,"b":480,"rows":[4,5,6,11,17,22,26,42],"determinant":-512},
{"counts":[6,0,2,1],"a":448,"b":256,"rows":[0,1,2,3,4,33,42,119],"determinant":1024},
{"counts":[6,1,1,1],"a":384,"b":320,"rows":[7,14,20,25,29,32,33,42],"determinant":-512},
{"counts":[6,2,0,1],"a":256,"b":448,"rows":[0,1,2,3,4,33,42,119],"determinant":1024},
{"counts":[7,0,1,1],"a":384,"b":256,"rows":[6,13,19,24,28,31,33,42],"determinant":-512},
{"counts":[7,1,0,1],"a":256,"b":384,"rows":[6,13,19,24,28,31,33,42],"determinant":-512}
]
}
134 changes: 134 additions & 0 deletions research/e8-one-coset-deficiency/FORMAL.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,134 @@
# Formal scope

Prepared by conorholds with substantial OpenAI Codex assistance. Apache-2.0.

The package includes `formal/BinaryCliqueCore.lean` and
`formal/ConsumerArithmetic.lean`, both importing only Lean `Init`. All six
declarations passed targeted Lean 4.21.0 checks with warnings treated as errors,
one Lean thread, and an external 512 MiB RSS watchdog. The files were checked
serially:

| Source | Result | Elapsed | Peak process-group RSS |
|---|---|---|---|
| `BinaryCliqueCore.lean` | PASS, exit zero | 1.417 s | 262.30 MiB |
| `ConsumerArithmetic.lean` | PASS, exit zero | 1.135 s | 235.02 MiB |

Status: **PASS** for these scoped formal results.

## Statements and explicit assumptions

`BinaryCliqueCore.lean` defines `binarySum zero add xs` as the right-associated
sum of a finite list. Its five declarations prove:

1. `detector_sum_zero`: an additive Boolean-valued detector vanishes on a sum
when it vanishes on every summand.
2. `detector_sum_selected`: if a list has no repeated vectors, a detector which
is one on one selected vector and zero on the others evaluates to one on
their sum.
3. `compatible_clique_zero_sum_empty`: a distinct list of nonzero pairwise
compatible vectors has zero sum only if it is empty. Pairing additivity
detects every odd member of a putative relation. The remaining even members
have pairwise distinct Boolean colors, so there are at most two. A nonzero
singleton and two distinct vectors cannot have zero sum.
4. `compatible_transversal_zero_sum_empty`: for membership predicates `Z i`
with pairwise trivial intersections, nonzero choices from distinct indices
cannot collide. If all nonzero cross-choices are compatible, any finite
zero relation among these grouped choices has an empty active index list.
5. `BinaryNine.clique_zero_sum_empty`: instantiate the clique theorem in the
concrete binary space `Fin 9 → Bool`. Zero is pointwise false, addition is
pointwise XOR, and the pairing is the XOR of coordinatewise AND over the
explicit coordinate list `[0, 1, 2, 3, 4, 5, 6, 7, 8]`. All addition and
pairing laws required by the abstract theorem are proved. Distinctness,
nonzero vectors, orthogonality, and the even-color condition remain explicit
premises.

`ConsumerArithmetic.lean` proves `copy_ge_seventy_two`: for arbitrary natural
numbers `COPY`, `m`, `s`, and `t`, the two explicit premises
`9 * m ≤ COPY + 9 * s + 9 * t` and `8 + s + t ≤ m` imply `72 ≤ COPY`.
This is only the arithmetic consequence. The file does not derive either
premise from ranks, dimensions, the Sylvester inequality, or E8 geometry.

In the first four declarations, the operations are parameters, not undeclared
axioms. Their exact laws are explicit premises:

- `add x zero = x` and `add x y = zero ↔ x = y`, the characteristic-two
cancellation law;
- `β x zero = false` and
`β x (add y z) = Bool.xor (β x y) (β x z)`;
- pairing zero for distinct compatible vectors;
- different Boolean colors for distinct even compatible vectors, where even
means `β x x = false`;
- for the grouped-family corollary, trivial intersections and compatibility of
all nonzero cross-choices, together with membership/nonzero conditions on
the selected grouped vectors.

`BinaryNine.clique_zero_sum_empty` discharges the first two algebraic premise
groups for its concrete operations. It retains the geometric orthogonality and
even-color premises. Neither symmetry nor nondegeneracy of `β` is silently
assumed by the abstract proof. No fixed number of summands is assumed.

Each public theorem has a `#print axioms` audit. The successful checks reported
no axioms for `detector_sum_zero`, and only `propext`, `Classical.choice`, and
`Quot.sound` for the other four clique/grouping declarations. The arithmetic
theorem depends only on `propext`. There were no `sorryAx` dependencies or
compiler warnings. Neither source contains a `sorry` or custom
`axiom` declaration.

## Boundary of the formal result

This is a checked binary clique argument with a concrete nine-coordinate
instantiation, not a formalization of the complete E8 theorem over fields of
characteristic different from two. The identification of the E8 quotient with
the concrete binary coordinate space, its geometric color map, nondegeneracy,
and verification of the geometric compatibility premises are not formalized.
Neither are the construction of the annihilators `Z i`, their
intersection/cross-compatibility properties, the grouping of arbitrary scalar
relations, the equivalence with Mathlib `LinearIndependent`, the finrank
direct-sum budget, the scalar rank comparisons and field transfer, or the
derivation of the two Sylvester/deficiency consumer premises. Those steps
remain in PROOF.md; only their final natural-number consequence is separately
formalized in `ConsumerArithmetic.lean`.

The further singleton-pair classification and rank-(10,8) consequence in
`SPARSE-PAIR.md` are written proofs. No new formal declaration covers their
projective-ray classification, filtered-span basis bound or decoder assembly.

## Toolchain and replay

The repository's `formal/lean/lean-toolchain` pins
`leanprover/lean4:v4.21.0`. The checked sources need that Lean distribution and
`Init` only; they have no mathlib, external certificate, or package dependency.

From the isolated worktree root, the local cached invocation is:

```sh
../e8-formal-work/toolchain/lean-4.21.0-darwin_aarch64/bin/lean \
--threads=1 -DwarningAsError=true \
research/e8-one-coset-deficiency/formal/BinaryCliqueCore.lean

../e8-formal-work/toolchain/lean-4.21.0-darwin_aarch64/bin/lean \
--threads=1 -DwarningAsError=true \
research/e8-one-coset-deficiency/formal/ConsumerArithmetic.lean
```

The available cache is a local convenience, not a committed binary bundle. A
provisioned Lean 4.21.0 binary can run the same sources and flags directly. No
`lake` command or full build is required. The coordinating agent scheduled the
recorded replays under a separate 512 MiB RSS watchdog; the commands above alone
do not provide that external limit. Finish each command before starting the
next. No Lean jobs were run concurrently.

## Resource-limited drafts

Two exploratory mathlib drafts were preserved privately outside this package
and are not publication artifacts or formal claims. Their attempted checks
were stopped before compiler diagnostics by the 1024 MiB RSS watchdog:

| Draft | Result |
|---|---|
| Generic independent-transversal/direct-sum/finrank draft | STOPPED, 1033.16 MiB, 3.497 s; default Lean thread count |
| Generic orthogonal coefficient-detection draft | STOPPED, 1049.67 MiB, 3.266 s; one Lean thread |

These stops establish neither a theorem failure nor successful elaboration.
The Init-only sources replace their formal coverage in this package. Full Lean
project verification and clean toolchain provisioning were not run.
Loading