An active research program formalizing the arithmetic surface Spec ℤ ×_{𝔽₁} Spec ℤ together with the Hodge-index positivity whose truth is the Riemann Hypothesis. It pairs a Lean 4 formalization — extending the UOR-Foundation library — that encodes the construction's honest epistemic status (verified and classical results carry their established status; the RH crux is encoded as not-asserted, never as proven) with research documents that specify the target object, the candidate-construction gap, the named obstructions, and a checkable verification ladder.