Counted group chain recovery windows

Abstract

One finite matrix chain constructs one equivariant homeomorphism carrying both edge windows and both group-coordinate windows. The transfer is read from that same code.

Theorem 1.1 (Construct one code with four recovery budgets).

$$\forall H\in Type,group\in \mathrm{Group}\left(H\right),finite\in \mathrm{Fintype}\left(H\right),topology\in \mathrm{TopologicalSpace}\left(H\right),continuousGroup\in \mathrm{IsTopologicalGroup}\left(H\right),a\in Nat,b\in Nat,L\in Nat,A\in \mathrm{GroupMat}\left(H,a,a\right),B\in \mathrm{GroupMat}\left(H,b,b\right),ch\in \mathrm{ExchangeChain}\left(\mathrm{MonoidAlgebra}\left(Nat,H\right),A,B,L\right),\mathrm{Nonempty}\left(\mathrm{WindowGroupConjugacy}\left(A,B,L\right)\right)$$

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

Source. Repository-derived.

Commentary.

The elementary map is built from counted group-labelled edge fibers. Its forward edge uses the present and next input, its inverse uses the preceding and present output. The group transfers use the first split label and the preceding inverse split label. Composition adds all four budgets, and induction handles every intermediate matrix dimension.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/CountedGroupWindowChain.chain_has_window_group_conjugacy
• Dependency: D5/S3/ConceptDynamics/Coding/CountedGroupOverlap