v0.21.0 — stage G: the missing-object embedding route + the UOR Atlas formalized

v0.21.0 — stage G: the missing-object embedding route + the UOR Atlas formalized

Pure Lean 4 (no Mathlib, no sorry, no native_decide), choice-free {propext, Quot.sound}; CI green; honesty audit passes — now with a no-smuggling check (the Gate-A pairing must be λ-free, the metric analog of intrinsicH1_dict).

Outcome: LOCALIZED. The missing-object embedding route is built end to end and the UOR Atlas is formalized to its frontier; the gate ran and the crux did not close (the §9 Localized terminal state). hodgeIndexHolds / liPositivityHolds stay none — RH remains open, exactly per the bright line.

The embedding route

Model the Hodge-index slack as an isometric embedding ι of the primitive span into a definite atlas space, so that ‖ι Cₙ‖² = 2λₙ would force ⟨Cₙ,Cₙ⟩ ≤ 0 ∀n (= RH). Built as a sequence of green, audited bricks, each with a falsifier:

• Square/WeilPSD.lean — the finite-truncation PSD predicate; rank-one Gram = manifest square; Gate B free for any ℝ^D embedding (WeilPSD_gramOf); the embedding bridge.
• Square/FrobForm.lean — the full primitive form on the Frobenius carrier; diagonal forced to −2λₙ.
• Square/AtlasRule.lean — the zero-free atlas rule + growth pre-filter; cayley_relocation (the §6 recorded negative result: a zero-built candidate matches ⟺ RH).
• Square/KillTest.lean — the decidable finite-Gram kill-test.
• Square/GateA.lean — the λ-free pairing atlasPair; gateA_is_liNonneg (Gate A under free Gate B is RH); two-sided no-smuggling guards.
• Square/E8Seed.lean — the E₈ Gram = 4× the Cartan matrix (e8_is_cartan), PSD free.
• Square/GaugeTower.lean — the gauge tower with a metric; the make-or-break obstruction limit_indefinite_of_neg_signature.
• Square/StageG.lean — stageG_frontier_located + the conditional closure strictRealizes_closes_crux.
• Square/GateSanity.lean — crux_gate_faithful: the gate discriminates and closes on a genuine witness (it does not arbitrarily fail).

The UOR Atlas, formalized

From the uor-atlas.md formalization document — every facet (§1–§15) as facets of one {T,O} = (3,8) object:

• AtlasSpectrum.lean — the spectral operator M, signature Σ = {10,2,7,−1}, multiplicities {1,2,7,14}, trace 24, atlasM_indefinite; the Hurwitz norm as a different, definite object (§9).
• AtlasCharacteristics.lean / AtlasAddressing.lean / AtlasClasses.lean / AtlasConservation.lean — the convergence tower, the Euler–Lefschetz self-intersection, the prime skeleton = explicit-formula prime side Λ(p) = log p, the transforms as finite-order permutations, conservation.
• The discovery program — AtlasForcing, AtlasSynthesis (atlas_forced_web: every Atlas constant a function of {T,O}, no coincidences), AtlasExceptional (the Freudenthal–Tits magic square; dim G₂ = 14), AtlasCoxeter, AtlasModular (θ_{E₈^T} = E₄³), AtlasComposition (the 2/4/8-square Hurwitz identities, Degen's octonion identity by ring_uor), AtlasTopology, AtlasCalculus, and AtlasComplete (atlas_complete: the roll-up).

The genuine frontier this revealed

The Atlas's spectral operator is indefinite by design (its −1 reflection, dim 14 = dim G₂, sits in the odd degree where the Euler–Lefschetz self-intersection vanishes); its definite object is the Hurwitz norm, which the Atlas does not identify with the RH form. So the crux is not whole-form positive-definiteness — it is negative-semidefiniteness on the primitive part (the Lefschetz signature), governed by the zeros, exactly as BridgeFF.ff_hodge_iff_hasse has it for the curve. The crux refines to the prime–archimedean coupling sign (LefschetzCoupling.lean, genuine_crux_arch_coupling), conquered at the head (n = 1, 2) and in the Connes–Consani window (α(0) > 0), open outside.

The crux stays none; RH open. See CHANGELOG.md and ROADMAP.md for the full record.