Inert group block conjugacy

Abstract

Actual stationary actions and rational splitting give every original positive-threshold block construction.

Theorem 1.1 (One common annihilation stage).

$\forall R \in T y p e, co mm R in g R \in CommRing (R), M \in T y p e, a dd G ro u pM \in AddCommGroup (M), m o d u l e M \in Module (R, M), I \in T y p e, f ini t e I \in Fintype (I), G amma \in T y p e, f ini t e G amma \in Fintype (G amma), ba s i s \in Basis (I, R, M), T \in ModuleEnd (R, M), P \in Function (G amma, ModuleEnd (R, M)), co mm u t es \in (\forall g \in G amma, Commute (apply (P, g), T)), ((\forall g \in G amma, induced (T, apply (P, g), apply (co mm u t es, g)) = linearIdentity (StationaryModule (T))) \Rightarrow (\exists N \in N a t, \forall g \in G amma, compose (power (T, N), apply (P, g)) = power (T, N))) \land ((\exists N \in N a t, \forall g \in G amma, compose (power (T, N), apply (P, g)) = power (T, N)) \Rightarrow (\forall g \in G amma, induced (T, apply (P, g), apply (co mm u t es, g)) = linearIdentity (StationaryModule (T))))$

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

Source. Repository-derived.

Commentary.

StationaryModule(T) is the actual module direct limit with transition from stage i to stage j equal to T raised to j minus i. The commuting endomorphism P(g) induces the displayed map on this direct limit. Powers of endomorphisms use composition, so the finite-stage equation is T^N composed with P(g) equals T^N.

Equality of two stage-zero classes is witnessed at a later stage by direct-limit exactness. There are finitely many basis vectors and finitely many family members; taking finite maxima gives one N for all of them. Conversely the same finite-stage equation holds after every starting stage, so it forces identity on the entire colimit. The exponent N may be zero, the basis may be empty, and the family need not be a group action.

Theorem 1.2 (Every admissible exponent).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, A \in GroupMat (H, n, n), k \in N a t, (tau (A) \leq finiteWithTop (k) \Rightarrow (NatPositive (k) \land UniformMatrix (matrixPower (A, k)))) \land ((NatPositive (k) \land UniformMatrix (matrixPower (A, k))) \Rightarrow tau (A) \leq finiteWithTop (k))$

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

Source. Repository-derived.

Commentary.

GroupMat(H,n,n) is the matrix semiring over the natural group algebra. UniformMatrix means every actual group coefficient in each entry equals its coefficient at the identity, including zero coefficients. The value tau lies in the natural numbers with a top element: it is the least positive uniform exponent when one exists and infinity otherwise. Ordered convolution preserves uniformity under right multiplication, without assuming the finite group H is commutative.

Theorem 1.3 (The positive convention includes zero).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, A \in GroupMat (H, n, n), (tau (A) = finiteWithTop (1) \Rightarrow UniformMatrix (A)) \land (UniformMatrix (A) \Rightarrow tau (A) = finiteWithTop (1))$

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

Source. Repository-derived.

Commentary.

The equivalence includes the zero matrix, whose least positive exponent is one even though its zeroth power behaves differently. If H is trivial, every entry is uniform and every matrix has tau one. It also includes n=0; no positivity of the matrix order is needed for the natural threshold theorem.

Theorem 1.4 (Equal augmentation gives equal natural powers).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, A \in GroupMat (H, n, n), B \in GroupMat (H, n, n), s am e A ug m e n t a t i o n \in matrixAugmentation (A) = matrixAugmentation (B), k \in N a t, t h res h o l d \in max (tau (A), tau (B)) \leq finiteWithTop (k), NatPositive (k) \land matrixPower (A, k) = matrixPower (B, k)$

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

Source. Repository-derived.

Commentary.

Augmentation sums the actual natural coefficients entry by entry and is a ring homomorphism. At every k at least both tau values, both powers are uniform. A uniform natural entry is determined by its augmentation because its coefficient sum is |H| times any coefficient and |H| is positive. Thus A^k=B^k in the original natural group-matrix semiring. Positivity of k is a conclusion; k=1 is retained.

Theorem 1.5 (The exact kernel of the nontrivial tail).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), S \in T y p e, r in g S \in Ring (S), a l g e b r a S \in Algebra (R a t, S), p hi \in AlgEquiv (R a t, MonoidAlgebra (R a t, H), Product (R a t, S)), a ug m e n t a t i o n F i rs t \in (\forall z \in MonoidAlgebra (R a t, H), first (apply (p hi, z)) = augmentation (z)), x \in MonoidAlgebra (R a t, H), (UniformRational (x) \Rightarrow second (apply (p hi, x)) = 0) \land (second (apply (p hi, x)) = 0 \Rightarrow UniformRational (x))$

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

Source. Repository-derived.

Commentary.

UniformRational means equality of every coefficient with the identity coefficient. Augmentation is their rational sum. The normalized element average(H), denoted e_H, has every coefficient 1/|H|. The theorem applies to any actual rational algebra equivalence phi whose first coordinate is literally augmentation; S may be noncommutative. A uniform element satisfies x*y=augmentation(y) times x. Conversely, vanishing tail makes every left group translation fix x and hence makes every coefficient equal.

Theorem 1.6 (All nontrivial rational simple factors).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n o n t r i v ia l H \in Nontrivial (H), Nonempty (RationalDecomposition (H))$

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

Source. Repository-derived.

Commentary.

RationalDecomposition(H) consists of a positive count m, a division algebra D_l over the rationals of finite rational dimension for each l in Fin(m), positive natural matrix orders r_l, and an actual rational algebra equivalence Q[H] with Q times the product of Mat(r_l,D_l). Its first coordinate equals augmentation on every element. No complex splitting or change of coefficient field occurs.

Uniform elements form a two-sided ideal J. The map x to (augmentation(x),[x]) is bijective: its kernel is zero because a uniform augmentation-zero element is zero, and a preimage of (a,[x]) is x+(a-augmentation(x))*e_H. For nontrivial H the quotient Q[H]/J is nontrivial. Maschke supplies semisimplicity and the finite rational Wedderburn theorem supplies the division-ring factors of this quotient. The quotient’s nontriviality makes the factor count positive; no empty maximum is assigned to a trivial group.

Theorem 1.7 (The exact normalized expression).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), x \in MonoidAlgebra (R a t, H), u ni f or m \in UniformRational (x), x = scalarMultiply (augmentation (x), average (H))$

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

Source. Repository-derived.

Commentary.

Every uniform rational element is its actual augmentation times e_H. This includes zero and preserves the factor 1/|H| exactly.

Theorem 1.8 (Actual uniformity and faithful blocks).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, W \in RationalDecomposition (H), C \in GroupMat (H, n, n), (UniformMatrix (C) \Rightarrow (\forall l \in Fin (count (W)), block (W, l, C) = 0)) \land ((\forall l \in Fin (count (W)), block (W, l, C) = 0) \Rightarrow UniformMatrix (C))$

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

Source. Repository-derived.

Commentary.

W is an actual augmentation-first rational decomposition with positive factor count, positive matrix orders r_l and finite rational division algebras D_l. The map block(W,l,C) casts natural coefficients to rational coefficients, applies the l-th tail factor entrywise, then flattens Mat(n,Mat(r_l,D_l)) to Mat(Fin(n) times Fin(r_l),D_l). Faithfulness and augmentation-firstness identify its simultaneous zero kernel with uniform coefficients. This is a theorem about every C, not an assumed bridge for selected powers.

Theorem 1.9 (The exact bound n*b_H).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, W \in RationalDecomposition (H), p os i t i v e N \in NatPositive (n), A \in GroupMat (H, n, n), u ni f or mi zes \in Uniformizes (A), tau (A) \leq finiteWithTop (multiply (n, bH (W)))$

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

Source. Repository-derived.

Commentary.

The natural number bH(W) is the maximum of W’s original nontrivial rational matrix orders r_l. A positive uniform power makes every tail block nilpotent. Right multiplication on row vectors is linear over the same division ring and reverses products, but preserves powers of one matrix. Kernel stabilization therefore kills an nr_l dimensional block by exponent nr_l, and hence all blocks vanish by n*bH(W).

The dimension is measured over D_l, not over the rationals; there is no factor dim_Q(D_l). The hypotheses n>0, positive factor count and positive r_l ensure that n*bH(W) is a positive exponent, as required by the least-positive convention. The trivial group uses the separate tau=1 boundary and has no artificial b_H.

Theorem 1.10 (Rational expression of a natural uniform matrix).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, C \in GroupMat (H, n, n), u ni f or m \in UniformMatrix (C), i \in Fin (n), j \in Fin (n), rationalEntry (C, i, j) = scalarMultiply (castRat (augmentationEntry (C, i, j)), average (H))$

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

Source. Repository-derived.

Commentary.

rationalEntry(C,i,j) is the natural entry C[i,j] with its coefficients cast to the rationals; augmentationEntry is the natural augmentation entry. The equality is entrywise equality in Q[H]. It divides only after casting to the rationals and does not assert divisibility by introducing an operation in the natural semiring.

Theorem 1.11 (Ordered vertex coordinates).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, A \in GroupMat (H, n, n), i \in Fin (n), j \in Fin (n), h \in H, t \in H, coefficient (vertexCoordinate (apply (transition (A), vertex (i, h)), j), t) = castInt (coefficient (entry (A, i, j), multiply (inverse (h), t)))$

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

Source. Repository-derived.

Commentary.

VertexModule is Fin(n) to Z[H], the free abelian group on vertices (i,h). The vector vertex(i,h) has coefficient one at that vertex and zero elsewhere. The transition sends a row vector v to v times the coefficientwise integer cast of A. The displayed coefficient is exactly the number of actual expanded edges from (i,h) to (j,t): an edge labelled s ends at h*s, so s=h inverse times t. The order is retained for noncommutative H.

Theorem 1.12 (Identity on the actual stationary group).

$\forall H \in T y p e, g ro u p H \in Group (H), f ini t eH \in Fintype (H), n \in N a t, A \in GroupMat (H, n, n), (Inert (A) \Rightarrow Uniformizes (A)) \land (Uniformizes (A) \Rightarrow Inert (A))$

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

Source. Repository-derived.

Commentary.

DimensionGroup(A) is the actual stationary module colimit of this integer transition. The original left H-action sends each vertex (i,h) to (i,g*h), commutes with adjacency, and therefore induces groupAction(A,g) on that colimit. Inert(A) means groupAction(A,g) equals the identity for every g; uniformization is not part of this definition. Uniformizes(A) means that some positive natural exponent has all actual group coefficients constant in each matrix entry.

The finite vertex basis and finite group give a common stage N at which T_A^N composed with every left translation equals T_A^N. Reading basis coefficients equates every coefficient of A^N; conversely uniform coefficients imply those stage equations on the basis. Advancing from N to N+1 supplies a positive exponent even when the common stage was zero. Inertness is identity on the underlying stationary group; the argument does not require a separately constructed ordered-group API or an order-unit normalization.

Theorem 1.13 (The full threshold and unchanged construction).

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

Source. Repository-derived.

Commentary.

A and B are natural group-ring matrices with the same actual augmentation matrix. Their finite base graphs are essential, and their original left H-actions are inert on the stationary dimension groups of the actual integer free-expansion adjacencies. NatPositive means strictly positive. The displayed equalPowerFiberCounts denotes the existing fiber_counts_of_equal_power proof on the same A, B, hk and hpower. Tau is the least positive uniform exponent, or infinity if no such exponent exists. The displayed existential proofs hk and hpower express conclusions 0<k and A^k=B^k; neither is an additional premise.

The final conjunct supplies an actual single decomposition W when H is nontrivial and n is positive. Its own original block orders give the displayed cutoff, and this same W controls the constructed map for every k at least that cutoff. No decomposition or cutoff is an extra premise. The preceding clauses still cover every supplied W and every k at least max tau, including smaller admissible exponents. For nontrivial H, an augmentation-first RationalDecomposition is supplied by the rational splitting theorem. The cutoff clause holds for every such decomposition W and every positive n. It retains W’s original nontrivial rational block orders r_l, with bH(W)=max_l r_l, giving max(tau(A),tau(B)) at most nbH(W). Therefore every k at least nbH(W) satisfies the final clause, while all smaller k at least the original max-tau threshold remain included. For trivial H both tau values are one and equal augmentation already gives A=B. Zero matrices have tau one by the positive convention; no empty b_H is assigned.

The rational equations are equalities in Q[H] at each entry: both A^k and B^k equal the corresponding entry of the k-th power of their common augmentation matrix times e_H, whose actual coefficients are 1/|H|. The equality A^k=B^k itself is in the natural group-matrix semiring. No commutativity of H or replacement by complex irreducible degrees is used.

For each admissible k, the exact equalPowerHomeomorph uses the existing ordered-label fiber bijections and the same fixed nonoverlapping integer blocks [jk,(j+1)k-1]. Operational equality identifies original181History with this homeomorphism; the next equations give the original left H-equivariance and the k-step shift law for this same map. Positive and negative positions use the same quotient-and-remainder construction, and k=1 is included. Different k may give different maps.

If this exact fixed-block map also commutes with the original one-step shift, essentiality and fixed-block rigidity force A=B. The conclusion does not forbid other overlapping codes, other state presentations or other original-time conjugacies. No unit-time conjugacy is claimed from inertness alone.

References

Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.actual_expansion_adjacency
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.equal_power_of_tau_le
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.finite_family_inert_iff_eventual
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.inert_iff_uniformizes
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.nonempty_decomposition
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.original18_1
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.tau_eq_one_iff_uniform
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.tau_le_cutoff
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.tau_le_iff_uniform_power
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.uniform_eq_augmentation_smul_average
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.uniform_iff_blocks_zero
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.uniform_iff_tail_zero
Truth anchor: D5/S3/ConceptDynamics/Coding/InertGroupBlockConjugacy.uniform_rational_expression
Dependency: D5/S3/ConceptDynamics/Coding/CountedGroupOverlap
Dependency: D5/S3/ConceptDynamics/Coding/FixedBlockRigidity

Keyboard shortcuts

trureturing — Discovering truth

Inert group block conjugacy

Abstract

References