Openness of strict dual and cap signs
Abstract
The strict dual/cap Lorentz sign region is open in hyperbolic three-space.
The hyperbolic lift is continuous in upper-half-space coordinates. Each dual and original-row Lorentz pairing is therefore continuous, and the finite intersection of their strict sign sets is open.
Theorem 1.1 (The strict dual/cap region is open).
Proof. Machine-checked in Lean as D5/S3/Geometry/Hyperideal/LengthGramStrictOpen.strictDualCapRegion_isOpen (✓ std3). ∎
Source. Repository-derived.
Commentary.
The proof expands the lift coordinates, proves continuity of the lift, and applies finite intersection to the eight strict inequalities.