# Three concrete dimensional and algebraic bridges in OMEGA

Matthew Alan Newman's OMEGA constructions; synthesis dated 10 November 2026.

This supplement identifies explicit connections, with a self-contained Lean
file for the golden-pair algebra and the local 600-cell sampling data. It
preserves the earlier publication packages. It does not change Paper IX.

## 1. Planar OMEGA placed in three or more dimensions

Let the existing marked planar curve at radius a be Gamma_a. Its selected
measurements are G(a)=a*phi and C(a)=a*pi. For a real-linear isometric embedding
E from the plane into a real normed space V and a center alpha, put

    place(z) = alpha + E(z).

Isometry preserves the distances used by G; linear isometry also preserves
the arc-speed integral defining C. Therefore

    G(placed Gamma_a) = a*phi,
    C(placed Gamma_a) = a*pi,
    G/(G+C) = phi/(phi+pi),       a > 0.

For the homothety H_{alpha,k}(v)=alpha+k(v-alpha), linearity gives

    H_{alpha,k}(place(z)) = place(k*z).

Consequently placing the planar construction and scaling it commute. The
same statement applies in R^3, R^4, or another ambient space admitting E.
The intrinsic planar dimension and the ambient dimension remain explicit.

**Existing public Lean source:** `/formal/Omega/Placement.lean`, especially
`placed_G`, `placed_C`, `provenance_all_placements`, and `placed_homothety`;
`/formal/Omega/Affine.lean`, especially `observation_commutes`. These source
files were read and hashed in this session. Their Mathlib build was not rerun
as part of this Std-only supplement. The source and the site's earlier build
record are separate evidence from the new compiler run below.

## 2. The 4D 600-cell contains the 3D sampling configuration

Use the pinned 120-vertex coordinate construction. A pair (a,b) represents
(a+b*phi)/2. Vertex 0 is p0=(-1,0,0,0). Its twelve neighbors, numbered 33..44,
all have first coordinate -phi/2. Thus their remaining coordinates form a
three-dimensional vertex figure.

Define the explicit map on that affine slice by

    L(p0,p1,p2,p3) = 2*phi*(p1,p3,p2).

The coordinate swap aligns the sampling convention used in the earlier
joining checker. It is a fixed orthogonal permutation. Its inverse is

    L^-1(u0,u1,u2) = (-phi/2, u0/(2*phi), u2/(2*phi), u1/(2*phi)).

Exact evaluation gives precisely the twelve cyclic-coordinate points

    (0, +/-1, +/-phi),
    (+/-1, +/-phi, 0),
    (+/-phi, 0, +/-1).

These are the standard icosahedral nodes already used by the 3D sampling
branch. Every node has squared radius r^2=2+phi. The unit-sphere version is
u/r. The original neighbor figure has squared radius

    (2+phi)/(4*phi^2) = (3-phi)/4.

This is an exact affine identification of a specified local 600-cell figure
with a specified 3D sampling set.

### Degree-five moments

For exponents (a,b,c) with a+b+c <= 5, sum the monomial x^a y^b z^c over
the twelve unnormalized nodes. There are 56 such exponent triples. The sums
are:

| Exponents | Sum |
| --- | --- |
| (0,0,0) | 12 |
| Any odd exponent | 0 |
| A permutation of (2,0,0) | 4(2+phi) |
| A permutation of (4,0,0) | 12+12phi |
| A permutation of (2,2,0) | 4+4phi |

Because (2+phi)^2=5+5phi, after normalization and division by 12 these become
1, 0, 1/3, 1/5, and 1/15. They are the corresponding normalized spherical
moments. Monomial linearity then gives the usual degree-five cubature rule
on S^2. This last identification with the real sphere integral is a written
argument; the companion Lean file checks every finite algebraic moment and
proves its universal exponent statement for all a+b+c <= 5.

### An explicit sampling inverse

Let U have the twelve unnormalized icosahedral nodes as its rows. The
degree-two moments give

    U^T U = 4(2+phi) I_3.

For a linear field f_w(u)=u dot w, all its coefficients are recovered by

    w = [1/(4(2+phi))] sum_u u*f_w(u)
      = [(3-phi)/20] sum_u u*f_w(u).

The Lean theorem `linear_field_reconstruction` proves the exact integer-pair
implementation for every w in Z[phi]^3, including signed coefficients. The
division by 20 is exact on valid sample records. The associated injectivity
theorem is universal, not a check of a finite selection of coefficient vectors.
The displayed real matrix inverse follows from the same finite Gram identity.

This links a local part of the 4D recovery graph to the 3D sampling branch by
an explicit map and a concrete left inverse. Quadratic-field reconstruction
uses the existing nine-dimensional sampling inverse; it is not newly
formalized by the linear-field theorem here.

## 3. Golden arithmetic, Fibonacci evolution, and a spectral factor

Write a+b*phi as the integer pair (a,b), with multiplication

    (a,b)*(c,d) = (ac+bd, ad+bc+bd).

Its Galois conjugate is (a+b,-b), and its norm is

    N(a,b) = a^2+ab-b^2.

Direct expansion proves N(x*y)=N(x)*N(y). For the 600-cell coordinate
matrices 2C=C0+phi*C1, the geometric coefficient update is

    B(a,b) = (13a+6b, 6a+19b).

This is multiplication by alpha=13+6phi. It is also

    B = 13 I + 6 F,     F(a,b)=(b,a+b),

where F is the ordinary Fibonacci recurrence matrix. Its nth power acts as
multiplication by alpha^n. The finite matrix premise connecting this block
to the actual 600-cell matrix M=13I+A is checked on all 480 coordinate
entries by Lean, using the same literal 120 vertices and exact adjacency
test as the pinned fixture. Equivalently,

    A C0 = 6 C1,
    A C1 = 6 C0+6 C1.

The multiplier's conjugate is 19-6phi, so

    alpha + alpha' = 32,
    alpha*alpha' = 211.

Consequently B satisfies

    B^2 - 32 B + 211 I = 0,
    N(B^n w) = 211^n N(w),     n >= 0.

These identities are proved for every integer pair and every natural n in
the companion Lean file. Since phi=(1+sqrt(5))/2, the two real multipliers
are 16+3sqrt(5) and 16-3sqrt(5), the roots of

    X^2 - 32X + 211.

That is exactly one factor in Paper IX's matrix polynomial. The number 211
therefore has an explicit geometric/algebraic origin: it is the norm of the
golden multiplier acting on the coordinate-derived signal modes. The
identity proves this factor on that invariant block; the other factors of
the full matrix polynomial are separate components of the existing certificate.

## 4. The resulting composed route

There is now a concrete route from the local 600-cell neighbor slice to the
icosahedral sampling set and to reconstructed field coefficients. A specified
finite coefficient codec e, followed by an existing witnessed-history
encoder with inverse D, carries those coefficients through exact recovery:

    coefficient_decoder o e^-1 o D o History o e o Samples = identity.

This composition uses the stated sampling class, finite codec, and history
inverse. The new Lean file formalizes the local identification, finite
moments, golden block, and linear-field inverse. It does not instantiate
the entire Paper IX modulo-eight history decoder in Lean.

## Reproduction and evidence

Use Lean 4.19.0, with its bundled Std library:

    lean OmegaBridges.lean
    python3 verify_bridges.py
    python3 -O verify_bridges.py

The Lean file is self-contained. Optional source regeneration is
`python3 build_lean_source.py`; it uses the included `.inc` fragments and
the same pinned vertex construction. `run_checks.py` reruns the compiler,
checks the per-theorem axiom inventory, and runs a deliberately false
norm-law control. `EXECUTION.json` records only actual runs.

The graph digest is
`40bc6a1d52efab3d75cf343e65ac06b314f9c9c375fc02bf6d45bf6bb21f9529`.
`SOURCES.json` identifies the source URLs and bytes consulted. The package
does not claim a new bit bound, a new high-degree cubature rule, or an
independent third-party reproduction of OMEGA.