Selfdual and antiselfdual split the six

NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.

The split: self-dual ⊕ anti-self-dual, 3 + 3 = 6. This is why four dimensions are special — only there does ★ map middle forms to middle forms.

Proposition

3 + 3 = choose 4 2

Proof

By decide in yang-mills.lean. The kernel reduces the proposition and reports no axiom dependency.

Sources and identifiers

• Lean source · src/pair/formal/proofs/yang-mills.lean
• Typeset paper · src/research/lean-theorems.tex
• Repository deposit · doi:10.5281/zenodo.21787144
• Author · ORCID 0009-0000-7312-9778
• Deposit record · yang-mills--selfdual_and_antiselfdual_split_the_six

Proved in the same file

• Middle forms have dimension six
• Star squares to the identity
• Star is an endomorphism only in the middle
• Involution splits the middle forms

All machine-checked theorems