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 (A supplied reset retains the all-horizon codebook bound).

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

Source. Repository-derived.

Commentary.

R, sourceModel, target model and exact weight N are supplied parameters. The source premises are the empty-list ActualPairSupply and, for every q, the power of the full weak dictionary cardinal bounded by the cardinal of all actual supplied lists of weight q(N+20+6R.m). They assert actual source membership and count, never decoder capacity, a configuration injection or a storage lower bound. The primitive-operation capacity bound on those actual sources, followed by floor interpolation and the finite or infinite peak cases, gives the displayed lower-limit conjunction. Choosing the original reset and actual source book yields original_codebook_storage_liminf.

An exact downstream application may use the same supplied FixedCodebook R and its unchanged actual field. Its positive fixed-codebook error converts the strict supply at b-eps to each original contract at b; literal reset concatenation and the existing equal-weight parser derive all-q counts. The original source labels, colors and guards, both templates with offsets 26/52, same-list high/low D sources, first labels 5/0, empty past output and high common future versus the low side’s own future retain their meanings. Margins may depend on N. No equality between separately chosen existential resets is required.

For the stated original color-record contract, Configuration contains the decoder’s actual readable control, phase, persistent and temporary workspace, counters, input/output positions, clocks, timing and readable output-side storage. action follows its actual primitive instructions, retaining every charged intermediate state and actual finite ordered emission. Frame.acquired and Frame.output are proof-only bookkeeping and provide no machine input. Finite-prefix trace correspondence transports all-Omega safety, all-D per-position liveness including L0 padding, and finite processing. This is a source interpretation of the stated contract, without an independent physical-machine universality claim.

The original prefix cost is the supremum over all actual reached configurations with acquisition count at most H. Reach inclusion gives monotonicity. Split an original top peak before choosing finite layouts: it remains top at all larger horizons and its ratio liminf is top. Otherwise actual complete binary layouts are faithful on actual reach, with harmless totalization elsewhere. Trace reflection and each reached layout’s charged cost bound give operationalPeak(H)<=originalPeak(H) by indexed suprema. No uniform memory, state, support or processing bound and no free checkpoint lower bound are supplied. The necessary coefficient does not assert a uniform eta_b H-C loss or an attaining decoder.

Theorem 1.2 (Full finite weak codebooks with one reset at every seam).

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

Source. Repository-derived.

Commentary.

WeakCodebook(K,d,sourceModel,N) is the entire subtype of return lists xs with GuardTrace K d false high xs (initial high sourceModel) and listWeight xs=N. The single reset R is chosen before sourceModel and N. Its r is one and C_R=20+6R.m. resetConcatenation(R,[]) is []; resetConcatenation(R,xs::words) is (R::xs) appended to resetConcatenation(R,words). Each chosen word receives this same reset. For every N>0 the full subtype is finite. The positive eps may depend on N and sourceModel, but works for every finite joint choice, every target model and every number of seams. It supplies the actual paired sources at closed budget b-eps and hence all three contracts at b. Their fixed literal tails and zero-error futures are those of ActualPairSupply. The total weight is q(N+C_R).

The reset state strictly exceeds either initial state. The affine difference over every word prefix is bounded below by (B-D)g^N; choosing eps below a fixed multiple of that gap makes each high guard strict at every seam. The exact positive weights recover equal-weight words from their cumulative cuts, even when their return-list lengths differ. Thus all q-tuples inject into actual lists and give at least NatCard(WeakCodebook)^q members. Empty and unsupported codebooks and q=0 are included. No common margin over all weights is asserted.

Theorem 1.3 (All observation horizons force the exact codebook coefficient).

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

Source. Repository-derived.

Commentary.

AllActualReachable consists of configurations c for which ReachThrough(H,c) holds for some H. The supplied encoding is injective on this complete set. PeakFunction(H) is the WithTop Nat supremum of encoding lengths over all records and all primitive vertices through H. CompletePeakRatio(H) is ENat.toENNReal(PeakFunction(H))/(H:ENNReal), and liminfAtTop is its lower limit over natural observation horizons. Safety, positionwise D liveness and finite drains after actual acquisitions are expanded in the displayed premises; no independent startup premise is supplied. Actual empty-list high/low records have distinct first labels, so these contracts derive finite startup.

For every fixed N>0 with a=NatCard(WeakCodebook)>=1, L=N+C_R is positive and Delta is the original 26 or anchored 52. The exhaustive actual-operation separation and full variable-length capacity yield a^q<=2^(B+1)-1 at Delta+qL. Monotonicity of the complete peak transfers this bound to q=floor((H-Delta)/L) for every H>=Delta. Thus q log2(a)-1<=B whenever the full peak is bounded by B. Floor interpolation has a fixed-codebook loss divided by H, which tends to zero. Infinite peaks are treated as top, without finite conversion. The resulting necessary lower-limit coefficient is exactly log2(a)/(N+C_R).

Theorem 1.4 (Actual primitive cuts and the complete encoding peak).

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

Source. Repository-derived.

Commentary.

OperationOmega(a,x) is exactly the original legal supported affine path: path starts at G0, follows nextGuard on a, supports x at each position, and x(p)=branch(a(p),x(p+1)). OperationRecord(o,b,contract)(a,r) supplies that path and an original ErrorBound error with observe(o,x(p),err(p))=r(p) at every position. OperationFiniteSource is eventual L0. OperationSafety and OperationLiveness quantify every such original record and every finite primitive trace, with positionwise liveness on eventual L0 sources. Processing includes the real startup drain and actual post-acquisition drains, with no global termination on unreachable states.

ExactActualPairFamily is the subtype of all return lists satisfying ActualPairSupply(model,o,b,contract) and listWeight=N, without sampling or weight monotonicity. The original anonymous45 finite-family construction is reused. Every cut is constructed from actual D liveness. Its high and low paired records share history(model,xs); the same retained primitive past trace embeds on the low record. Safety and the actual L5/L0 first difference force the output word to be empty. Equal original cut states replay the same literal high future; safety and positionwise D liveness recover equal addresses and the original source injection recovers the return lists. Cut uniqueness follows primitive determinism at input exhaustion.

stateCutMap(cuts)(x) is state(cuts(x)). states is its finite image, whose cardinal is exactly NatCard of the exhaustive family. The history length is observationOffset(model)+N, namely 26+N for original and 52+N for anchored. AllActualReachable means configurations in ReachThrough(H) for some H. The supplied original complete encoding is injective on that set. PeakFunction is H mapped to the full WithTop Nat encoding-length supremum over every actual record and primitive intermediate state. A finite peak bound B yields at most 2^(B+1)-1 variable-length codes. Fixed complete width B at the selected states yields at most 2^B codes. Infinite peaks and empty or unsupported exact-weight families remain included. Every trace vertex in the horizon is bounded by this full peak.

This result is for the explicit primitive operation presentation. It proves neither universal representation of every prose decoder nor the source initialization and endpoint correspondence. The equal-weight codebook and complete-storage lower-limit results provide the additional necessary coefficient argument.

Theorem 1.5 (One fixed actual stem gives the original prefix factor).

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

Source. Repository-derived.

Commentary.

The finite supplied family has actual alpha records in eventual L0 and actual beta records in Omega, using precisely OperationRecord and all original error contracts and endpoint flags. Each high and low record shares the same n acquired colors for its family member. The high unread future is the same across members; the low future may differ. The single word w is fixed independently of the family member. Both actual addresses agree with w before its length and differ at that position; sourceInjection concerns alpha addresses only and is a source-side hypothesis.

Actual high-side liveness constructs each cut, and primitive past transfer supplies the beta run without assuming progress on all Omega records. Safety at the first disagreement bounds old output length by length(w); safety before it gives output=take(w,length(output)) and prefix membership. Equal cut state and old word then permit unread-suffix replay, forcing equal alpha addresses and equal family members. jointCutMap is the external pair of cut state and cumulative old word. Prefix length injects the possible words into Fin(length(w)+1). Counting the finite state image times that many prefix tags gives NatCard(Z) at most card(states)*(length(w)+1). The old word is never readable storage. No prefix or joint decoder injection is assumed.

This theorem requires actual source-side witnesses and preserves their fixed-stem and common-future scope. The original39.7 construction supplying those witnesses is not newly formalized here. It is not a standalone product-cardinality result and does not change the retained k0 source family.

References