Actual boundaries for Fibonacci completion

Abstract

Both actual Fibonacci starts retain the complete-boundary, closed and strict source laws and one finite actual reset map.

Theorem 1.1 (Every Boolean choice preserves the return guard).

$$\forall s\in Guard,R\in \mathrm{Function}\left(Bool,\mathrm{List}\left(Label\right)\right),zs\in \mathrm{List}\left(Bool\right),\left(\forall i\in Bool,\mathrm{LegalWord}\left(s,s,\mathrm{apply}\left(R,i\right)\right)\right)\Rightarrow \mathrm{LegalWord}\left(s,s,\mathrm{choiceBlocks}\left(R,zs\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every Boolean choice preserves the return guard. The synchronized source constructions use this exact relation with their chosen fixed tail.

Theorem 1.2 (The exact synchronized observation length).

$$\forall A\in Type,P\in \mathrm{List}\left(A\right),R\in \mathrm{Function}\left(Bool,\mathrm{List}\left(A\right)\right),L\in Nat,n\in Nat,z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\left(\forall i\in Bool,\mathrm{length}\left(\mathrm{apply}\left(R,i\right)\right)=L\right)\Rightarrow \mathrm{length}\left(\mathrm{synchronousPrefix}\left(P,R,z\right)\right)=\mathrm{add}\left(\mathrm{length}\left(P\right),\mathrm{multiply}\left(n,L\right)\right)$$

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

Source. Repository-derived.

Commentary.

The exact synchronized observation length. The synchronized source constructions use this exact relation with their chosen fixed tail.

Theorem 1.3 (Actual addresses retain the literal prefix).

$$\forall A\in \mathrm{List}\left(Label\right),w\in \mathrm{List}\left(Label\right),p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(A\right)\right)\Rightarrow \mathrm{apply}\left(\mathrm{address}\left(\mathrm{append}\left(A,w\right)\right),p\right)=\mathrm{getElem}\left(A,p\right)$$

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

Source. Repository-derived.

Commentary.

Actual addresses retain the literal prefix. The synchronized source constructions use this exact relation with their chosen fixed tail.

Theorem 1.4 (Equal-length block extraction separates literal sources).

$$\forall P\in \mathrm{List}\left(Label\right),R\in \mathrm{Function}\left(Bool,\mathrm{List}\left(Label\right)\right),L\in Nat,w\in \mathrm{List}\left(Label\right),n\in Nat,\left(\left(\forall i\in Bool,\mathrm{length}\left(\mathrm{apply}\left(R,i\right)\right)=L\right)\wedge \mathrm{notEqual}\left(\mathrm{apply}\left(R,false\right),\mathrm{apply}\left(R,true\right)\right)\right)\Rightarrow \left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),zprime\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{address}\left(\mathrm{append}\left(\mathrm{synchronousPrefix}\left(P,R,z\right),w\right)\right)=\mathrm{address}\left(\mathrm{append}\left(\mathrm{synchronousPrefix}\left(P,R,zprime\right),w\right)\right)\Rightarrow z=zprime\right)$$

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

Source. Repository-derived.

Commentary.

Equal-length block extraction separates literal sources. The synchronized source constructions use this exact relation with their chosen fixed tail.

Theorem 1.5 (One finite tail supplies all high histories).

$$\forall o\in Ownership,theta\in Real,s\in Guard,P\in \mathrm{List}\left(Label\right),h\in \mathrm{List}\left(Color\right),R\in \mathrm{Function}\left(Bool,\mathrm{List}\left(Label\right)\right),W\in \mathrm{Function}\left(Bool,\mathrm{List}\left(Color\right)\right),lo\in Real,hi\in Real,\left(\mathrm{le}\left(0,theta\right)\wedge \left(\mathrm{LegalWord}\left(G0,s,P\right)\wedge \left(\mathrm{length}\left(P\right)=\mathrm{length}\left(h\right)\wedge \left(\left(\forall i\in Bool,\mathrm{LegalWord}\left(s,s,\mathrm{apply}\left(R,i\right)\right)\wedge \mathrm{length}\left(\mathrm{apply}\left(R,i\right)\right)=\mathrm{length}\left(\mathrm{apply}\left(W,i\right)\right)\right)\wedge \left(\mathrm{lt}\left(lo,hi\right)\wedge \left(\left(\forall z\in Real,\left(\mathrm{le}\left(lo,z\right)\wedge \mathrm{le}\left(z,hi\right)\right)\Rightarrow \mathrm{InSupport}\left(s,z\right)\right)\wedge \left(\left(\forall i\in Bool,z\in Real,\left(\mathrm{le}\left(lo,z\right)\wedge \mathrm{le}\left(z,hi\right)\right)\Rightarrow \left(\mathrm{le}\left(lo,\mathrm{compose}\left(\mathrm{apply}\left(R,i\right),z\right)\right)\wedge \mathrm{le}\left(\mathrm{compose}\left(\mathrm{apply}\left(R,i\right),z\right),hi\right)\right)\right)\wedge \left(\mathrm{EndpointCertificate}\left(theta,lo,hi,P,h\right)\wedge \left(\forall i\in Bool,\mathrm{EndpointCertificate}\left(theta,lo,hi,\mathrm{apply}\left(R,i\right),\mathrm{apply}\left(W,i\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists e\in Guard,w\in \mathrm{List}\left(Label\right),\mathrm{LegalWord}\left(s,e,w\right)\wedge \left(\mathrm{lt}\left(lo,\mathrm{coordinate}\left(w,0\right)\right)\wedge \left(\mathrm{lt}\left(\mathrm{coordinate}\left(w,0\right),hi\right)\wedge \left(\forall zs\in \mathrm{List}\left(Bool\right),\mathrm{OperationRecord}\left(o,theta,closed,\mathrm{address}\left(\mathrm{append}\left(\mathrm{append}\left(P,\mathrm{choiceBlocks}\left(R,zs\right)\right),w\right)\right),\mathrm{recordWithTail}\left(o,\mathrm{append}\left(h,\mathrm{choiceBlocks}\left(W,zs\right)\right),w\right)\right)\wedge \left(\mathrm{OperationFiniteSource}\left(\mathrm{address}\left(\mathrm{append}\left(\mathrm{append}\left(P,\mathrm{choiceBlocks}\left(R,zs\right)\right),w\right)\right)\right)\wedge \left(\forall p\in Nat,\mathrm{apply}\left(\mathrm{recordWithTail}\left(o,\mathrm{append}\left(h,\mathrm{choiceBlocks}\left(W,zs\right)\right),w\right),\mathrm{add}\left(\mathrm{length}\left(\mathrm{append}\left(h,\mathrm{choiceBlocks}\left(W,zs\right)\right)\right),p\right)\right)=\mathrm{observe}\left(o,\mathrm{coordinate}\left(w,p\right),0\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The numerical hull is nondegenerate, supported and invariant under both legal returns; its stem and return endpoint costs satisfy EndpointCertificate. One finite word w is selected before all Bool choice lists. Each source is address((P++choiceBlocks(R,zs))++w), with the prescribed h++choiceBlocks(W,zs) past followed by the literal zero-error coordinate future of w. Errors are chosen on this same source and are zero after the past. Empty stems and histories remain included. A common positive margin over unbounded histories is not asserted.

Theorem 1.6 (One lawful Omega tail supplies all rival histories).

$$\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 \mathrm{Function}\left(Bool,\mathrm{List}\left(Color\right)\right),a\in Real,y\in Real,\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(\mathrm{lt}\left(\mathrm{negate}\left(1\right),a\right)\wedge \left(\mathrm{lt}\left(a,1\right)\wedge \left(\mathrm{notEqual}\left(a,0\right)\wedge \left(a=\mathrm{power}\left(\mathrm{negate}\left(g\right),\mathrm{length}\left(V\right)\right)\wedge \left(\mathrm{compose}\left(V,y\right)=y\wedge \mathrm{ifThenElse}\left(\mathrm{lt}\left(0,a\right),\mathrm{Nonempty}\left(\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)\wedge \mathrm{member}\left(y,\mathrm{closure}\left(\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)\right),\mathrm{member}\left(y,\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists tail\in \mathrm{Function}\left(Nat,Label\right),x\in \mathrm{Function}\left(Nat,Real\right),path\in \mathrm{Function}\left(Nat,Guard\right),\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(\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 \mathrm{Function}\left(Nat,Label\right),X\in \mathrm{Function}\left(Nat,Real\right),\mathrm{OperationOmega}\left(beta,X\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)\right)\wedge \left(\left(\forall p\in Nat,\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)\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)$$

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

Source. Repository-derived.

Commentary.

constantWordFamily(V)(i)=V and composeMap(V)(z)=compose(V,z). The actual fixed-point and slope equations identify the centered affine return. Positive-slope feasibility uses nonempty CompetingT and closure membership of its fixed point; negative-slope feasibility uses actual CompetingT membership. One supported scalar is lifted to one legal tail before all histories. Each finite choice sees only the remaining number of identical V returns, while both distinct W color choices remain in every orbit test. The full CompetingT orbit condition is equivalent to supported terminal coordinates and BlockSupply for every finite Q-prefixed history; the reverse direction extracts Q and both W blocks from those same histories. Every record uses its own actual finite errors and the unchanged zero-error tail future.

Theorem 1.7 (The same scalar realizes every finite competing history).

$$\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 \mathrm{Function}\left(Bool,\mathrm{List}\left(Color\right)\right),z\in Real,\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(\forall i\in Bool,\mathrm{length}\left(V\right)=\mathrm{length}\left(\mathrm{apply}\left(W,i\right)\right)\right)\right)\right)\right)\Rightarrow \left(\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)\iff \left(\mathrm{InSupport}\left(s,z\right)\wedge \left(\forall zs\in \mathrm{List}\left(Bool\right),\mathrm{BlockSupply}\left(o,theta,false,\mathrm{append}\left(Q,\mathrm{choiceBlocks}\left(\mathrm{constantWordFamily}\left(V\right),zs\right)\right),\mathrm{append}\left(h,\mathrm{choiceBlocks}\left(W,zs\right)\right),z\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

CompetingT tests the support, every stem suffix and both complete color words for the identical return V. Its full forward orbit is equivalent to actual BlockSupply for every finite choice history at the same terminal scalar. Empty histories retain the stem tests.

Theorem 1.8 (An actual record with the fixed literal and scalar future).

$$\forall o\in Ownership,theta\in Real,s\in Guard,A\in \mathrm{List}\left(Label\right),cs\in \mathrm{List}\left(Color\right),tail\in \mathrm{Function}\left(Nat,Label\right),x\in \mathrm{Function}\left(Nat,Real\right),path\in \mathrm{Function}\left(Nat,Guard\right),\left(\mathrm{le}\left(0,theta\right)\wedge \left(\mathrm{length}\left(A\right)=\mathrm{length}\left(cs\right)\wedge \left(\mathrm{LegalWord}\left(G0,s,A\right)\wedge \left(\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 \mathrm{BlockSupply}\left(o,theta,false,A,cs,\mathrm{apply}\left(x,0\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists beta\in \mathrm{Function}\left(Nat,Label\right),X\in \mathrm{Function}\left(Nat,Real\right),\mathrm{OperationOmega}\left(beta,X\right)\wedge \left(\left(\forall p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(A\right)\right)\Rightarrow \mathrm{apply}\left(beta,p\right)=\mathrm{getElem}\left(A,p\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{apply}\left(beta,\mathrm{add}\left(\mathrm{length}\left(A\right),p\right)\right)=\mathrm{apply}\left(tail,p\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{apply}\left(X,\mathrm{add}\left(\mathrm{length}\left(A\right),p\right)\right)=\mathrm{apply}\left(x,p\right)\right)\wedge \mathrm{OperationRecord}\left(o,theta,closed,beta,\mathrm{recordWithOmegaTail}\left(o,cs,x\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

One lawful tail is prepended by the given legal prefix. Actual slot supplies choose bounded errors before the seam; the entire future uses zero error on the same scalar sequence. The resulting source retains the exact prefix labels, shifted tail labels and shifted coordinates.

Theorem 1.9 (Literal source construction at every first stem disagreement).

$$\forall Configuration\in Type,action\in \mathrm{Function}\left(Configuration,\mathrm{Op}\left(Configuration,Color,Label\right)\right),initialConfiguration\in Configuration,o\in Ownership,theta\in Real,s1\in Guard,s2\in Guard,P\in \mathrm{List}\left(Label\right),Q\in \mathrm{List}\left(Label\right),h\in \mathrm{List}\left(Color\right),U\in \mathrm{Function}\left(Bool,\mathrm{List}\left(Label\right)\right),V\in \mathrm{List}\left(Label\right),W\in \mathrm{Function}\left(Bool,\mathrm{List}\left(Color\right)\right),L\in Nat,lo\in Real,hi\in Real,a\in Real,y\in Real,k\in Nat,\left(\mathrm{SynchronousSourceData}\left(o,theta,s1,s2,P,Q,h,U,V,W,L,lo,hi,a,y,k\right)\wedge \left(\mathrm{ClosedOperationSafety}\left(action,initialConfiguration,o,theta\right)\wedge \left(\mathrm{ClosedOperationLiveness}\left(action,initialConfiguration,o,theta\right)\wedge \mathrm{ExecutedPostprocessing}\left(action,initialConfiguration,o,theta\right)\right)\right)\right)\Rightarrow \left(\exists e\in Guard,w\in \mathrm{List}\left(Label\right),eta\in \mathrm{Function}\left(Nat,Label\right),x\in \mathrm{Function}\left(Nat,Real\right),\mathrm{LegalWord}\left(s1,e,w\right)\wedge \left(\mathrm{lt}\left(lo,\mathrm{coordinate}\left(w,0\right)\right)\wedge \left(\mathrm{lt}\left(\mathrm{coordinate}\left(w,0\right),hi\right)\wedge \left(\forall n\in Nat,\exists beta\in \mathrm{Function}\left(\mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{Function}\left(Nat,Label\right)\right),cuts\in \mathrm{Function}\left(\mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{Frame}\left(Configuration,Label\right)\right),states\in \mathrm{Finset}\left(Configuration\right),\left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{OperationRecord}\left(o,theta,closed,\mathrm{SynchronousHighSource}\left(P,U,z,w\right),\mathrm{recordWithTail}\left(o,\mathrm{synchronousPrefix}\left(h,W,z\right),w\right)\right)\wedge \mathrm{OperationFiniteSource}\left(\mathrm{SynchronousHighSource}\left(P,U,z,w\right)\right)\right)\wedge \left(\left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{OperationRecord}\left(o,theta,closed,\mathrm{apply}\left(beta,z\right),\mathrm{recordWithOmegaTail}\left(o,\mathrm{synchronousPrefix}\left(h,W,z\right),x\right)\right)\right)\wedge \left(\left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\forall p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(\mathrm{synchronousPrefix}\left(Q,\mathrm{constantWordFamily}\left(V\right),z\right)\right)\right)\Rightarrow \mathrm{apply}\left(\mathrm{apply}\left(beta,z\right),p\right)=\mathrm{getElem}\left(\mathrm{synchronousPrefix}\left(Q,\mathrm{constantWordFamily}\left(V\right),z\right),p\right)\right)\wedge \left(\left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),p\in Nat,\mathrm{apply}\left(\mathrm{apply}\left(beta,z\right),\mathrm{add}\left(\mathrm{add}\left(\mathrm{length}\left(P\right),\mathrm{multiply}\left(n,L\right)\right),p\right)\right)=\mathrm{apply}\left(eta,p\right)\right)\wedge \left(\left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),p\in Nat,\mathrm{apply}\left(\mathrm{recordWithTail}\left(o,\mathrm{synchronousPrefix}\left(h,W,z\right),w\right),\mathrm{add}\left(\mathrm{add}\left(\mathrm{length}\left(P\right),\mathrm{multiply}\left(n,L\right)\right),p\right)\right)=\mathrm{observe}\left(o,\mathrm{coordinate}\left(w,p\right),0\right)\right)\wedge \left(\mathrm{Injective}\left(\mathrm{SynchronousHighFamily}\left(P,U,n,w\right)\right)\wedge \left(\left(\forall z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{Cut}\left(action,initialConfiguration,\mathrm{front}\left(\mathrm{recordWithTail}\left(o,\mathrm{synchronousPrefix}\left(h,W,z\right),w\right),\mathrm{add}\left(\mathrm{length}\left(P\right),\mathrm{multiply}\left(n,L\right)\right)\right),\mathrm{apply}\left(cuts,z\right)\right)\wedge \left(\mathrm{le}\left(\mathrm{length}\left(\mathrm{output}\left(\mathrm{apply}\left(cuts,z\right)\right)\right),k\right)\wedge \left(\mathrm{output}\left(\mathrm{apply}\left(cuts,z\right)\right)=\mathrm{take}\left(\mathrm{take}\left(P,k\right),\mathrm{length}\left(\mathrm{output}\left(\mathrm{apply}\left(cuts,z\right)\right)\right)\right)\wedge \mathrm{IsPrefix}\left(\mathrm{output}\left(\mathrm{apply}\left(cuts,z\right)\right),\mathrm{take}\left(P,k\right)\right)\right)\right)\right)\wedge \left(\mathrm{Injective}\left(\mathrm{cutStateOutputMap}\left(cuts\right)\right)\wedge \left(\left(\forall c\in Configuration,\mathrm{member}\left(c,states\right)\iff \left(\exists z\in \mathrm{Function}\left(\mathrm{Fin}\left(n\right),Bool\right),\mathrm{state}\left(\mathrm{apply}\left(cuts,z\right)\right)=c\right)\right)\wedge \mathrm{le}\left(\mathrm{power}\left(2,n\right),\mathrm{multiply}\left(\mathrm{card}\left(states\right),\mathrm{add}\left(k,1\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

SynchronousSourceData expands as follows: theta>=0; P and Q are legal G0-to-s1/s2 stems with the same length as h; both U returns and the shared V return are legal and have common length L, equal to each W length; U(false) differs from U(true). The supported high hull [lo,hi] has positive width and is invariant under U, with the finite EndpointCertificate for P and each U/W pair. The actual V slope a=(-g)^length(V) is nonzero and lies between -1 and 1, compose(V,y)=y, and the sign-sensitive CompetingT feasibility holds. The stems agree before k<length(P) and differ at k. ClosedOperationSafety and ClosedOperationLiveness quantify all original closed OperationRecords and all primitive Runs; liveness is positionwise on eventual-L0 sources. ExecutedPostprocessing is a finite Drain only after actual executed acquisitions.

SynchronousHighSource(P,U,z,w)=address(synchronousPrefix(P,U,z)++w), and synchronousPrefix(P,U,z)=P++choiceBlocks(U,List.ofFn(z)); SynchronousHighFamily is this source map. The observation horizon is length(P)+nL. Literal block extraction proves its injection from U(false)!=U(true), without a history-injection premise. Independent lawful zero-error [L0] and [L3] records derive startup, preserving arbitrary k in the target family. cutStateOutputMap(cuts)(z) is the pair of readable state and output at that cut. The actual common-stem theorem gives exactly 2^n<=card(states)*(k+1), with n=0 included. This local theorem assumes numerical hull data. CanonicalGeometry.canonical_legal_return_hull derives canonical width, support, invariance and minimality from legal returns, and FibonacciFactorCompletion.canonical_synchronous_common_stem derives the identical competing return from a degenerate canonical low hull. EndpointNecessity.original_fixed_tail_endpoint_budget proves the arbitrary-fixed-tail endpoint maximum is necessary and belongs to Q(t). Optional original return pieces retain their actual selection and whole-prefix conditions; these results do not supply canonical containing-path synthesis, the full auxiliary SFT theorem or an attaining decoder.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.actual_omega_prefix_record
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.address_prefix
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.choices_legal
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.competingT_orbit_iff_all_histories
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.fixed_finite_tail_all_histories
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.fixed_omega_tail_all_histories
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.original_synchronous_common_stem
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.synchronous_address_injective
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedSources.synchronous_length
• Dependency: D5/S3/ConceptDynamics/Coding/DecoderOperationTrace
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Operations
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry