Finite covers of signed return atlases

Abstract

The primitive-base period ratio is the exact degree of an intertwining map, even for infinite noncommutative deck groups.

Let A and B be complete ReturnAtlas charts over the same arbitrary group H, with positive natural periods d and e and holonomies h and k. Their full signed equality laws are A(t,z)=A(s,w) exactly when t=s+dn and zh^n=w for an integer n, and similarly for B. Atlas periods describe the primitive base return; they need not be the ordinary minimal periods of the lifted time maps. Every statement here concerns sets and specified deck and time maps, with no topology, finiteness, commutativity or torsion assumption on H.

Theorem 1.1 (Unique degree and normalized seed).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall X\in Type,Y\in Type,A\in \mathrm{ReturnAtlas}\left(H,X\right),B\in \mathrm{ReturnAtlas}\left(H,Y\right),f\in \mathrm{Map}\left(X,Y\right),((((\forall a\in H,x\in X,\mathrm{apply}\left(f,\mathrm{deck}\left(A,a,x\right)\right)=\mathrm{deck}\left(B,a,\mathrm{apply}\left(f,x\right)\right))\wedge (\forall x\in X,\mathrm{apply}\left(f,\mathrm{time}\left(A,x\right)\right)=\mathrm{time}\left(B,\mathrm{apply}\left(f,x\right)\right))))⟹(\exists p\in \mathrm{Prod}\left(Nat,\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),H\right)\right),((((\mathrm{Positive}\left(\mathrm{first}\left(p\right)\right))\wedge (((\mathrm{period}\left(A\right)=\mathrm{mul}\left(\mathrm{period}\left(B\right),\mathrm{first}\left(p\right)\right))\wedge (((\mathrm{mul}\left(\mathrm{second}\left(\mathrm{second}\left(p\right)\right),\mathrm{holonomy}{\left(B\right)}^{\mathrm{intCast}\left(\mathrm{first}\left(p\right)\right)}\right)=\mathrm{mul}\left(\mathrm{holonomy}\left(A\right),\mathrm{second}\left(\mathrm{second}\left(p\right)\right)\right))\wedge (\forall t\in Int,z\in H,\mathrm{apply}\left(f,\mathrm{point}\left(A,t,z\right)\right)=\mathrm{point}\left(B,(t+\mathrm{intCast}\left(\mathrm{val}\left(\mathrm{first}\left(\mathrm{second}\left(p\right)\right)\right)\right)),\mathrm{mul}\left(z,\mathrm{second}\left(\mathrm{second}\left(p\right)\right)\right)\right))))))))\wedge (\forall q\in \mathrm{Prod}\left(Nat,\mathrm{Prod}\left(\mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),H\right)\right),((((\mathrm{Positive}\left(\mathrm{first}\left(q\right)\right))\wedge (((\mathrm{period}\left(A\right)=\mathrm{mul}\left(\mathrm{period}\left(B\right),\mathrm{first}\left(q\right)\right))\wedge (((\mathrm{mul}\left(\mathrm{second}\left(\mathrm{second}\left(q\right)\right),\mathrm{holonomy}{\left(B\right)}^{\mathrm{intCast}\left(\mathrm{first}\left(q\right)\right)}\right)=\mathrm{mul}\left(\mathrm{holonomy}\left(A\right),\mathrm{second}\left(\mathrm{second}\left(q\right)\right)\right))\wedge (\forall t\in Int,z\in H,\mathrm{apply}\left(f,\mathrm{point}\left(A,t,z\right)\right)=\mathrm{point}\left(B,(t+\mathrm{intCast}\left(\mathrm{val}\left(\mathrm{first}\left(\mathrm{second}\left(q\right)\right)\right)\right)),\mathrm{mul}\left(z,\mathrm{second}\left(\mathrm{second}\left(q\right)\right)\right)\right))))))))⟹(q=p))))))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.normal_form (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every f:X->Y intertwining all left deck maps and the specified time maps, there is exactly one triple (m,(r,b)) with m a positive natural, r:Fin e and b:H such that d=em, bk^m=hb, and f(A(t,z))=B(t+r.val,zb) for all signed t and all z. The pair (r,b) is exactly the complete normalized coordinate of f(A(0,1)). The period ratio follows from the existing seam obstruction; comparing the seam again at this actual seed gives its own holonomy equation. Reducing a signed source point to complete phase coordinates and transporting holonomy powers then extends the forward law to every negative representative as well. Positivity of e makes m unique, and uniqueness of complete target coordinates makes (r,b) unique.

Definition 1.2 (Transport with the target phase).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall X\in Type,Y\in Type,A\in \mathrm{ReturnAtlas}\left(H,X\right),B\in \mathrm{ReturnAtlas}\left(H,Y\right),\forall r\in \mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),b\in H,x\in X,\mathrm{coveringMap}\left(A,B,r,b,x\right)=\mathrm{apply}\left(\mathrm{iterate}\left(\mathrm{time}\left(B\right),\mathrm{val}\left(r\right)\right),\mathrm{transport}\left(A,B,b,x\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.coveringMap (✓ std3).

Source. Repository-derived.

Commentary.

coveringMap A B r b first applies the existing complete-coordinate transport and then advances target time by r.val. Under d=em and bk^m=hb it sends every A(t,z) to B(t+r.val,zb), including signed t. Indeed bk^(mn)=h^n*b is supplied by SemiconjBy.zpow_right and zpow_mul; this is precisely what makes each source seam respected in the target, without requiring d=e.

Theorem 1.3 (Exact existence with a prescribed seed).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall X\in Type,Y\in Type,A\in \mathrm{ReturnAtlas}\left(H,X\right),B\in \mathrm{ReturnAtlas}\left(H,Y\right),r\in \mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),b\in H,((\exists f\in \mathrm{Map}\left(X,Y\right),((\forall a\in H,x\in X,\mathrm{apply}\left(f,\mathrm{deck}\left(A,a,x\right)\right)=\mathrm{deck}\left(B,a,\mathrm{apply}\left(f,x\right)\right))\wedge (((\forall x\in X,\mathrm{apply}\left(f,\mathrm{time}\left(A,x\right)\right)=\mathrm{time}\left(B,\mathrm{apply}\left(f,x\right)\right))\wedge (\mathrm{apply}\left(f,\mathrm{point}\left(A,0,1\right)\right)=\mathrm{point}\left(B,\mathrm{intCast}\left(\mathrm{val}\left(r\right)\right),b\right))))))⟺(\exists m\in Nat,((\mathrm{Positive}\left(m\right))\wedge (((\mathrm{period}\left(A\right)=\mathrm{mul}\left(\mathrm{period}\left(B\right),m\right))\wedge (\mathrm{mul}\left(b,\mathrm{holonomy}{\left(B\right)}^{\mathrm{intCast}\left(m\right)}\right)=\mathrm{mul}\left(\mathrm{holonomy}\left(A\right),b\right)))))))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.map_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

For each prescribed r:Fin e and b:H, there exists a deck and time intertwiner f with f(A(0,1))=B(r.val,b) if and only if a positive natural m satisfies d=em and bk^m=h*b. Necessity identifies the unique normalized seed in normal_form with the prescribed one. Sufficiency is the actual coveringMap A B r b on the full source carrier. Thus unequal-period maps exist exactly when the target holonomy raised to the period ratio is conjugate to the source holonomy in the displayed order.

Definition 1.4 (The signed fiber map).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall X\in Type,Y\in Type,A\in \mathrm{ReturnAtlas}\left(H,X\right),B\in \mathrm{ReturnAtlas}\left(H,Y\right),f\in \mathrm{Map}\left(X,Y\right),m\in Nat,r\in \mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),b\in H,s\in Int,w\in H,j\in \mathrm{Fin}\left(m\right),((\forall t\in Int,z\in H,\mathrm{apply}\left(f,\mathrm{point}\left(A,t,z\right)\right)=\mathrm{point}\left(B,(t+\mathrm{intCast}\left(\mathrm{val}\left(r\right)\right)),\mathrm{mul}\left(z,b\right)\right))⟹(((\mathrm{apply}\left(\mathrm{fiberEnumeration}\left(A,B,f,m,r,b,s,w\right),j\right):\{x:X\mid \mathrm{apply}\left(f,x\right)=\mathrm{point}\left(B,s,w\right)\})\wedge (\mathrm{val}\left(\mathrm{apply}\left(\mathrm{fiberEnumeration}\left(A,B,f,m,r,b,s,w\right),j\right)\right)=\mathrm{point}\left(A,((s-\mathrm{intCast}\left(\mathrm{val}\left(r\right)\right))+\mathrm{mul}\left(\mathrm{intCast}\left(\mathrm{period}\left(B\right)\right),\mathrm{intCast}\left(\mathrm{val}\left(j\right)\right)\right)),\mathrm{mul}\left(\mathrm{mul}\left(w,\mathrm{holonomy}{\left(B\right)}^{(0-\mathrm{intCast}\left(\mathrm{val}\left(j\right)\right))}\right),\mathrm{inverse}\left(b\right)\right)\right)))))$$

Formalization. D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.fiberEnumeration (✓ std3).

Source. Repository-derived.

Commentary.

For any signed target representative B(s,w), fiberEnumeration sends j:Fin m to A(s-r.val+ej.val,wk^(-(j.val:Int))*b^(-1)), together with a proof that its image under f is B(s,w). This membership uses only the signed normal law: the target seam j cancels the negative power. The application suppresses the proof of that law. The degree ratio and source holonomy constraint enter when proving that this map is bijective.

Theorem 1.5 (Signed reconstruction is injective and exhaustive).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall X\in Type,Y\in Type,A\in \mathrm{ReturnAtlas}\left(H,X\right),B\in \mathrm{ReturnAtlas}\left(H,Y\right),f\in \mathrm{Map}\left(X,Y\right),m\in Nat,r\in \mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),b\in H,s\in Int,w\in H,((((\mathrm{period}\left(A\right)=\mathrm{mul}\left(\mathrm{period}\left(B\right),m\right))\wedge (((\mathrm{mul}\left(b,\mathrm{holonomy}{\left(B\right)}^{\mathrm{intCast}\left(m\right)}\right)=\mathrm{mul}\left(\mathrm{holonomy}\left(A\right),b\right))\wedge (\forall t\in Int,z\in H,\mathrm{apply}\left(f,\mathrm{point}\left(A,t,z\right)\right)=\mathrm{point}\left(B,(t+\mathrm{intCast}\left(\mathrm{val}\left(r\right)\right)),\mathrm{mul}\left(z,b\right)\right))))))⟹(\mathrm{Bijective}\left(\mathrm{fiberEnumeration}\left(A,B,f,m,r,b,s,w\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.fiberEnumeration_bijective (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under d=em, bk^m=h*b and the full signed normal law, the displayed fiberEnumeration is bijective for every integer s and every w:H. Injectivity uses the source seam and the Fin m bounds. Surjectivity reconstructs every source point from the residue of its target seam modulo m, using the signed power relation in its original noncommutative order. Thus every signed target representation enumerates the entire same fiber, not a chosen subfamily.

Definition 1.6 (Every point of every fiber, exactly once).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall X\in Type,Y\in Type,A\in \mathrm{ReturnAtlas}\left(H,X\right),B\in \mathrm{ReturnAtlas}\left(H,Y\right),f\in \mathrm{Map}\left(X,Y\right),m\in Nat,r\in \mathrm{Fin}\left(\mathrm{period}\left(B\right)\right),b\in H,y\in Y,((((\mathrm{period}\left(A\right)=\mathrm{mul}\left(\mathrm{period}\left(B\right),m\right))\wedge (((\mathrm{mul}\left(b,\mathrm{holonomy}{\left(B\right)}^{\mathrm{intCast}\left(m\right)}\right)=\mathrm{mul}\left(\mathrm{holonomy}\left(A\right),b\right))\wedge (\forall t\in Int,z\in H,\mathrm{apply}\left(f,\mathrm{point}\left(A,t,z\right)\right)=\mathrm{point}\left(B,(t+\mathrm{intCast}\left(\mathrm{val}\left(r\right)\right)),\mathrm{mul}\left(z,b\right)\right))))))⟹(((\mathrm{fiberEquiv}\left(A,B,f,m,r,b,y\right):\mathrm{Equiv}\left(\mathrm{Fin}\left(m\right),\{x:X\mid \mathrm{apply}\left(f,x\right)=y\}\right))\wedge (\forall j\in \mathrm{Fin}\left(m\right),\mathrm{val}\left(\mathrm{apply}\left(\mathrm{fiberEquiv}\left(A,B,f,m,r,b,y\right),j\right)\right)=\mathrm{point}\left(A,((\mathrm{intCast}\left(\mathrm{val}\left(\mathrm{first}\left(\mathrm{inverseCoordinates}\left(B,y\right)\right)\right)\right)-\mathrm{intCast}\left(\mathrm{val}\left(r\right)\right))+\mathrm{mul}\left(\mathrm{intCast}\left(\mathrm{period}\left(B\right)\right),\mathrm{intCast}\left(\mathrm{val}\left(j\right)\right)\right)),\mathrm{mul}\left(\mathrm{mul}\left(\mathrm{second}\left(\mathrm{inverseCoordinates}\left(B,y\right)\right),\mathrm{holonomy}{\left(B\right)}^{(0-\mathrm{intCast}\left(\mathrm{val}\left(j\right)\right))}\right),\mathrm{inverse}\left(b\right)\right)\right)))))$$

Formalization. D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.fiberEquiv (✓ std3).

Source. Repository-derived.

Commentary.

Given the degree, seed and signed law furnished by normal_form, fiberEquiv is an actual equivalence Fin m -> {x:X // f(x)=y} for every y:Y. Write (s,w)=B.coordinates.symm(y), where s:Fin e, so y=B(s.val,w). Its forward value at j is A(s.val-r.val+ej.val, wk^(-(j.val:Int))b^(-1)). The displayed application suppresses only the proofs of the ratio, seam and signed law. The inverse is obtained from the proved bijectivity of this explicit enumeration, not from a cardinal equation. Positivity of m follows from d=em and positivity of the atlas periods.

The same enumeration works over any signed representative y=B(s,w): E(j)=A(s-r.val+ej.val,wk^(-(j.val:Int))b^(-1)). Membership is the target seam j. If E(j)=E(l), the source return law forces j.val-l.val=mq. The strict Fin m bounds force q=0 and j=l. Conversely, write an arbitrary preimage as A(t,z). Its image equality gives t+r.val=s+en and (zb)k^n=w for an arbitrary integer n. Euclidean division gives n=j.val+mq even when n is negative. The source seam q and bk^(mq)=h^q*b then show that this original preimage is E(j). The order of w, the negative holonomy power and b inverse is essential.

The joint deck and signed time operations give a transitive H times Z action on each atlas carrier. At the normalized seed, the cyclic return stabilizer generated by the source seam maps into the target return stabilizer by multiplication of its integer parameter by m. Its index is m; the explicit enumeration realizes the corresponding m classes as a full fiber. This links arithmetic divisibility of primitive-base periods to an exact finite-fiber structure without counting the group or the ambient carriers.

For a root that routes a cycle of joint components, applying these positive degree ratios around the cycle makes their product one. Each ratio is therefore one, so each routed map has singleton fibers and is a bijection, and the component holonomies obey the degree-one conjugacy condition. This explains the equal-period transport used in the two-orbit square-root and three-orbit cube-root criteria. It is an interpretation of cyclic stabilizer inclusion and the proved fiber construction, with no claim of literature priority.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.coveringMap
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.fiberEnumeration
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.fiberEnumeration_bijective
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.fiberEquiv
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.map_criterion
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ReturnAtlasFiniteCovers.normal_form
• Dependency: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/TwoOrbitSquareRootCriterion