Original pieces and a fixed competing tail

Abstract

One competing scalar and tail realize every finite history inside the specified original pieces.

Definition 1.1 (Typed original closed pieces).

$$\forall endpoints\in \mathrm{Finset}\left(Real\right),s\in Guard,lo\in Real,hi\in Real,\mathrm{OriginalPieceFields}\left(endpoints,s,lo,hi\right)\iff \left(\mathrm{member}\left(lo,endpoints\right)\wedge \left(\mathrm{member}\left(hi,endpoints\right)\wedge \left(\mathrm{le}\left(lo,hi\right)\wedge \left(\mathrm{InSupport}\left(s,lo\right)\wedge \left(\mathrm{InSupport}\left(s,hi\right)\wedge \left(\forall z\in Real,\mathrm{member}\left(z,endpoints\right)\Rightarrow \mathrm{not}\left(\mathrm{lt}\left(lo,z\right)\wedge \mathrm{lt}\left(z,hi\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.OriginalPiece (✓ std3).

Source. Repository-derived.

Commentary.

A piece has ordered endpoints in the same finite endpoint set, both in its actual guard support. No endpoint of that set lies strictly between them. Equal endpoints retain every singleton; unequal endpoints give the entire interval between consecutive endpoints. OriginalPieceFields is exactly the displayed condition on its lo and hi fields.

Definition 1.2 (The entire closed carrier).

$$\forall endpoints\in \mathrm{Finset}\left(Real\right),s\in Guard,P\in \mathrm{OriginalPiece}\left(endpoints,s\right),z\in Real,\mathrm{member}\left(z,\mathrm{carrier}\left(P\right)\right)\iff \left(\mathrm{le}\left(\mathrm{lo}\left(P\right),z\right)\wedge \mathrm{le}\left(z,\mathrm{hi}\left(P\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.piece_carrier (✓ std3).

Source. Repository-derived.

Commentary.

The carrier includes both endpoints and every intermediate scalar. A singleton is the closed interval with equal endpoints.

Definition 1.3 (Full original piece paths).

$$\forall endpoints\in \mathrm{Finset}\left(Real\right),A\in \mathrm{List}\left(Label\right),s\in Guard,P2\in \mathrm{OriginalPiece}\left(endpoints,s\right),route\in \mathrm{PathRecord}\left(\right),\mathrm{OriginalPiecePathFields}\left(route,endpoints,A,s,P2\right)\iff \left(\mathrm{apply}\left(\mathrm{guards}\left(route\right),0\right)=G0\wedge \left(\mathrm{apply}\left(\mathrm{guards}\left(route\right),\mathrm{length}\left(A\right)\right)=s\wedge \left(\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(route\right),\mathrm{length}\left(A\right)\right)\right)=\mathrm{carrier}\left(P2\right)\wedge \left(\left(\forall p\in Nat,\mathrm{hasType}\left(\mathrm{apply}\left(\mathrm{pieces}\left(route\right),p\right),\mathrm{OriginalPiece}\left(endpoints,\mathrm{apply}\left(\mathrm{guards}\left(route\right),p\right)\right)\right)\right)\wedge \left(\forall p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(A\right)\right)\Rightarrow \left(\mathrm{nextGuard}\left(\mathrm{apply}\left(\mathrm{guards}\left(route\right),p\right),\mathrm{getElem}\left(A,p\right)\right)=\mathrm{some}\left(\mathrm{apply}\left(\mathrm{guards}\left(route\right),\mathrm{add}\left(p,1\right)\right)\right)\wedge \left(\left(\forall z\in Real,\mathrm{member}\left(z,\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(route\right),p\right)\right)\right)\Rightarrow \left(\exists y\in Real,\mathrm{InSupport}\left(\mathrm{apply}\left(\mathrm{guards}\left(route\right),\mathrm{add}\left(p,1\right)\right),y\right)\wedge z=\mathrm{branch}\left(\mathrm{getElem}\left(A,p\right),y\right)\right)\right)\wedge \left(\forall y\in Real,\mathrm{member}\left(y,\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(route\right),\mathrm{add}\left(p,1\right)\right)\right)\right)\Rightarrow \mathrm{member}\left(\mathrm{branch}\left(\mathrm{getElem}\left(A,p\right),y\right),\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(route\right),p\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.OriginalPiecePath (✓ std3).

Source. Repository-derived.

Commentary.

PathRecord has a guard sequence and a piece of that guard at each position. The initial guard is G0; at the prefix length the guard and carrier are the specified terminal piece. Each prefix edge has its actual nextGuard transition, its whole source carrier in the legal branch root domain, and the image of the whole target carrier inside the source carrier. OriginalPiecePathFields expands exactly these requirements. Positions after the terminal index are unused.

Theorem 1.4 (Joint transport from one terminal scalar).

$$\forall A\in \mathrm{List}\left(Label\right),pieces\in Nat\to \mathrm{Set}\left(Real\right),z\in Real,\left(\mathrm{member}\left(z,\mathrm{apply}\left(pieces,\mathrm{length}\left(A\right)\right)\right)\wedge \left(\forall p\in Nat,y\in Real,\left(\mathrm{lt}\left(p,\mathrm{length}\left(A\right)\right)\wedge \mathrm{member}\left(y,\mathrm{apply}\left(pieces,\mathrm{add}\left(p,1\right)\right)\right)\right)\Rightarrow \mathrm{member}\left(\mathrm{branch}\left(\mathrm{getElem}\left(A,p\right),y\right),\mathrm{apply}\left(pieces,p\right)\right)\right)\right)\Rightarrow \left(\forall p\in Nat,\mathrm{le}\left(p,\mathrm{length}\left(A\right)\right)\Rightarrow \mathrm{member}\left(\mathrm{compose}\left(\mathrm{drop}\left(A,p\right),z\right),\mathrm{apply}\left(pieces,p\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.original_piece_suffix_membership (✓ std3). ∎

Source. Repository-derived.

Commentary.

Backward transport through full-containing edges puts every suffix coordinate of the same scalar in its corresponding piece. The terminal index is included, and an empty prefix retains the selected scalar without an edge.

Theorem 1.5 (A selected actual tail and all original prefixes).

$$\forall o\in Ownership,theta\in Real,s\in Guard,Q\in \mathrm{List}\left(Label\right),V\in \mathrm{List}\left(Label\right),h\in \mathrm{List}\left(Color\right),W\in Bool\to \mathrm{List}\left(Color\right),endpoints\in \mathrm{Finset}\left(Real\right),P2\in \mathrm{OriginalPiece}\left(endpoints,s\right),paths\in \mathrm{DependentPathFamily}\left(endpoints,Q,V,s,P2\right),\left(\mathrm{le}\left(0,theta\right)\wedge \left(\mathrm{LegalWord}\left(G0,s,Q\right)\wedge \left(\mathrm{LegalWord}\left(s,s,V\right)\wedge \left(\mathrm{length}\left(Q\right)=\mathrm{length}\left(h\right)\wedge \left(\left(\forall i\in Bool,\mathrm{length}\left(V\right)=\mathrm{length}\left(\mathrm{apply}\left(W,i\right)\right)\right)\wedge \left(\left(\exists z\in Real,\left(\forall n\in Nat,\mathrm{member}\left(\mathrm{iterateApply}\left(\mathrm{composeMap}\left(V\right),n,z\right),\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)\right)\wedge \mathrm{member}\left(z,\mathrm{carrier}\left(P2\right)\right)\right)\wedge \left(\forall zs\in \mathrm{List}\left(Bool\right),\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),0\right)=G0\wedge \left(\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right)\right)=s\wedge \left(\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(\mathrm{apply}\left(paths,zs\right)\right),\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right)\right)\right)=\mathrm{carrier}\left(P2\right)\wedge \left(\left(\forall p\in Nat,\mathrm{hasType}\left(\mathrm{apply}\left(\mathrm{pieces}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right),\mathrm{OriginalPiece}\left(endpoints,\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right)\right)\right)\right)\wedge \left(\forall p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right)\right)\Rightarrow \left(\mathrm{nextGuard}\left(\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right),\mathrm{getElem}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right),p\right)\right)=\mathrm{some}\left(\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),\mathrm{add}\left(p,1\right)\right)\right)\wedge \left(\left(\forall z\in Real,\mathrm{member}\left(z,\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right)\right)\right)\Rightarrow \left(\exists y\in Real,\mathrm{InSupport}\left(\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),\mathrm{add}\left(p,1\right)\right),y\right)\wedge z=\mathrm{branch}\left(\mathrm{getElem}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right),p\right),y\right)\right)\right)\wedge \left(\forall y\in Real,\mathrm{member}\left(y,\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(\mathrm{apply}\left(paths,zs\right)\right),\mathrm{add}\left(p,1\right)\right)\right)\right)\Rightarrow \mathrm{member}\left(\mathrm{branch}\left(\mathrm{getElem}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right),p\right),y\right),\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists tail\in Nat\to Label,x\in Nat\to Real,path\in Nat\to Guard,\left(\mathrm{apply}\left(path,0\right)=s\wedge \left(\left(\forall p\in Nat,\mathrm{nextGuard}\left(\mathrm{apply}\left(path,p\right),\mathrm{apply}\left(tail,p\right)\right)=\mathrm{some}\left(\mathrm{apply}\left(path,\mathrm{add}\left(p,1\right)\right)\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{InSupport}\left(\mathrm{apply}\left(path,p\right),\mathrm{apply}\left(x,p\right)\right)\right)\wedge \left(\forall p\in Nat,\mathrm{apply}\left(x,p\right)=\mathrm{branch}\left(\mathrm{apply}\left(tail,p\right),\mathrm{apply}\left(x,\mathrm{add}\left(p,1\right)\right)\right)\right)\right)\right)\right)\wedge \left(\mathrm{member}\left(\mathrm{apply}\left(x,0\right),\mathrm{carrier}\left(P2\right)\right)\wedge \left(\left(\forall n\in Nat,\mathrm{member}\left(\mathrm{iterateApply}\left(\mathrm{composeMap}\left(V\right),n,\mathrm{apply}\left(x,0\right)\right),\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)\right)\wedge \left(\forall zs\in \mathrm{List}\left(Bool\right),\exists beta\in Nat\to Label,X\in Nat\to Real,q\in Nat\to Guard,\left(\mathrm{apply}\left(q,0\right)=G0\wedge \left(\left(\forall p\in Nat,\mathrm{nextGuard}\left(\mathrm{apply}\left(q,p\right),\mathrm{apply}\left(beta,p\right)\right)=\mathrm{some}\left(\mathrm{apply}\left(q,\mathrm{add}\left(p,1\right)\right)\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{InSupport}\left(\mathrm{apply}\left(q,p\right),\mathrm{apply}\left(X,p\right)\right)\right)\wedge \left(\forall p\in Nat,\mathrm{apply}\left(X,p\right)=\mathrm{branch}\left(\mathrm{apply}\left(beta,p\right),\mathrm{apply}\left(X,\mathrm{add}\left(p,1\right)\right)\right)\right)\right)\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right)\right)\Rightarrow \mathrm{apply}\left(beta,p\right)=\mathrm{getElem}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right),p\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{apply}\left(beta,\mathrm{add}\left(\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right),p\right)\right)=\mathrm{apply}\left(tail,p\right)\wedge \left(\mathrm{apply}\left(X,\mathrm{add}\left(\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right),p\right)\right)=\mathrm{apply}\left(x,p\right)\wedge \mathrm{apply}\left(q,\mathrm{add}\left(\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right),p\right)\right)=\mathrm{apply}\left(path,p\right)\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{le}\left(p,\mathrm{length}\left(\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right)\right)\right)\Rightarrow \left(\mathrm{member}\left(\mathrm{apply}\left(X,p\right),\mathrm{carrier}\left(\mathrm{apply}\left(\mathrm{pieces}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right)\right)\right)\wedge \mathrm{apply}\left(q,p\right)=\mathrm{apply}\left(\mathrm{guards}\left(\mathrm{apply}\left(paths,zs\right)\right),p\right)\right)\right)\wedge \mathrm{OperationRecord}\left(o,theta,closed,beta,\mathrm{recordWithOmegaTail}\left(o,\mathrm{append}\left(h,\mathrm{choiceBlocks}\left(W,zs\right)\right),x\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.selected_original_piece_tail (✓ std3). ∎

Source. Repository-derived.

Commentary.

K is the set of scalars whose every iterate under compose(V) lies in CompetingT. The nonempty intersection K with the specified P2 selects the scalar once. A lawful tail supplies its literal labels, coordinates and guards, fixed before every finite Boolean history. Both original color words are retained even though V is identical. DependentPathFamily supplies one full original path for each Q followed by the selected copies of V, ending at that same P2 in the same endpoint set.

Each actual source retains every prescribed prefix label. At the seam and every later position its label, coordinate and guard agree with the fixed tail. At every prefix index, including the seam, the coordinate belongs to the whole original carrier and the guard is the specified original guard. BlockSupply supplies bounded actual errors in the observed past; future errors are zero on the same source. This finite path lift assumes the specified original paths and does not construct their endpoint set or infer bilateral auxiliary realizations or a decoder upper bound.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.OriginalPiece
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.OriginalPiecePath
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.original_piece_suffix_membership
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.piece_carrier
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/OriginalPieces.selected_original_piece_tail
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/BranchStorage