Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

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 (Actual complete boundaries and internal inputs).

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

Source. Repository-derived.

Commentary.

For every prefix of the common execution list, both actual initial states retain A_j < D_j < h_j and the high displacement is smaller than the low displacement. Internal inputs obtained by any number of C contractions and six-letter affine iterates remain positive and below h_j, keep the same side ordering, and their signed coordinates belong to [0,T2]. Each complete boundary is identified with the coordinate at stem length plus the weight of the unexecuted suffix in the same fixed source. The lower bound A_j is asserted only at complete boundaries, not at arbitrary internal cuts.

Theorem 1.2 (Strict and per-record-margin supply on the original paired sources).

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

Source. Repository-derived.

Commentary.

For K at least two and the original transition budget q_K < b < Psi_K, strict supply and per-record positive-margin supply of the independently defined actual source pair are each equivalent to the exact cap and strict high guard. The proof derives acquisition for arbitrary repetitions of the original six- and twenty-letter blocks, assembles all errors on the fixed same-list literal sources, and reads their original futures with zero error. It pays the stem and every repeated return, and the anchored template pays its own anchor using chi times X_H. Returns above the cap are rejected at the actual control cost; low returns are strictly supplied. Finite history errors give a positive margin for each record, without a common margin for an infinite family. All five endpoint flags remain arbitrary.

Theorem 1.3 (Complete actual source costs above the nonactive-slot bound).

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

Source. Repository-derived.

Commentary.

This supplier exposes the existing whole-source cost construction with its actual lower-budget hypothesis budget>lam-rho. It is the same fixed source, history, external block order and literal tail used by the strict record theorem. StrictControl recursively tests lam-g^2chi^rD at each actual return start. The stem tests chi times the final whole-list state, and the paid anchor tests chi times X_H, not its output Y_H.

For a six-block input D<h_j, the nth outer input is h_j-rho^n*(h_j-D). Its active cost minus the next active cost is g^2rho^n(1-rho)*(h_j-D)>0. The proof applies the original affine suffix law, interval existence and finite normalization locally at each actual six-slot and twenty-slot departure above lam-rho. The complete block application and its ownership and input domains are given in the Literal source exposition. High/low ordering transports the high costs to the actual paired low source, and the finite departure errors extend by zero on the prescribed future.

Sharp endpoints of the original fixed-tail family

For j equal to high or low, A_j=(1-rho)h_j and X_j=A_j+rhochi^3E_j. The original initial displacement is X_j. The set below contains every finite positive Return list, including the empty list; it concerns complete right suffixes on the prescribed actual sources.

The singleton lists [Return(1,R)] have displacement A_j+rhochi^RX_j, which tends to A_j as R tends to infinity. The lists [Return(M,1)] have displacement h_j-rho^M*(h_j-chi*X_j), which tends to h_j. The strict complete-boundary bounds exclude both endpoints for every finite list. X_j is not a valid lower bound: the original list [Return(1,3)] has displacement below X_j. Internal C inputs can be below A_j, while remaining positive.

Actual finite departure costs

For each side j, list xs and p less than length(history original xs), let z=coordinate(sourcePrefix j original xs,p) and i=history original xs[p]. Its closed-cell cost is max(cut(i)-z,max(0,z-cut(i+1))). actual_strict_cost_supply at budget lam supplies errors of absolute value strictly below lam at every such slot on the same source. literal_address_path supplies support, and owned_color_error, owned_color_interval and expanded_distance_formula imply that the cost is at most the absolute value of that actual error. Thus every finite departure cost is strictly below lam, including the stem and every repeated internal block. The terminal slot at history length is not included.

For the high singleton [Return(1,R)], R>0, departure 30 is the color-1 position in the U immediately next to C^R. Its complete right suffix is C^R followed by the prescribed high tail. The coordinate and closed distance are:

A bound from one prescribed high history

Suppose only that err satisfies ErrorBound b contract err and reads history original xs on the prescribed high source at every departure. No low history or future condition is needed. Write xs=before++[a]++after in execution order. External reversal places the selected return after externalWord high after, and its right complete suffix has displacement D=execute high before (initial high original). The active departure is q=26+length(externalWord high after)+6*(a.m-1)+4, in the last U next to C^(a.r), and its history color is 1. Its coordinate is cut(1)-(lam-g^2*chi^(a.r)D). Closed-distance necessity gives lam-g^2chi^(a.r)D<=b. Since D<h_H, this forces g^2chi^(a.r)*h_H>lam-b.

For each b<lam, geometric convergence permits an integer K with g^2chi^rh_H=K. Every return in any such high history then has r<K, and hence r<=K. This K depends only on b and the fixed system, uniformly over lists, m, ownership and all three error contracts. The empty list has no return to bound.

This bound is necessary only. It supplies no subcritical sufficiency criterion, no rate transfer, and no assertion that restricted subfamilies have zero rate. Increasing m cannot remove the bound on r.

References