Three bridges

Placement

For a real-linear isometry $E$ and a center $\alpha$, the placement $z\mapsto\alpha+E(z)$ preserves the selected lengths $a\varphi$ and $a\pi$, hence $\lambda=\varphi/(\varphi+\pi)$ when $a>0$. Scaling about $\alpha$ commutes with that placement. The statement is already in the hosted files Placement.lean and Affine.lean. Those two files, and Dimension.lean, match the copies inside this package byte for byte. Their Mathlib build was not rerun. A drawing of one such placement into $\mathbb{R}^n$, $n\ge 4$, is on the geometry page at the higher-dimensional placement. The picture is a display of an explicit frame, $\theta=\pi/6$. It is not an additional theorem.

600-cell slice to the icosahedron

The twelve neighbors of $(-1,0,0,0)$, numbered 33 through 44, lie in the slice $p_0=-\varphi/2$. The map $L(p)=2\varphi(p_1,p_3,p_2)$ sends them to the twelve unnormalized icosahedral nodes. The checker reports 12 aligned nodes and all 56 monomials through degree five. For a linear field $f_w(u)=u\cdot w$,

$w=\dfrac{3-\varphi}{20}\sum_u u\,f_w(u).$

The identification of those normalized moments with the integral on the real sphere is a written argument in PROOFS.md. The Lean file checks the finite algebraic moments. It does not check that sphere integral. Quadratic-field reconstruction is not newly formalized here.

Golden block and the factor 211

The coordinate update is $B=13I+6F$, multiplication by $13+6\varphi$, where $F$ is the Fibonacci matrix. With $N(a,b)=a^2+ab-b^2$,

$N(B^n w)=211^n N(w).$

The conjugate multipliers are the roots of $X^2-32X+211$. That is one factor of the matrix polynomial in Paper IX, on this invariant block. The other factors are unchanged, and this note is not Paper IX. The checker recomputed all 480 geometric-mode entries. The graph fixture is SHA-256 40bc6a1d52efab3d75cf343e65ac06b314f9c9c375fc02bf6d45bf6bb21f9529Copy, the same fixture as the joining note.

What was run here

python3 verify_bridges.py and python3 -O verify_bridges.py were run on Python 3.10.21. Both exited 0, stderr was empty, and the stdout bytes match the supplied report, SHA-256 bb3740e643b95319606cda8c16280836d310d03558be63352bd74962506b8341Copy. The supplied execution names Python 3.12.14 for that same report.

The supplied execution also records Lean 4.19.0, exit 0, 27 theorems, axioms only propext and Quot.sound, and a rejected control that changes 211 to 210. Lean is not installed in this archive. That compiler run was not repeated. formal_proof_assistant_executed is false. The written proofs were not reviewed.

Check the Lean file yourself

OmegaBridges.lean is the file to compile. It imports Std only. It does not use the September Mathlib package. The source names 27 theorems and contains no sorry, admit, native_decide, or declared axiom.

Unpack the zip and use Lean 4.19.0 with its bundled Std:

lean OmegaBridges.lean
python3 run_checks.py --lean /absolute/path/to/lean

run_checks.py requires version 4.19.0, compiles the file, checks that every theorem is reported, rejects any axiom outside propext, Quot.sound, and Classical.choice, reruns both Python modes, regenerates the source, and requires the false law 210*gnorm to fail. The supplied compiler transcript is lean_compile.stdout.txt, 2,000 bytes, SHA-256 ee409bf130c87e803c6f5103d48996bb02df64c9058031e30d33f99618fe3f7bCopy. Matching that transcript checks the recorded compiler text. It does not replace running Lean.

Not claimed

• A new bit bound, a fast general decoder, or a cubature rule past the certificates already hosted.
• That the sphere-integral step was checked by Lean.
• The full Paper IX modulo-eight history decoder in Lean.
• That the source works are one theory.
• Peer review, independent reproduction, or a tenth Zenodo deposit.

Related pages, kept separate: the joining note, Paper IX, the September Lean package, a 13 November working note on bases and one binary64 pattern, and Frontier. Frontier remains the list of unfinished questions. This page is not one of those items.