Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original dynamics and cyclic arithmetic

Abstract

Finite alternating subgroups and their simultaneous finite-support product in the original Reset kernel.

Theorem 1.1 (Original full-rho commutation).

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

Source. Repository-derived.

Commentary.

This existing owning argument applies the actual representation to the literal fullAutSubgroup shift-commutation law and uses rho_unitShift. It is public for ResetNativeUnitNormalForm’s complete original-rho consumer.

Theorem 1.2 (The consumed general scalar argument).

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

Source. Repository-derived.

Commentary.

commutesWithForwardTime(q,A) means forall x, A(resetTheta(q,x))=resetTheta(q,A(x)). centralizingMap transports A by nativeIntEquiv and promotes it to Int[X]-linearity with LinearMap.ofAEval. Polynomial-quotient surjectivity gives the scalar law. The original chartMap and chartMap_scalar specialize this same owning argument to actual rho. ResetNativeUnitNormalForm consumes it for both A and its inverse. This generalized helper supplies no new component-unit classification.

The original rho acts on DimensionGroup(resetMatrix q) by actual beam pushforward. Every full history automorphism commutes with UNIT shift; rho_unitShift identifies its native image with forward resetTheta. nativePolynomialEquiv then makes the transported image polynomial-linear on QF=Z[X]/(F q). Its value at 1 determines it as multiplication by that value, so actual image maps commute. No ring is installed on Native.

The live nonbinding input is MarkerPermutationAction’s faithful guarded action on ALL original Reset histories. Its marker and eligibility invariance are indispensable to the inverse and group law. Reindexing, cyclicity, centralizer commutativity and commutator transport are consumed library applications, not separate mathematical contributions. The classical marker method is attributed in the owning MarkerPermutationAction Scribe and the Boyle–Lind–Rudolph library note.

Definition 1.3 (The prescribed finite symmetric group action).

Formalization. D5/S3/ConceptDynamics/Coding/ResetHistoryKernel.symmetricAction (✓ std3).

Source. Repository-derived.

Commentary.

Fin(2^k) is reindexed by the existing cardinal equivalence with Fin k→Bool. This transports the actual resetAction without changing any graph, history, shift, topology or representation. Its radius is 12k+5.

Definition 1.4 (Alternating permutations land in the actual kernel).

Formalization. D5/S3/ConceptDynamics/Coding/ResetHistoryKernel.alternatingKernelEmbedding (✓ std3).

Source. Repository-derived.

Commentary.

The hom restricts symmetricAction and codRestricts to (rho q hq0).ker. Every three-cycle is conjugate to its square in Sym, hence a commutator by mem_commutatorSet_of_isConj_sq. closure_three_cycles_eq_alternating and abelian rho image kill the entire alternating group. This includes k=2 and A4; it does not assume A4 perfect or use a cardinal>=5 theorem.

Theorem 1.5 (Uniform original-kernel injectivity).

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

Source. Repository-derived.

Commentary.

The injectivity is inherited from the genuine original-history action, whose guarded words are realized by existing positive-word extension. hq0 can be any proof of 0<q, which follows from q>=2. For k>=2 the alternating groups are nonabelian, including A4, and their factorial orders are unbounded as k grows. No cross-k compatibility, complete kernel classification or locally finite whole-kernel conclusion is claimed.

Definition 1.6 (A countable product with finite support).

Formalization. D5/S3/ConceptDynamics/Coding/ResetHistoryKernel.FiniteGapAlternating (✓ std3).

Source. Repository-derived.

Commentary.

This is Mathlib RestrictedProduct with n-th fiber Alt(Fin(2^(n+2))), bottom subgroups, and Filter.cofinite. A tuple has finitely many nonidentity coordinates, multiplied coordinatewise in their original noncommutative groups. The coordinate n=0 is A4.

Definition 1.7 (Simultaneous action in the original kernel).

Formalization. D5/S3/ConceptDynamics/Coding/ResetHistoryKernel.gapProductKernelEmbedding (✓ std3).

Source. Repository-derived.

Commentary.

Use the actual signed edge b: (0,zeta)→(0,1), and a: (0,1)→(0,zeta). With c_h the chain 0→1 and d_h the reset from 1, U=a c_zeta d_zeta and V=c_one d_one c_zeta d_zeta are b-free loops at (0,1), of lengths 3 and 4. A bit is U^4 or V^3. Concatenating n+2 blocks and closing with a gives d(n)=12(n+2)+1 edges from target(b) to source(b). The first edges of the two blocks differ, so the codes are injective. All edges are transported through originalEdge with their actual labels, numbers and absolute signs. The chain requires q>=2.

Theorem 1.8 (Joint faithfulness on all original histories).

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

Source. Repository-derived.

Commentary.

SeparatorGapAction proves that overlapping interiors between consecutive b edges have the same endpoints. It proves exact separator preservation, both directions of eligibility invariance, and cross-length commutation on arbitrary bilateral sequences. The legal seams use the distinct source and target of b. Its finite-support homomorphism acts on ALL History(ResetGraph q), commutes with the actual unit shift and has a real continuous inverse. On a realized word b D(n,i) b, every other length fixes the central data while coordinate n outputs D(n,g(n)(i)); this determines every coordinate of the tuple. Noncoded gaps, extra q>2 edges and arbitrary exterior tails are included. The original rho has commuting images by the cyclic integer chart. Alternating factors are killed as restrictions of these new symmetric actions, using three-cycle commutators in Sym, including A4. Subgroup closure places the finite product in the SAME rho kernel. The classical marker method is discussed in Library/FiniteGroups/boylelindrudolph1988automorphism.md. There is no q=1 claim, unrestricted infinite-product continuity, publication novelty claim or classification of the whole kernel.

References