Twisted periods from finite seamed words

Abstract

Every positive twisted period is an actual legal bilateral history reconstructed from one finite numbered word and its ordered group seam.

Theorem 1.1 (The return law at every signed block address).

$$\forall H\in Type,[\mathrm{Group}\left(H\right)]\forall n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),h\in H,j\in Nat,x\in \mathrm{TwistedPeriod}\left(C,h,j\right),q\in Int,t\in Int,\mathrm{historyAt}\left(x,\mathrm{add}\left(t,\mathrm{mul}\left(q,j\right)\right)\right)=\mathrm{pair}\left(\mathrm{baseEdge}\left(\mathrm{historyAt}\left(x,t\right)\right),\mathrm{mul}\left(h^q,\mathrm{groupCoordinate}\left(\mathrm{historyAt}\left(x,t\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.signed_recovery (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any actual twisted history and any integers q and t, the edge at t+q*j has the same original numbered base edge as at t, and its group coordinate is h^q times the coordinate at t. No positivity or finiteness premise is needed. The commuting translation and left-group permutations turn the given one-block equation into its signed powers. This same return law supplies the actual primitive-lift chart and its noncommutative seam relation.

Definition 1.2 (Restriction and signed extension are inverse).

$$\forall H\in Type,group\in \mathrm{Group}\left(H\right),finiteH\in \mathrm{Fintype}\left(H\right),n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),h\in H,j\in Nat,hj\in \mathrm{NatPositive}\left(j\right),\mathrm{Equiv}\left(\mathrm{TwistedPeriod}\left(C,h,j\right),\mathrm{SeamWords}\left(C,h,hj\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.twistedPeriodEquiv (✓ std3).

Source. Repository-derived.

Commentary.

NatPositive(j) means 0<j. TwistedPeriod(C,h,j) is the subtype of actual History(expandedGraph C) satisfying shift iterated j times of x equals groupHistory(C,h,x). SeamWords(C,h,hj) is Sigma i:Fin n, Sigma z:H, WordFiber C hj i i (z inverse times h times z). WordFiber retains every original edge and parallel-edge number, both endpoints and the ordered total label. The bridge requires no essentiality, inertness, assumed history equivalence or assumed finiteness of histories. The zero-vertex case is included naturally as an empty sigma; no period-zero assertion is made.

Restriction reads the actual length-j window at zero and its initial coordinate z. The original expandedWordCoordinates inverse recovers this window as liftWord(w,z). Last-edge legality and the twist at zero give equal base endpoints and ztotalLabel(w)=hz, hence totalLabel(w)=z inversehz in this order.

For every integer address t=assemble j(q,r), extension uses the exact numbered edge (w.edge r, h^q*(zprefixLabel w r)). Internal legality is supplied by liftWord. At each seam, the original lift_source and lift_target endpoint equations and ztotalLabel(w)=h*z join adjacent blocks. Euclidean blockAddress and both assemble inverse identities cover all negative as well as positive positions. The twist is proved on every integer coordinate. Signed recovery of an arbitrary twisted history uses the commuting translation and left-group permutations, Function.IsFixedPt.perm_zpow and Commute.mul_zpow. Thus restriction followed by extension recovers every coordinate, and extension followed by restriction recovers the same dependent finite word data. No generic signed-action induction or duplicated finite-word coordinate proof is added.

Definition 1.3 (Actual finite enumeration).

$$\forall H\in Type,group\in \mathrm{Group}\left(H\right),finiteH\in \mathrm{Fintype}\left(H\right),n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),h\in H,j\in Nat,hj\in \mathrm{NatPositive}\left(j\right),\mathrm{Fintype}\left(\mathrm{TwistedPeriod}\left(C,h,j\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.twistedPeriodFintype (✓ std3).

Source. Repository-derived.

Commentary.

The positive-length argument is supplied explicitly. Fintype.ofEquiv transports the finite dependent sigma enumeration through twistedPeriodEquiv inverse. Consequently the actual twisted-history subtype is Finite. No global finiteness instance for unrestricted History is assumed.

Theorem 1.4 (Exact diagonal conjugacy sum).

$$\forall H\in Type,group\in \mathrm{Group}\left(H\right),finiteH\in \mathrm{Fintype}\left(H\right),n\in Nat,C\in \mathrm{GroupMat}\left(H,n,n\right),h\in H,j\in Nat,hj\in \mathrm{NatPositive}\left(j\right),\mathrm{FintypeCard}\left(\mathrm{TwistedPeriod}\left(C,h,j\right)\right)=\mathrm{sumFin}\left(n,i,\mathrm{sumGroup}\left(H,z,\mathrm{coeff}\left(\mathrm{entry}\left(\mathrm{matrixPower}\left(C,j\right),i,i\right),\mathrm{product}\left(\mathrm{product}\left(\mathrm{inverse}\left(z\right),h\right),z\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.twistedPeriod_card (✓ std3). ∎

Source. Repository-derived.

Commentary.

FintypeCard uses the constructed twistedPeriodFintype. sumFin and sumGroup sum over every i:Fin n and z:H. MatrixPower is the same natural group-ring matrix power C^j. The proof uses the actual reconstruction equivalence on its live path, expands the two sigma cardinalities and directly applies FixedBlockRigidity.wordFiber_card to each loop fiber. It counts actual bilateral histories, including parallel edges, rather than substituting a coefficient-only proxy. This supplies the bridge for the original18.4 example; the literal D8 coefficients, period-one cancellation, all positive counts16^j and arbitrary original coprime block-map iterate laws remain separate obligations.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.signed_recovery
• Truth anchor: D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.twistedPeriodEquiv
• Truth anchor: D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.twistedPeriodFintype
• Truth anchor: D5/S3/ConceptDynamics/Coding/TwistedPeriodicHistories.twistedPeriod_card
• Dependency: D5/S3/ConceptDynamics/Coding/FixedBlockRigidity