Alternating reset histories and whole rays

Abstract

Alternating numbered reset squares yield finite-window tables and a disjoint same-cut decomposition of whole past rays.

NatPositive(q) means 0 < q. Sign is Multiplicative Bool with XOR addition. Matrix means resetMatrix q, Graph means expandedGraph Matrix, and Histories means History Graph with the native product and subtype topologies. The boundary matrix is literally the identity matrix plus Matrix, over the same natural Boolean group algebra. All edge numbers and absolute group coordinates are retained.

The names resetNumberedData, resetFiniteForgetting and resetExpandedEssential denote Alternating.resetNumberedData, Alternating.resetFiniteForgetting and Alternating.reset_expanded_essential in the ResetNumberedHistories namespace. resetAlternatingTablesLocal denotes reset_alternating_tables_local. The other displayed reset names are the same public names in that namespace.

Definition 1.1 (Uniform alternating table pair on the actual reset graph).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),\mathrm{TablePair}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),0,q,q,0\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetAlternatingTablePair (✓ std3).

Source. Repository-derived.

Commentary.

For every positive q the definition returns TablePair Graph Graph 0 q q 0. Its forward and backward tables read q+1 original numbered edges. The D, F and legal A boundary constructors distinguish identity, reset and advance; the guarded FD/AF squares preserve the endpoints.

Theorem 1.2 (Even positive q gives the local criterion).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),he\in \mathrm{Even}\left(q\right),\mathrm{LocalCriterion}\left(\mathrm{resetAlternatingTablePair}\left(q,hq\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every positive even q, the criterion gives both seams on legal q+2-edge words and both center roundtrips on legal 2q+1-edge words. The left and right comparison ranks contract along their respective sweeps; overlapping strips identify the windows and recover the original center edge.

Definition 1.3 (Squares on the actual numbered additive boundary).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),\mathrm{resetNumberedData}\left(q,hq\right):\mathrm{NumberedData}\left(\mathrm{resetMatrix}\left(q\right),\mathrm{resetMatrix}\left(q\right),\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetNumberedData (✓ std3).

Source. Repository-derived.

Commentary.

The local square interface uses Edge(identityMatrix + resetMatrix) times Sign as its boundary type. Its source and target are the original expanded boundary endpoints. The two summands occupy disjoint coefficient-number intervals; labels, numbers and absolute signs determine the boundary equivalence.

Definition 1.4 (Forgetting after q squares).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),he\in \mathrm{Even}\left(q\right),\mathrm{resetFiniteForgetting}\left(q,hq,he\right):\mathrm{FiniteForgetting}\left(\mathrm{squares}\left(\mathrm{resetNumberedData}\left(q,hq\right)\right),q\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetFiniteForgetting (✓ std3).

Source. Repository-derived.

Commentary.

FiniteForgetting is the existing positive-length, left and right forgetting proposition on unrestricted natural-indexed square strips. Equality of the left input strips forces the initial boundaries to coincide after q squares; equality of the right input strips forces the terminal boundaries to coincide. The last common input edge supplies the terminal source equality used by the left contraction.

Theorem 1.5 (Every positive reset graph is essential).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),\mathrm{Essential}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every expanded vertex has an outgoing reset edge. Incoming to suffix zero uses reset with the opposite absolute sign; incoming to a positive suffix uses the predecessor advance with the same sign. Positivity is the only hypothesis, so q=1 is included.

Theorem 1.6 (The square lift equals the finite table map).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),he\in \mathrm{Even}\left(q\right),\forall x\in \mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right),H\left(\mathrm{squares}\left(\mathrm{resetNumberedData}\left(q,hq\right)\right),\mathrm{resetFiniteForgetting}\left(q,hq,he\right),x\right)=\mathrm{applyTable}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{forward}\left(\mathrm{resetAlternatingTablePair}\left(q,hq\right)\right),\mathrm{seamG}\left(\mathrm{resetAlternatingTablesLocal}\left(q,hq,he\right)\right),x\right)$$

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

Source. Repository-derived.

Commentary.

The equality holds on every legal bilateral history. A q+1-square window of the full generic lift is compared with the original forward sweep. Both sides retain the same numbered expanded edge at each integer coordinate. forward denotes the f field of the table pair; seamG is the seam field of reset_alternating_tables_local.

Definition 1.7 (The native history homeomorphism).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),he\in \mathrm{Even}\left(q\right),\mathrm{resetAlternatingWholeRayHomeomorph}\left(q,hq,he\right):\mathrm{Homeomorph}\left(\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right),\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetAlternatingWholeRayHomeomorph (✓ std3).

Source. Repository-derived.

Commentary.

This is Squares.historyHomeomorph applied to the actual reset numbered data and its q-square finite forgetting. Both histories carry their original product and subtype topology.

Definition 1.8 (A full representative for each numbered boundary).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),\forall alpha\in \mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right),n\in Int,r\in \{r:\mathrm{product}\left(\mathrm{Edge}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),Sign\right)|\mathrm{source}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),r\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(alpha,n\right)\right)\},\mathrm{resetRayRepresentative}\left(q,hq,alpha,n,r\right):\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetRayRepresentative (✓ std3).

Source. Repository-derived.

Commentary.

For every positive q, every full history alpha and integer cut n, r is the subtype of full numbered boundary edges with absolute group coordinate whose source equals the target of alpha at n. The representative is NumberedData.beta using the essential reset graph. Its arbitrary legal future extends the prescribed right past; no even hypothesis is needed to define it. A subtype value is denoted value(r).

Theorem 1.9 (Exact disjoint decomposition and every future preimage).

$$\forall q\in Nat,hq\in \mathrm{NatPositive}\left(q\right),he\in \mathrm{Even}\left(q\right),\forall alpha\in \mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right),n\in Int,\mathrm{image}\left(\mathrm{resetAlternatingWholeRayHomeomorph}\left(q,hq,he\right),\{y:\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)|\forall k\in Int,k\le n\Rightarrow \mathrm{coordinate}\left(y,k\right)=\mathrm{coordinate}\left(alpha,k\right)\}\right)={\cup }_{r\in \{r:\mathrm{product}\left(\mathrm{Edge}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),Sign\right)|\mathrm{source}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),r\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(alpha,n\right)\right)\}}\{y:\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)|\forall k\in Int,k\le n\Rightarrow \mathrm{coordinate}\left(y,k\right)=\mathrm{coordinate}\left(\mathrm{resetRayRepresentative}\left(q,hq,alpha,n,r\right),k\right)\}\wedge \left(\left(\forall r\in \{r:\mathrm{product}\left(\mathrm{Edge}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),Sign\right)|\mathrm{source}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),r\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(alpha,n\right)\right)\},\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(\mathrm{resetRayRepresentative}\left(q,hq,alpha,n,r\right),n\right)\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),\mathrm{value}\left(r\right)\right)\right)\wedge \left(\left(\forall r\in \{r:\mathrm{product}\left(\mathrm{Edge}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),Sign\right)|\mathrm{source}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),r\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(alpha,n\right)\right)\},s\in \{r:\mathrm{product}\left(\mathrm{Edge}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),Sign\right)|\mathrm{source}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),r\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(alpha,n\right)\right)\},r\ne s\Rightarrow \mathrm{Disjoint}\left(\{y:\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)|\forall k\in Int,k\le n\Rightarrow \mathrm{coordinate}\left(y,k\right)=\mathrm{coordinate}\left(\mathrm{resetRayRepresentative}\left(q,hq,alpha,n,r\right),k\right)\},\{y:\mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right)|\forall k\in Int,k\le n\Rightarrow \mathrm{coordinate}\left(y,k\right)=\mathrm{coordinate}\left(\mathrm{resetRayRepresentative}\left(q,hq,alpha,n,s\right),k\right)\}\right)\right)\wedge \left(\forall r\in \{r:\mathrm{product}\left(\mathrm{Edge}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),Sign\right)|\mathrm{source}\left(\mathrm{expandedGraph}\left(\mathrm{identityMatrix}\left(Sign,q\right)+\mathrm{resetMatrix}\left(q\right)\right),r\right)=\mathrm{target}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right),\mathrm{coordinate}\left(alpha,n\right)\right)\},y\in \mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right),\left(\forall k\in Int,k\le n\Rightarrow \mathrm{coordinate}\left(y,k\right)=\mathrm{coordinate}\left(\mathrm{resetRayRepresentative}\left(q,hq,alpha,n,r\right),k\right)\right)\Rightarrow \left(\exists x\in \mathrm{History}\left(\mathrm{expandedGraph}\left(\mathrm{resetMatrix}\left(q\right)\right)\right),\left(\forall k\in Int,k\le n\Rightarrow \mathrm{coordinate}\left(x,k\right)=\mathrm{coordinate}\left(alpha,k\right)\right)\wedge \left(\mathrm{apply}\left(\mathrm{resetAlternatingWholeRayHomeomorph}\left(q,hq,he\right),x\right)=y\wedge \mathrm{boundary}\left(\mathrm{leftLift}\left(\mathrm{squares}\left(\mathrm{resetNumberedData}\left(q,hq\right)\right),\mathrm{resetFiniteForgetting}\left(q,hq,he\right),x\right),n\right)=\mathrm{value}\left(r\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every ray in the formula fixes all numbered expanded coordinates at all integers k <= n, including negative times. image is literal set image under the homeomorphism and the union ranges over the exact source-constrained numbered boundary subtype. The four conjuncts state the entire image equality at the same cut, the actual endpoint of every representative, pairwise disjointness for unequal full boundary indices, and a preimage for every legal right future with the original alpha past and exactly that boundary value at n. The preimage boundary is read from Squares.leftLift with the same finite-forgetting proof.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetAlternatingTablePair
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetAlternatingWholeRayHomeomorph
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetFiniteForgetting
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetNumberedData
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.resetRayRepresentative
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.reset_alternating_tables_local
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.reset_even_same_cut_whole_rays
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.reset_expanded_essential
• Truth anchor: D5/S3/ConceptDynamics/Coding/ResetAlternatingHistories.reset_generic_H_eq_applyTable
• Dependency: D5/S3/ConceptDynamics/Coding/ResetAlternatingSquares