The involution factorization as an exact exchange

Abstract

An involution supplies explicit nonnegative factors and an exact one-step exchange chain with a proved lower bound.

Theorem 1.1 (Natural coefficients satisfy both products).

$$\forall H\in Type,group\in \mathrm{Group}\left(H\right),finite\in \mathrm{Fintype}\left(H\right),s\in H,t\in H,hs\in \mathrm{product}\left(s,s\right)=1,\mathrm{product}\left(\mathrm{toNat}\left(\mathrm{leftFactor}\left(s,t\right)\right),\mathrm{toNat}\left(\mathrm{rightFactor}\left(s\right)\right)\right)=\mathrm{sourceNat}\left(s,t\right)\wedge \mathrm{product}\left(\mathrm{toNat}\left(\mathrm{rightFactor}\left(s\right)\right),\mathrm{toNat}\left(\mathrm{leftFactor}\left(s,t\right)\right)\right)=\mathrm{targetNat}\left(H\right)$$

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

Source. Repository-derived.

Commentary.

Nonnegative integer factors are converted coefficientwise to natural coefficients. Lifting back is injective, so the two actual products equal the original source and target formulas.

Theorem 1.2 (The chain cannot have length zero).

$$\forall H\in Type,group\in \mathrm{Group}\left(H\right),finite\in \mathrm{Fintype}\left(H\right),s\in H,t\in H,hs\in \mathrm{product}\left(s,s\right)=1,hst\in \left(\neg \mathrm{product}\left(s,t\right)=\mathrm{product}\left(t,s\right)\right),\mathrm{ExchangeChain}\left(\mathrm{MonoidAlgebra}\left(Nat,H\right),\mathrm{sourceMatrix}\left(s,t\right),\mathrm{targetMatrix}\left(H\right),1\right)\wedge \left(\neg \mathrm{ExchangeChain}\left(\mathrm{MonoidAlgebra}\left(Nat,H\right),\mathrm{sourceMatrix}\left(s,t\right),\mathrm{targetMatrix}\left(H\right),0\right)\right)$$

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

Source. Repository-derived.

Commentary.

Noncommuting elements make the source and target coefficients different. A zero-length exchange chain has equal endpoints, while the explicit factors already give a length-one chain.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/InvolutionCountedConjugacy.involution_minimum_one
• Truth anchor: D5/S3/ConceptDynamics/Coding/InvolutionCountedConjugacy.natural_factor_products
• Dependency: D5/S3/ConceptDynamics/Coding/CountedGroupOverlap
• Dependency: D5/S3/ConceptDynamics/Coding/InvolutionUniformExchange