The Bridge Implication for the (3,4,∞) Lattice Form: Restriction Lemma for Ω0

A short note recording the lattice bridge checked in OmegaZero34/TetherInterface.lean. Proved in Lean: the classification uniqueness_over_Q of the invariant form, and the bridge implication restriction_lemma (nondegeneracy forces the scalar to be nonzero). Not proved: the geometric hypotheses, and X≃S^6 is not claimed. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/OmegaZero34 at commit 222e48d5db30f3b2097b4e8ca5bfc38b0a16b2ea.

Authors

Publication Details

Journal
Zenodo (CERN European Organization for Nuclear Research)
Published
2026-11-04
DOI
https://doi.org/10.5281/zenodo.23942460
Primary Topic
Geometric and Algebraic Topology
Type
preprint
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

The Bridge Implication for the (3,4,∞) Lattice Form: Restriction Lemma for Ω0

Benjamin Frohman
Zenodo (CERN European Organization for Nuclear Research)
Geometric and Algebraic Topology
preprint

The Bridge Implication for the (3,4,∞) Lattice Form: Restriction Lemma for Ω0

Benjamin Frohman
preprint en

Abstract

A short note recording the lattice bridge checked in OmegaZero34/TetherInterface.lean. Proved in Lean: the classification uniqueness_over_Q of the invariant form, and the bridge implication restriction_lemma (nondegeneracy forces the scalar to be nonzero). Not proved: the geometric hypotheses, and X≃S^6 is not claimed. The Lean development builds in CI (green on the commit archived here) with no sorry and no user-declared axioms. Source: https://github.com/BenFrohman/OmegaZero34 at commit 222e48d5db30f3b2097b4e8ca5bfc38b0a16b2ea.

Zenodo (CERN European Organization for Nuclear Research)
Geometric and Algebraic Topology
DOIOpen Access PDFOpenAlex
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Laika access coming soon
The Bridge Implication for the (3,4,∞) Lattice Form: Restriction Lemma for Ω0 — Benjamin Frohman · Zenodo (CERN European Organization for Nuclear Research) (2026) | TGRS Research Map | TGRS