GU in Lean

A machine-checked auditGeometric Unity

Does Geometric Unity stand up?

Geometric Unity (GU) is a draft theory by Eric Weinstein, from April 2021.

We check it in Lean. Lean is a proof checker. It accepts only airtight proofs.

Floors 1–3Built and checked
Floors 5–6Partly checked
Floor 7Mostly not reached
Main findingOn floor 4, the arrow of time flips

GU is a tower. Each floor stands on the one below.

  • Checked by machine
  • Partly checked
  • Not reached
  • Obstruction found
  1. Floor 7: Physics output Not reached 3 generations, the Standard Model, predictions A few pieces checked (one generation, one mixing angle)
  2. Floor 6: Field equations Partly Einstein-like and Yang-Mills-like equations, from one “Shiab” operator Core identity proved Defects found (a dropped star, equations that do not follow)
  3. Floor 5: Gauge group & action Partly The big symmetry group, and the energy function of the theory Algebra checked Several defects
  4. Floor 4: Spinors (matter)We are here Checked: obstruction Where electrons and quarks would live. Needs a “spin structure”. Obstruction found
  5. Floor 3: The 14-dim bundle C Built, checked A 14-dimensional space built over spacetime, with a (7,7) geometry
  6. Floor 2: The space of all metrics Y Built, checked Every possible way to measure distances, at every point
  7. Floor 1: Spacetime X Given Our 4-dimensional world

On floor 4, the arrow of time flips.

Before matter can live on the 14-dim bundle, GU needs one consistent arrow of time on it, everywhere.

Start: the arrow of time points one way.

  1. Pick a loop of metrics. (A metric is a way to measure distances.)
  2. Walk once around it, carrying the arrow of time.
  3. The arrow comes back reversed, like on a Möbius strip.

So GU’s spinors (matter) cannot exist on the full space, as written.

Machine-proved · Phase 4

What if GU means a two-piece group?

We checked this other reading too. Its second piece flips the sign of every spinor pairing (machine-proved). That this breaks GU’s matter setup is our reading, not yet machine-checked.

Sign flip machine-proved · Phase 6

The fix: a double cover.

Take two sheets, glued together. One loop takes you to the other sheet. Two loops bring you home.

On the double cover, the arrow of time is consistent. Spinors exist on flat space, and on any spacetime with a global frame. In general: open.

Start: sheet A.

  • Arrow of time, for every spacetimeMachine-proved
  • Spinors on ℝ⁴ (flat 4D space)Machine-proved
  • Spinors, any spacetime with a global frameMachine-proved
  • Spinors in general, locallyYes
  • Spinors in general, globallyOpen question

The idea of a double cover is standard. Applying it here, and proving it by machine, is new as far as we found.

Progress so far.

  1. Phase 4

    The twist

    Found the obstruction: the arrow of time flips.

    Machine-proved
  2. Phase 5

    The double cover

    Built the double cover. Spinors on ℝ⁴ (flat 4D space).

    Machine-proved
  3. Phase 6

    Every spacetime

    The fix works for every spacetime (the arrow-of-time part).

    Spinors in general: locally yes. Globally: an open question.

    The two-piece group reading flips every spinor pairing (its effect on the matter setup: our reading).

    Machine-proved
  4. Phase 7–8 · now

    Tidy the edges

    Tidying the fix’s edges, plus public tooling.

    • Done · P7 · item 1The pieces of the symmetry group O(7,7)
    • Done · P7 · item 2Spinors for every spacetime with a global frame, e.g. flat space, or flat space with a hole
    • Partly · P7 · item 3A yes/no test for spinors in general (on one fixed patchwork)
    • Done · P7 · item 4A first spinor bundle on the double cover (flat space)
    • Done · Phase 8, items 1 and 4The space GU’s gauge symmetry acts on, built on the double cover (flat space; nothing living on it yet). Swapping the time direction needs the second piece of the symmetry group

What could be published, honestly.

ResultNoveltyPublishable?
The arrow-of-time obstruction in GU’s 14-dim bundle We found no prior statement of it. Likely
As a short note, once an expert confirms it isn’t known.
The double-cover fix: arrow of time restored for every spacetime; spinors for spacetimes with a global frame The idea is standard. Applying and proving it here is new, as far as we found. Yes
As part of the same note.
The two-piece group flips every spinor pairing, so it likely fails GU’s matter setup Sharpens the obstruction (last step informal). Yes
Makes the note stronger.
The whole machine-checked audit (defects, confirmations) The first formal audit of the draft that we found. Yes
As a formalisation paper.
Most Phase 7 items (O(7,7) pieces, tooling) Classical maths, or engineering. No
They support the paper, but aren’t news.

First, an expert check.

Nothing is published until an expert confirms the obstruction isn’t already known. A note for experts is ready.

Read the expert note

Next: floor 5, on top of the fix.

Build GU’s spinor bundle on the double cover

Done for flat space, with the space GU’s gauge symmetry acts on

Check the field equations (floor 6) there

Not yet checked. One thing is already clear, and classical: the two time directions are related only by the second piece of the symmetry group, which flips the sign of spinor pairings. Whether GU’s equations survive that is the open question.

Two possible outcomes

If yes

The floor-4 obstruction is repaired

The double cover would remove it. A stronger paper.

If no

A second obstruction

Also publishable.