Square roots on two full actual lift orbits

Abstract

Two primitive base orbits can jointly admit an equivariant square root even when separate roots fail.

Definition 1.1 (All original histories over both 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),\mathrm{OrbitUnion}\left(C,P,Q\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)))\}$$

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

Source. Repository-derived.

Commentary.

OrbitUnion C P Q is the subtype of every original bilateral legal history of expandedGraph C whose forgotten numbered-edge base history is translate(t,P) or translate(t,Q) for an integer t. The two alternatives retain all group coordinates and all original numbered edges. Neither a representative lift nor a selected subset of a fibre replaces this carrier.

Definition 1.2 (The original time map restricted to the 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),\forall x\in \mathrm{OrbitUnion}\left(C,P,Q\right),\mathrm{value}\left(\mathrm{apply}\left(\mathrm{unionShift}\left(C,P,Q\right),x\right)\right)=\mathrm{shift}\left(\mathrm{expandedGraph}\left(C\right),\mathrm{value}\left(x\right)\right)$$

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

Source. Repository-derived.

Commentary.

unionShift has exactly the original one-step history shift as its underlying value. Signed base orbit membership is invariant under this operation: a base translate by t becomes the translate by t+1.

Definition 1.3 (The original left deck action restricted to the 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),\forall a\in H,x\in \mathrm{OrbitUnion}\left(C,P,Q\right),\mathrm{value}\left(\mathrm{unionDeck}\left(C,P,Q,a,x\right)\right)=\mathrm{groupHistory}\left(C,a,\mathrm{value}\left(x\right)\right)$$

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

Source. Repository-derived.

Commentary.

unionDeck a acts by the original groupHistory C a. It leaves the forgotten base path, including every edge number, unchanged. The group is arbitrary and can be infinite or noncommutative.

Theorem 1.4 (Complete square-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),d\in Nat,e\in Nat,((((((\mathrm{Positive}\left(d\right))\wedge (\mathrm{Positive}\left(e\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 (\forall t\in Int,\mathrm{translate}\left(\mathrm{baseGraph}\left(C\right),t,P\right)\ne Q)))))⟹(((\exists R\in \mathrm{Map}\left(\mathrm{OrbitUnion}\left(C,P,Q\right),\mathrm{OrbitUnion}\left(C,P,Q\right)\right),((\forall a\in H,x\in \mathrm{OrbitUnion}\left(C,P,Q\right),\mathrm{apply}\left(R,\mathrm{unionDeck}\left(C,P,Q,a,x\right)\right)=\mathrm{unionDeck}\left(C,P,Q,a,\mathrm{apply}\left(R,x\right)\right))\wedge (\mathrm{iterate}\left(R,2\right)=\mathrm{unionShift}\left(C,P,Q\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(2,\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^2,\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(2,\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^2,\mathrm{orbitHolonomy}{\left(C,Q,e\right)}^m\right)=1)))))))\vee (((d=e)\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)))))))))$$

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

Source. Repository-derived.

Commentary.

Let d and e be the positive minimal periods of P and Q, and suppose no signed translate of P equals Q. Put h=orbitHolonomy C P d and k=orbitHolonomy C Q e. An arbitrary deck-equivariant endomap R of the entire original-history union has R squared equal to the original shift exactly in the displayed two cases. The preserving case requires both signed local equations: there are s:Fin d, m:Int and b:H with Commute b h, 2s.val=1+dm and b^2h^m=1, and independently the same conditions for Q,e,k. The exchanging case requires d=e and an intertwiner bk=h*b. Holonomy order or equality of ordinary periodic counts cannot replace the displayed holonomy condition. No time-commutation, bijectivity or component-preservation premise is imposed on R.

For the reverse direction, the root equation first gives time commutation. Complete finite phase coordinates then show that the image tag of R is constant on each joint deck/time component. Applying the square equation to the two origins forces the tag map to be either the identity or the exchange. In the identity case the existing one-orbit root criterion gives the two local equations. In the exchange case each directed cross map carries the source seam into the target seam, giving d=em and e=dn for integers m,n. Positivity forces d=e and m=n=1, so the first seam becomes bk=hb. This uses both directions of transport; equal infinite cardinalities would not determine the primitive periods.

For the converse exchange, complete atlas coordinates define F(point(t,z))=point(t,zb) on the other component. Source equality at a signed seam m is respected because SemiconjBy.zpow_right directly gives bk^m=h^m*b for every integer m. The inverse transport uses b inverse. Sending the first component through F and the second through time composed with F inverse squares to time on both. The complete charts are identified with the full original union by an equivalence whose underlying map is the same numbered-edge history; it intertwines original time and every original deck operation. Thus the construction neither omits histories nor adds artificial ones.

The argument combines classical permutation-centralizer component routing, regular-action right multiplication and ordered voltage-return holonomy. The one-orbit arithmetic is supplied by PrimitiveLiftRootCriterion; the signed power identity is supplied by pinned Mathlib SemiconjBy.zpow_right. This is a synthesis on actual history carriers and makes no claim of literature priority or global classification beyond these two signed base orbits.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/TwoOrbitSquareRootCriterion.OrbitUnion
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/TwoOrbitSquareRootCriterion.square_root_criterion
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/TwoOrbitSquareRootCriterion.unionDeck
• Truth anchor: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/TwoOrbitSquareRootCriterion.unionShift
• Dependency: D5/S3/ConceptDynamics/Coding/PrimitiveLifts/PrimitiveLiftRootCriterion