Quotient page lifts to a cover-level rational page

This is the covering-theory lift behind the Levi-Civita transport: a quotient page ascends to the cover.

Let $\varphi$ be a flow on the selected Levi-Civita component with antipodal equivariance, and suppose the component is antipodally invariant and free, the descended quotient dynamics are jointly continuous, and $\gamma$ is a closed orbit whose half-period image is a prime quotient binding (i.e. $\gamma$ is an antipodal double cover). If $\gamma$ bounds a rational disk-like global surface of section $Q$ in the antipodal quotient, then there exists a lifted rational page upstairs: a smooth embedded immersed disk with boundary $\gamma$, transverse interior, exactly opposite-boundary antipodal identifications, and two-sided unbounded returns against either deck lift of its interior.

The content is the standard path-lifting argument through the free double cover identified in Joung--van Koert Proposition 2.4: the quotient disk lifts to a smooth immersed disk because the cover is a local homeomorphism, the boundary lifts to the closed double orbit by the prime-binding hypothesis, antipodal fibers upstairs are exactly the opposite-boundary pairs because the deck action is free, and transversality plus unbounded returns pull back under the covering projection.

Formalization Note Lean packages the upstairs data as the mission's LiftedRationalPage structure and the quotient data as RationalDiskLikeGlobalSurfaceOfSection.