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 supported scalar has one legal itinerary).

$$\forall s\in Guard,z\in Real,\mathrm{InSupport}\left(s,z\right)\Rightarrow \left(\exists a\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(a,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(a,p\right),\mathrm{apply}\left(x,\mathrm{add}\left(p,1\right)\right)\right)\right)\right)\right)\right)\wedge \mathrm{apply}\left(x,0\right)=z\right)$$

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

Source. Repository-derived.

Commentary.

The closed branch images cover [-1,phi] at G0 and [-1,t] at G1. The inverse branch (shift(label)-z)/g remains in its next guard support. Iterating supported guard-scalar pairs gives one label sequence, one coordinate sequence and one legal guard path with the requested scalar. Shared branch endpoints remain legal.

Theorem 1.2 (Finite legal zero tails approximate every supported scalar).

$$\forall s\in Guard,z\in Real,epsilon\in Real,\left(\mathrm{InSupport}\left(s,z\right)\wedge \mathrm{lt}\left(0,epsilon\right)\right)\Rightarrow \left(\exists e\in Guard,w\in \mathrm{List}\left(Label\right),\mathrm{LegalWord}\left(s,e,w\right)\wedge \mathrm{lt}\left(\mathrm{abs}\left(\mathrm{subtract}\left(z,\mathrm{coordinate}\left(w,0\right)\right)\right),epsilon\right)\right)$$

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

Source. Repository-derived.

Commentary.

Truncate the same itinerary after n labels. The exact remaining-coordinate error is (-g)^nx(n), whose absolute value is at most phig^n. Geometric convergence gives every positive tolerance. This density concerns the full guard support; it does not identify that interval with a two-return attractor.

Theorem 1.3 (A finite tail in a supported interval interior).

$$\forall s\in Guard,lo\in Real,hi\in Real,\left(\mathrm{lt}\left(lo,hi\right)\wedge \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)\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(\mathrm{OperationFiniteSource}\left(\mathrm{address}\left(w\right)\right)\wedge \left(\exists path\in \mathrm{Function}\left(Nat,Guard\right),\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(\mathrm{address}\left(w\right),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(\mathrm{coordinateSequence}\left(w\right),p\right)\right)\right)\wedge \left(\forall p\in Nat,\mathrm{apply}\left(\mathrm{coordinateSequence}\left(w\right),p\right)=\mathrm{branch}\left(\mathrm{apply}\left(\mathrm{address}\left(w\right),p\right),\mathrm{apply}\left(\mathrm{coordinateSequence}\left(w\right),\mathrm{add}\left(p,1\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

A midpoint approximation within half the interval width yields a finite legal word whose zero-tail scalar lies strictly between lo and hi. coordinateSequence(w)(p)=coordinate(w,p). The full eventually-L0 address and its entire legal supported coordinate path are retained, for either initial guard.

Theorem 1.4 (Splicing one fixed legal coordinate tail).

$$\forall s\in Guard,e\in Guard,w\in \mathrm{List}\left(Label\right),a\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{LegalWord}\left(s,e,w\right)\wedge \left(\mathrm{apply}\left(path,0\right)=e\wedge \left(\left(\forall p\in Nat,\mathrm{nextGuard}\left(\mathrm{apply}\left(path,p\right),\mathrm{apply}\left(a,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(a,p\right),\mathrm{apply}\left(x,\mathrm{add}\left(p,1\right)\right)\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),q\in \mathrm{Function}\left(Nat,Guard\right),\left(\mathrm{apply}\left(q,0\right)=s\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(\mathrm{apply}\left(X,0\right)=\mathrm{compose}\left(w,\mathrm{apply}\left(x,0\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{lt}\left(p,\mathrm{length}\left(w\right)\right)\Rightarrow \mathrm{apply}\left(beta,p\right)=\mathrm{getElem}\left(w,p\right)\right)\wedge \left(\left(\forall p\in Nat,\mathrm{apply}\left(beta,\mathrm{add}\left(\mathrm{length}\left(w\right),p\right)\right)=\mathrm{apply}\left(a,p\right)\right)\wedge \left(\forall p\in Nat,\mathrm{apply}\left(X,\mathrm{add}\left(\mathrm{length}\left(w\right),p\right)\right)=\mathrm{apply}\left(x,p\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

TailPath(s,a,x,path) means that path starts at s, every label follows nextGuard, every scalar lies in its corresponding support, and every affine recurrence holds. A legal finite prefix prepends exactly its labels and composition value. Both shifted futures are exact, including the recurrence at the splice boundary.

Theorem 1.5 (Exact color cells and all five endpoint flags).

$$\forall o\in Ownership,c\in Color,z\in Real,\mathrm{Cell}\left(o,c,z\right)\iff \mathrm{FlagInterval}\left(\mathrm{cut}\left(\mathrm{val}\left(c\right)\right),\mathrm{cut}\left(\mathrm{add}\left(\mathrm{val}\left(c\right),1\right)\right),\mathrm{lowerOwned}\left(o,c\right),\mathrm{upperOwned}\left(o,c\right),z\right)$$

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

Source. Repository-derived.

Commentary.

FlagInterval(lo,hi,left,right,z) is lo<=z<=hi with z=lo implying left and z=hi implying right. lowerOwned is true at color zero and otherwise uses the corresponding true flag; upperOwned is true at color five and otherwise uses the corresponding false flag. These are exactly the original Cell boundaries.

Theorem 1.6 (Closed error dilation with actual endpoint ownership).

$$\forall o\in Ownership,theta\in Real,c\in Color,z\in Real,\mathrm{le}\left(0,theta\right)\Rightarrow \left(\mathrm{OwnedColor}\left(o,theta,c,z\right)\iff \left(\mathrm{InSupport}\left(G0,z\right)\wedge \mathrm{FlagInterval}\left(\mathrm{subtract}\left(\mathrm{cut}\left(\mathrm{val}\left(c\right)\right),theta\right),\mathrm{add}\left(\mathrm{cut}\left(\mathrm{add}\left(\mathrm{val}\left(c\right),1\right)\right),theta\right),\mathrm{lowerOwned}\left(o,c\right),\mathrm{upperOwned}\left(o,c\right),z\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

OwnedColor(o,theta,c,z) requires z in G0 support and a target u in the actual Cell(o,c) with abs(z-u)<=theta. Dilation shifts the two cell endpoints by theta and retains their original ownership. Support is intersected separately, so clipping an expanded interval does not transfer an unrelated ownership flag to a new boundary. At theta zero the target is z itself.

Theorem 1.7 (Attainable colors are exact observe error outcomes).

$$\forall o\in Ownership,theta\in Real,c\in Color,z\in Real,\mathrm{InSupport}\left(G0,z\right)\Rightarrow \left(\mathrm{OwnedColor}\left(o,theta,c,z\right)\iff \left(\exists error\in Real,\mathrm{le}\left(\mathrm{abs}\left(error\right),theta\right)\wedge \mathrm{observe}\left(o,z,error\right)=c\right)\right)$$

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

Source. Repository-derived.

Commentary.

For supported z, clipping z+error changes its distance from z by at most abs(error). Conversely a supported target u is fixed by clip and is obtained with error=u-z. This proves both directions of the actual observe relation, including every ownership flag.

Theorem 1.8 (Actual attainable color sets are intervals).

$$\forall o\in Ownership,theta\in Real,c\in Color,\mathrm{le}\left(0,theta\right)\Rightarrow \mathrm{OrdConnected}\left(\mathrm{setOfOwnedColor}\left(o,theta,c\right)\right)$$

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

Source. Repository-derived.

Commentary.

setOfOwnedColor(o,theta,c) is the set of real z satisfying OwnedColor(o,theta,c,z). Its supported flagged interval is order-connected, including empty sets and excluded endpoints.

Theorem 1.9 (The actual competing-tail intersection is an interval).

$$\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),\mathrm{le}\left(0,theta\right)\Rightarrow \mathrm{OrdConnected}\left(\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)$$

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

Source. Repository-derived.

Commentary.

CompetingT is the intersection of the terminal guard support, every actual Q-suffix color constraint for r<h.length, and every V-suffix constraint for each of the two W words. Affine preimages preserve order-connectedness for either slope sign. No terminal color test is added.

Theorem 1.10 (Concrete tail membership and actual slot errors).

$$\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),\forall z\in Real,\left(\mathrm{LegalWord}\left(G0,s,Q\right)\wedge \mathrm{LegalWord}\left(s,s,V\right)\right)\Rightarrow \left(\mathrm{member}\left(z,\mathrm{CompetingT}\left(o,theta,s,Q,V,h,W\right)\right)\iff \left(\mathrm{InSupport}\left(s,z\right)\wedge \left(\mathrm{BlockSupply}\left(o,theta,false,Q,h,z\right)\wedge \left(\forall i\in Bool,\mathrm{BlockSupply}\left(o,theta,false,V,\mathrm{apply}\left(W,i\right),z\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Legal Q and V words transport support through every suffix. Membership in CompetingT is exactly supported terminal membership and the closed BlockSupply conditions for the stem and both return-color choices.

Theorem 1.11 (Finite endpoint costs supply every interior slot).

$$\forall o\in Ownership,theta\in Real,lo\in Real,hi\in Real,w\in \mathrm{List}\left(Label\right),cs\in \mathrm{List}\left(Color\right),x\in Real,\left(\mathrm{le}\left(0,theta\right)\wedge \left(\mathrm{EndpointCertificate}\left(theta,lo,hi,w,cs\right)\wedge \left(\mathrm{lt}\left(lo,x\right)\wedge \mathrm{lt}\left(x,hi\right)\right)\right)\right)\Rightarrow \mathrm{BlockSupply}\left(o,theta,false,w,cs,x\right)$$

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

Source. Repository-derived.

Commentary.

EndpointCertificate gives supported images of lo and hi at each departure suffix and bounds max(cut(c)-z,0,z-cut(c+1)) by theta at each image. A nonzero literal suffix slope sends an interior scalar strictly between those two endpoint images. This yields actual ownership-sensitive error witnesses at theta, including theta zero.

Theorem 1.12 (Endpoint-sensitive scalar competing-tail orbits).

$$\forall T\in \mathrm{Set}\left(Real\right),a\in Real,y\in Real,\left(\mathrm{OrdConnected}\left(T\right)\wedge \left(\mathrm{lt}\left(\mathrm{negate}\left(1\right),a\right)\wedge \left(\mathrm{lt}\left(a,1\right)\wedge \mathrm{notEqual}\left(a,0\right)\right)\right)\right)\Rightarrow \left(\left(\forall x\in Real,\left(\forall n\in Nat,\mathrm{member}\left(\mathrm{iterateApply}\left(\mathrm{CenteredAffine}\left(y,a\right),n,x\right),T\right)\right)\iff \mathrm{ifThenElse}\left(\mathrm{lt}\left(0,a\right),\mathrm{member}\left(x,T\right)\wedge \mathrm{member}\left(y,\mathrm{closure}\left(T\right)\right),\mathrm{member}\left(x,T\right)\wedge \mathrm{member}\left(\mathrm{apply}\left(\mathrm{CenteredAffine}\left(y,a\right),x\right),T\right)\right)\right)\wedge \left(\left(\exists x\in Real,\forall n\in Nat,\mathrm{member}\left(\mathrm{iterateApply}\left(\mathrm{CenteredAffine}\left(y,a\right),n,x\right),T\right)\right)\iff \mathrm{ifThenElse}\left(\mathrm{lt}\left(0,a\right),\mathrm{Nonempty}\left(T\right)\wedge \mathrm{member}\left(y,\mathrm{closure}\left(T\right)\right),\mathrm{member}\left(y,T\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

CenteredAffine(y,a)(x)=y+a(x-y), and iterateApply(f,n,x)=f^[n](x). T is any order-connected real set, including empty and singleton intervals. For 0<a<1 the full orbit condition is x in T and y in closure(T); membership of y itself is unnecessary. For -1<a<0 it is x in T and f(x) in T; these two actual members also force y in T, and this is equivalent to a nonempty feasible orbit set. Positive iterates converge to y and lie strictly between the initial point and y; negative iterates remain in the closed segment between x and f(x). Actual open and closed endpoint membership is retained.

This is the scalar interval part of the original39.5 criterion. The concrete owned-color intersection and fixed-tail constructions connect this scalar condition to actual legal source records under their explicit hull and return-map data. CanonicalGeometry.canonical_legal_return_hull derives the legal-return hull and its nondegeneracy and minimality. FibonacciFactorCompletion.canonical_synchronous_common_stem derives the identical competing return when its canonical hull is a singleton. EndpointNecessity.original_fixed_tail_endpoint_budget proves arbitrary-fixed-tail necessity and Q(t) membership of the endpoint maximum. An optional original-piece restriction requires a member of the feasible orbit set in that piece and is imposed only when present in the family. OriginalPieces proves same-tail realization with the supplied full-containing piece paths; this scalar criterion does not construct those paths or prove their completeness. The full original39, auxiliary62.18, interior spectral root and storage/decoder33.13 optimum conclusions require their remaining original conditions.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.cell_flag_interval
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.certificate_actual_slots
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.competingT_mem_actual
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.competingT_ordConnected
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.competing_tail_orbit_criterion
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.finite_approximation
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.finite_tail_interior
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.lawful_tail
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.owned_color_error
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.owned_color_interval
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.owned_color_ordConnected
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/TailGeometry.prepend_legal_tail
• Dependency: D5/S3/ConceptDynamics/Coding/DecoderOperationTrace
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Operations