Fixed-tail endpoint-budget necessity
Abstract
The same full actual tails across every finite history force the original six-group endpoint budget in Q(t).
Theorem 1.1 (Every fixed actual tail obeys the complete endpoint budget).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EndpointNecessity.original_fixed_tail_endpoint_budget (✓ std3). ∎
Source. Repository-derived.
Commentary.
ClosedOriginalTailExtension(b,A,cs,xi,x,path) means there exist full literal, scalar and guard sequences a,X,q starting at guard G0, following every original nextGuard edge, supported at every position, and satisfying X(p)=branch(a(p),X(p+1)). The first length(A) labels equal A. At length(A)+p all three future sequences equal respectively xi(p),x(p),path(p), for every p. Only departures r<length(cs) satisfy ClosedExpanded(b,cs[r],X(r)). The theorem makes the observed source and color lengths equal. ClosedExpanded(b,c,z) is the original closed relaxation z in [-1,phi], cut(c)-b<=z<=cut(c+1)+b.
The same two full futures are fixed before every finite Boolean choice word, including the empty word. Their starting scalars need not belong to either canonical hull. For each component, the existing canonical periodic endpoint supplies one repeated extremal return when (-g)^L is positive, or two alternating extremal returns when it is negative. Finite repetitions act on the original fixed scalar. The existing signed orbit criterion, applied to the closed affine preimage of one slot constraint, forces that endpoint to satisfy the slot. Stem slots use the extremal choice history directly; each return slot uses its chosen first return followed by that history. Both endpoints of every one of the six indexed groups are included. Different endpoint tests may use different histories under the universal premise.
familyEndpointBudget is the existing foldr max 0 of familyEndpointCosts, with exactly two stem groups and all four return groups. Equal-valued entries are retained. Original suffix evaluations, all cut values and canonical endpoints belong to coefficientField=Q(t); every finite maximum selects one of its arguments. Each endpoint cost is at most the supplied nonnegative b, so the whole maximum is at most b and belongs to that field. Empty stems, singleton hulls, equal returns, either slope sign and b=0 are included. This necessary bound does not require U(false)!=U(true); the original source-separation requirements remain in the separate original goal.
This is necessity for the closed relaxation. It asserts neither ownership-sensitive color attainment at equality, nor a new decoder-capacity or optional-piece result. No terminal color is tested. The high and low futures may differ. No budget infimum over a changing family of tails replaces the original fixed-tail quantifiers.