Equivariant cube roots on three primitive lift orbits

Abstract

The complete original histories over three disjoint primitive base orbits admit precisely local cube roots or a compatible three-cycle.

Definition 1.1 (All original histories over the three signed base orbits).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),P\in \mathrm{Path}\left(C\right),Q\in \mathrm{Path}\left(C\right),S\in \mathrm{Path}\left(C\right),\mathrm{OrbitUnion}\left(C,P,Q,S\right)=\{x:\mathrm{History}\left(\mathrm{expandedGraph}\left(C\right)\right)\mid ((\exists t\in Int,\mathrm{forgetHistory}\left(x\right)=\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,P\right))\vee (((\exists t\in Int,\mathrm{forgetHistory}\left(x\right)=\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,Q\right))\vee (\exists t\in Int,\mathrm{forgetHistory}\left(x\right)=\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,S\right)))))\}$$

Formalization. D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.OrbitUnion (✓ std3).

Source. Repository-derived.

Commentary.

OrbitUnion C P Q S contains every original bilateral legal history of expandedGraph C whose forgotten numbered-edge history is an integer translate of P, Q or S. All phases and group coordinates remain present.

Definition 1.2 (The restricted original time shift).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),P\in \mathrm{Path}\left(C\right),Q\in \mathrm{Path}\left(C\right),S\in \mathrm{Path}\left(C\right),\forall x\in \mathrm{OrbitUnion}\left(C,P,Q,S\right),\mathrm{value}\left(\mathrm{apply}\left(\mathrm{unionShift}\left(C,P,Q,S\right),x\right)\right)=\mathrm{shift}\left(\mathrm{expandedGraph}\left(C\right),\mathrm{value}\left(x\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.unionShift (✓ std3).

Source. Repository-derived.

Commentary.

The time map is exactly the original one-step shift on each underlying history. An integer base phase t becomes t+1.

Definition 1.3 (The original deck action on the full union).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),P\in \mathrm{Path}\left(C\right),Q\in \mathrm{Path}\left(C\right),S\in \mathrm{Path}\left(C\right),\forall a\in H,x\in \mathrm{OrbitUnion}\left(C,P,Q,S\right),\mathrm{value}\left(\mathrm{unionDeck}\left(C,P,Q,S,a,x\right)\right)=\mathrm{groupHistory}\left(C,a,\mathrm{value}\left(x\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.unionDeck (✓ std3).

Source. Repository-derived.

Commentary.

The left action of a is the original groupHistory C a. It preserves the forgotten numbered-edge history. No finiteness or commutativity assumption is imposed on H.

Theorem 1.4 (Complete three-orbit cube-root criterion).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),P\in \mathrm{Path}\left(C\right),Q\in \mathrm{Path}\left(C\right),S\in \mathrm{Path}\left(C\right),d\in Nat,e\in Nat,f\in Nat,((((((\mathrm{Positive}\left(d\right))\wedge (((\mathrm{Positive}\left(e\right))\wedge (\mathrm{Positive}\left(f\right))))))\wedge (((((\mathrm{minimalPeriod}\left(\mathrm{baseShift}\left(C\right),P\right)=d)\wedge (((\mathrm{minimalPeriod}\left(\mathrm{baseShift}\left(C\right),Q\right)=e)\wedge (\mathrm{minimalPeriod}\left(\mathrm{baseShift}\left(C\right),S\right)=f)))))\wedge (((\forall t\in Int,\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,P\right)\ne Q)\wedge (((\forall t\in Int,\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,P\right)\ne S)\wedge (\forall t\in Int,\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,Q\right)\ne S)))))))))⟹(((\exists R\in \mathrm{Map}\left(\mathrm{OrbitUnion}\left(C,P,Q,S\right),\mathrm{OrbitUnion}\left(C,P,Q,S\right)\right),((\forall a\in H,x\in \mathrm{OrbitUnion}\left(C,P,Q,S\right),\mathrm{apply}\left(R,\mathrm{unionDeck}\left(C,P,Q,S,a,x\right)\right)=\mathrm{unionDeck}\left(C,P,Q,S,a,\mathrm{apply}\left(R,x\right)\right))\wedge (\mathrm{iterate}\left(R,3\right)=\mathrm{unionShift}\left(C,P,Q,S\right))))⟺(((((\exists s\in \mathrm{Fin}\left(d\right),m\in Int,b\in H,((\mathrm{Commute}\left(b,\mathrm{orbitHolonomy}\left(C,P,d\right)\right))\wedge (((\mathrm{mul}\left(3,\mathrm{intCast}\left(\mathrm{val}\left(s\right)\right)\right)=1+\mathrm{mul}\left(\mathrm{intCast}\left(d\right),m\right))\wedge (\mathrm{mul}\left(b^3,\mathrm{orbitHolonomy}{\left(C,P,d\right)}^m\right)=1)))))\wedge (((\exists s\in \mathrm{Fin}\left(e\right),m\in Int,b\in H,((\mathrm{Commute}\left(b,\mathrm{orbitHolonomy}\left(C,Q,e\right)\right))\wedge (((\mathrm{mul}\left(3,\mathrm{intCast}\left(\mathrm{val}\left(s\right)\right)\right)=1+\mathrm{mul}\left(\mathrm{intCast}\left(e\right),m\right))\wedge (\mathrm{mul}\left(b^3,\mathrm{orbitHolonomy}{\left(C,Q,e\right)}^m\right)=1)))))\wedge (\exists s\in \mathrm{Fin}\left(f\right),m\in Int,b\in H,((\mathrm{Commute}\left(b,\mathrm{orbitHolonomy}\left(C,S,f\right)\right))\wedge (((\mathrm{mul}\left(3,\mathrm{intCast}\left(\mathrm{val}\left(s\right)\right)\right)=1+\mathrm{mul}\left(\mathrm{intCast}\left(f\right),m\right))\wedge (\mathrm{mul}\left(b^3,\mathrm{orbitHolonomy}{\left(C,S,f\right)}^m\right)=1)))))))))\vee (((d=e)\wedge (((e=f)\wedge (((\exists b\in H,\mathrm{mul}\left(b,\mathrm{orbitHolonomy}\left(C,Q,e\right)\right)=\mathrm{mul}\left(\mathrm{orbitHolonomy}\left(C,P,d\right),b\right))\wedge (\exists b\in H,\mathrm{mul}\left(b,\mathrm{orbitHolonomy}\left(C,S,f\right)\right)=\mathrm{mul}\left(\mathrm{orbitHolonomy}\left(C,Q,e\right),b\right)))))))))))))$$

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

Source. Repository-derived.

Commentary.

Let d,e,f be the positive minimal periods of P,Q,S, whose signed base orbits are pairwise disjoint. A deck-equivariant endomap R of the entire original-history union cubes to the original shift exactly when the three local signed cube-root equations all hold, or d=e=f and consecutive ordered holonomies admit intertwiners bhQ=hPb and chS=hQc. Each local equation has s:Fin d, m:Int and b:H with Commute b h, 3s.val=1+dm and b^3*h^m=1, and independently for the other components. No preservation of components, time commutation or bijectivity is assumed of R.

The three signed base-orbit hypotheses identify the disjoint union of the complete actual lift atlases with this full history subtype. The equivalence keeps the very same underlying numbered-edge history, intertwines every original deck operation and intertwines the original time shift. Conjugating an arbitrary root through it gives precisely the three-chart cube-root problem, rather than a root on selected representatives or a reduced fibre.

The atlas criterion extracts the induced action on three components. A cube root either preserves them all or permutes them in a three-cycle. In the latter case cyclic seam divisibility forces the three primitive periods to be equal, and the ordered seam equations force the displayed conjugacies. Compatible transports then construct a root with one time step on the closing arrow. The order in these group equations is retained; equal holonomy orders or equal ordinary periodic counts are insufficient substitutes. The result concerns these three signed base orbits and does not claim a classification for an arbitrary number of components or literature priority.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.OrbitUnion
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.cube_root_criterion
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.unionDeck
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCriterion.unionShift
• Dependency: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/ThreeOrbitCubeRootCharts
• Dependency: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/TwoOrbitSquareRootCriterion