Checks for the native Conway target

The cut-defined carrier excludes one half, separating it from the entire surreal field. The public equivalence exposes native subring divisibility. The zero-input certificate ensures that the standalone statement does not silently exclude the cancellation boundary.

theorem Tests.Conway.half_not_in_carrier : ¬ConwayRefinement.Standalone.Oz.IsConwayOmnificInteger 2⁻¹

The target's carrier is not the whole field of surreal numbers.

theorem Tests.Conway.omega_in_carrier : ConwayRefinement.Standalone.Oz.IsConwayOmnificInteger (NatOrdinal.toSurreal (NatOrdinal.of Ordinal.omega0)) ∧ ∀ (n : ℕ), ↑n < NatOrdinal.toSurreal (NatOrdinal.of Ordinal.omega0)

The carrier includes an actual infinite omnific integer, so it is not just the integers.

theorem Tests.Conway.native_endpoint (h : ConwayRefinement.Standalone.Oz.ConwayConjecture) (b : Surreal.OmnificInteger) : IsPrimal b

The endpoint uses divisibility in the actual omnific subring.

theorem Tests.Conway.zero_row (h : ConwayRefinement.Standalone.Oz.ConwayConjecture) : ∃ (e : Surreal) (f : Surreal) (g : Surreal) (h : Surreal), ConwayRefinement.Standalone.Oz.IsConwayOmnificInteger e ∧ ConwayRefinement.Standalone.Oz.IsConwayOmnificInteger f ∧ ConwayRefinement.Standalone.Oz.IsConwayOmnificInteger g ∧ ConwayRefinement.Standalone.Oz.IsConwayOmnificInteger h ∧ 0 = e * f ∧ 3 = g * h ∧ 0 = e * g ∧ 2 = f * h

A zero top row remains within the standalone conjecture's quantifiers.