Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original18.3: fixed block rigidity

Abstract

A fixed disjoint block substitution that also respects unit time is induced by an actual-edge bijection at every position.

Theorem 1.1 (The same code is one-block).

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

Source. Repository-derived.

Commentary.

G and F are finite essential directed multigraphs on the same vertex type V. Parallel edges remain distinct. NatPositive(k) means 0<k. For positive k, f is the actual bijection of legal k-edge words. PreservesBlockEndpoints states equality of source at index 0 and target at index k minus 1 for every word. FixedBlockLaw quantifies every input history x and integer block index j and identifies the output window starting at jk with f of the input window starting at jk. It therefore binds the exact fixed alignment [jk,(j+1)k-1], the exact f and the exact h.

Only the original one-step shift equation is assumed. Integer translations are derived. Two histories sharing their edge at zero can be spliced using one past and the other future. The forward window identifies the output with one history; the shifted last-coordinate window identifies it with the other. Thus the output at zero depends only on the actual input edge. Essentiality realizes every edge, and the inverse block bijection yields the inverse edge map. Boundary-source preservation and adjacency then give both endpoint equations.

The map h is blockHomeomorph(hk,f,endpoints), constructed using integer quotient and remainder at every positive and negative position. Legality is proved inside blocks and at their actual endpoint seams. The inverse uses f inverse on the same aligned blocks, and both maps are continuous because each coordinate reads one finite word. The only dynamical premise is unit-shift commutation of this exact constructed map; no separately assumed history equivalence, continuity or inverse-locality premise is added. No strong connectivity, unique edge between vertices, symmetric window, positive mixing or pre-assumed one-block inverse is required. The k=1 case is included.

Theorem 1.2 (Literal equality of group-ring matrices).

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

Source. Repository-derived.

Commentary.

GroupMat has natural group-ring coefficients. An expanded actual edge is (e,a), where e retains source, target, label and parallel-edge number; its endpoints are (e.source,a) and (e.target,a*e.label). Essentiality of the base graph constructs incoming and outgoing actual edges at every expanded vertex. Vertices retain the same base index and the same group coordinate on both sides.

For each i,j and g, the actual edges from (i,1) to (j,g) are in explicit bijection with Fin(coeff(A[i,j],g)). Restricting the edge bijection from original18_3 to these exact endpoint fibers equates every coefficient with B. Hence A=B as natural group-ring matrices, rather than merely equality of augmentation, spectrum, high powers or unlabeled edge counts. The equal-power attachment constructs the word bijection and ordered-coordinate lift from the explicit premise A^k=B^k, identifies its operational output with blockHomeomorph, and establishes H-equivariance and the k-step law. For finite H and essential base graphs, InertGroupBlockConjugacy.original18_1 derives equal powers from inertness of the actual stationary dimension-group actions of A and B and equal augmentation matrices. Its tau is the least positive uniformizing exponent. For every rational decomposition W and positive n, it proves max(tau(A),tau(B)) <= n*bH(W). For a nontrivial finite group and positive n, it supplies an actual augmentation-first rational decomposition with the original nontrivial matrix orders. Every k at or above the tau threshold has the rational expression and this same equal-power attachment; the trivial-group and zero-size boundaries remain separate. Equivariance is not an additional premise of the endpoint-count theorem.

This excludes the specified fixed nonoverlapping block scheme when A differs from B. It does not exclude overlapping windows, another state presentation or another original-time conjugacy.

Theorem 1.3 (The actual equal-power construction).

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

Source. Repository-derived.

Commentary.

matrixPower is natural matrix exponentiation, iterate is Function.iterate, and equalPowerFiberCounts denotes the proved fiber_counts_of_equal_power proof at A,B,k. For each positive k with the explicit natural matrix equality A^k=B^k, the actual ordered-label word fibers have equal cardinality. Separate finite choices construct the base word map, and the initial group coordinate uniquely determines its ordered lift. The direct quotient-and-remainder output equals equalPowerHomeomorph at every integer coordinate. Left group action and k-step time commute with this same map, and one-step commutation of this map implies A=B. The premise A^k=B^k remains explicit in equalPower_attachment. Under its essentiality, inertness and equal-augmentation hypotheses, InertGroupBlockConjugacy.original18_1 proves the bridge from the actual dimension-group action through the least positive tau to the rational n*bH(W) cutoff and supplies this premise at every admissible exponent. Its attachment uses the exact equalPowerHomeomorph at that exponent; one-step commutation of a different map does not imply the rigidity conclusion.

Theorem 1.4 (Actual initial endpoint).

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

Source. Repository-derived.

Commentary.

For every positive-length base word w and initial group coordinate z, liftWord starts at the actual vertex (wordSource(hk,w),z). This original endpoint supplier is used directly by the twisted-history seam constructor.

Theorem 1.5 (Actual terminal endpoint).

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

Source. Repository-derived.

Commentary.

The same liftWord ends at (wordTarget(hk,w),z*totalLabel(w)). Labels multiply in temporal order on the right of z. This original endpoint supplier is used directly by the twisted-history restriction and seam constructor.

Theorem 1.6 (Original finite word count).

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

Source. Repository-derived.

Commentary.

WordFiber A hk i j g contains actual legal base words with the stated source, target and ordered total label, retaining each parallel-edge number. For every positive length k its cardinality is the g coefficient of the (i,j) entry of A^k. FintypeCard is Fintype.card. The actual twisted-history count consumes this original theorem after transporting finiteness through its reconstruction equivalence.

References