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 (The guard after a legal literal prefix).

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

Source. Repository-derived.

Commentary.

An actual guard path whose initial guard and every prefix label agree with a legal finite word ends at the prescribed terminal guard. Guard-edge determinism then aligns a fixed tail path after every legal prefix.

Theorem 1.2 (The canonical high hull supplies one finite tail for all histories).

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

Source. Repository-derived.

Commentary.

The two actual high return words differ literally and have the same positive length. The hull endpoints are exactly canonicalReturnLo(U,L) and canonicalReturnHi(U,L). Their width, support and invariance follow from those legal returns. familyEndpointCosts concatenates the indexed endpoint costs for P,h on the U hull, Q,h on the V hull, and each U(i),W(i) and V(i),W(i) pair. Each entry is the maximum of the two endpoint distances max(cut(c)-x,0,x-cut(c+1)) to the closed color interval. There are exactly 2length(h)+4L entries. familyEndpointBudget is their fold by max starting at zero. The legal supports and this one computed maximum derive every supported EndpointCertificate; no certificate is supplied as a premise.

A single finite legal word w is chosen before every finite Bool choice list zs. It lies strictly inside the canonical hull. The actual source is address((P++choiceBlocks(U,zs))++w), and its record is recordWithTail(o,h++choiceBlocks(W,zs),w). The original finite-tail theorem supplies the closed-budget actual record, eventual L0 source and literal zero-error future of this same fixed tail. Empty stems and the empty choice list are included. The finite endpoint maximum is computed and supplies the high actual family. EndpointNecessity.original_fixed_tail_endpoint_budget separately proves necessity for arbitrary fixed literal, scalar and guard tails and membership of that maximum in coefficientField=Q(t); it assumes no tail scalar lies in the canonical hull. The low certificates here are closed constraints and do not by themselves settle actual low endpoint ownership. This high-side statement does not settle the complete original theorem or a common positive margin over unbounded histories.

Theorem 1.3 (Canonical legal families supply the arbitrary common-stem count).

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

Source. Repository-derived.

Commentary.

U and V are the two actual Bool-indexed legal return families of the same positive length L. U(false) differs from U(true). The high hull is computed from U. Equality of the two canonical V endpoints is equivalent to literal V(false)=V(true), so the common competing return and its fixed point are derived. The actual CompetingT tests every Q suffix and both W color words. Its signed feasibility test uses the canonical low endpoint and a=(-g)^L; positive slope retains a closure limit and negative slope requires actual membership.

The finite endpoint budget familyEndpointBudget(P,Q,h,U,V,W,L) is at most theta. Its exact indexed costs derive the observed high stem and return certificates. The nonnegative computed budget also derives theta nonnegativity. EndpointNecessity.original_fixed_tail_endpoint_budget supplies the separate arbitrary-fixed-tail necessity and Q(t) membership result. SameStem compares P and Q at every position below k, and DifferentStem compares their labels at k<P.length. getElem denotes literal list extraction. ClosedOperationSafety, ClosedOperationLiveness and ExecutedPostprocessing retain their original actual-record contracts. SynchronousHighSource(P,U,z,w)=address(synchronousPrefix(P,U,z)++w); SynchronousHighFamily is this map on Fin(n)->Bool, and cutStateOutputMap(z)=((cuts(z)).state,(cuts(z)).output).

One finite high tail and one legal competing Omega tail are fixed before every n. The sources have the actual prescribed prefixes, all histories are acquired on those sources, the high future is the single literal zero-error tail, and literal block extraction gives source injection. Existing common-stem processing then supplies actual cuts and 2^n<=states.card*(k+1), including n=0 and arbitrary supported k. This construction uses the sufficient endpoint bound; its local conclusion is the common-stem count. Necessity is supplied by EndpointNecessity.original_fixed_tail_endpoint_budget. The optional original-piece condition and full auxiliary bilateral/SFT scope require their own hypotheses and conclusions.

Theorem 1.4 (Extremal literal return blocks encode the canonical endpoints).

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

Source. Repository-derived.

Commentary.

imin and imax attain the minimum and maximum of the two actual zero-tail translations. For positive signed slope the lower endpoint repeats U(imin), and the upper endpoint repeats U(imax). For negative slope the respective repeating words are U(imin)++U(imax) and U(imax)++U(imin). Their lengths are L or 2L, so the block periods are one or at most two, including equal translations.

PeriodicTail(s,w,z) means there are label, scalar and guard sequences a,x,path with path(0)=s and x(0)=z, every literal edge legal, every coordinate in that guard’s support, and x(p)=branch(a(p),x(p+1)). At each p<length(w), a(p)=w[p]. For every p the label, scalar and guard at p+length(w) equal their values at p. The proof splices one legal block onto a supported tail and repeats the actual finite block itinerary, using the fixed endpoint coordinate and return guard to verify the joining edge. It does not infer this periodicity from an arbitrary lawful_tail witness or claim a finite-D representative for either endpoint.

Theorem 1.5 (The original weak-list rate is a necessary full-storage lower limit).

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

Source. Repository-derived.

Commentary.

WeakListRate(K,d,sourceModel) is limsup atTop of logb 2 (max 1 (NatCard(WeakCodebook(K,d,sourceModel,n))))/n, with the casts and zero-denominator convention of Lean Real. Every fixed codebook coefficient is bounded by the same full-storage liminf. If that liminf is infinite the result holds directly. Otherwise its finite real value bounds all shifted coefficients. The factor n/(n+C_R) tends to one, and the limsup product inequality recovers the weak-list rate without assuming exact-weight count monotonicity. The anonymous37 equality identifies this rate with the independent factor and original actual contract rates.

The statement concerns the explicit primitive operation presentation and the supplied original complete encoding. Every readable quantity belongs to Configuration; Frame acquisition and output fields are external bookkeeping. An implementation must represent every actual instruction and charged intermediate state at that granularity. Universal correspondence to every prose decoder and independent authored-formula fidelity are separate from this conditional operational mathematics. No single additive constant at the limiting rate and no attaining decoder are asserted.

Theorem 1.6 (Complete configurations separate actual paired records).

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

Source. Repository-derived.

Commentary.

An acquisition stage takes a complete readable configuration and the next color, performs its finite computation, and returns the next configuration and a finite ordered output batch. All control, counters, timing, positions and readable output-side information belong to Configuration. The transition does not read the cumulative emitted word. appendOutputStep(advance)((q,v),c) is (q’,v concatenated with batch), where advance(q,c)=(q’,batch). foldl starts at the fixed initial configuration and initial output. runHistory and configurationHistory apply this recurrence to history(model,xs), taking respectively the joint pair and its first component. Safety is required for every supported legal affine source and actual error-bounded record; liveness requires each position, including L0 positions, at a finite acquisition stage of every eventually-L0 source.

pairedRecord(model,o,xs,j)(p) equals history(model,xs)[p] while p is less than its length M, and equals observe(o,coordinate(tailPrefix(j),p-M),0) thereafter. Its actual error witness, guard path, supported coordinate path and eventual empty tail are constructed from the original paired supply and source reconstruction. Thus the M departures are acquired once, the terminal M is unobserved at the cut, and the original literal future starts there. The original and anchored offsets are 26 and 52; the weight N may be zero or unsupported, and the family may be empty. Every endpoint flag and each original contract remains a parameter.

The high stem begins with L5 and the low stem with L0, so their actual first differing position is k=0. Safety on both continuations forces the cumulative output at the common departure cut to be empty. In general the prefix factor would be k+1; here it is 0+1. Equal cut configurations therefore give equal joint pairs. Folding either pair along the same high-side literal future gives identical subsequent output. Positionwise finite liveness and safety then equate the two high source addresses, and equal-weight actual address separation recovers the lists. The joint and configuration maps are injective and the number of family members is at most the number of reached complete configurations times one. The emitted word supplies no readable memory. This finite lower bound applies to each compliant transition semantics; it asserts no upper bound on inefficient decoders and no storage-capacity estimate without a configuration encoding.

Theorem 1.7 (The exact three-term automatic bound).

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

Source. Repository-derived.

Commentary.

actualAutomaticCost(K)=max(max(lam-g^2chixSide(high),lam-g^2chi^(K-1)aSide(high)),lam-g^6). This is precisely C_auto of the original display. The three entries are the fixed-anchor cost Theta_1, the low-return and stem envelope, and the nonactive-slot bound. For K>=2, chih_H<A_H and X_H>A_H give the first two strict comparisons with q_K; g^2chi^K*h_H<g^6 gives the third. The natural subtraction in K-1 is used only under K>=2.

Every actual complete state lies above A_H. A stem uses chiD; every r<K return uses chi^rD>=chi^(K-1)*D. These inputs strictly exceed chi^(K-1)*A_H and their active costs are below C_auto. The stated scalar bounds are consumed by the capped supplier and the exact-margin theorem.

Theorem 1.8 (Capped complete sources at every budget above C_auto).

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

Source. Repository-derived.

Commentary.

Only budget>C_auto, the literal cap r<=K, and the active-cost test at each actual r=K position are needed. There is no q_K<budget premise. The exact split before++(a::after) identifies the actual prefix state. Automatic slots pass by the envelope; high positions pass by the supplied strict cost. The resulting ActualPairSupply contains the whole prescribed paired sources and original zero-error futures for arbitrary ownership flags.

Theorem 1.9 (The original C_auto-based numerical margin for the whole family).

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

Source. Repository-derived.

Commentary.

Write G=actualFamilyHighGaps(model,b,K,family), Delta=actualFamilyDelta(model,b,K,family), and c=g^2chi^K. If G is nonempty, actualExactFamilyMargin is min(b-C_auto,cDelta.toReal)/2. If G is empty, it is (b-C_auto)/2. Delta is the signed EReal infimum over every actual high position; in the nonempty positive case the proof establishes Delta<top and Delta!=bottom before using toReal. No attained minimum is assumed.

The same positive epsilon is fixed before all lists and both source sides. In the nonempty case every high gap is at least Delta.toReal. Taking half the displayed minimum leaves strict budget room both above C_auto and above every high active cost. With no high returns the latter condition is vacuous, so the separate original formula applies even if the new budget is below q_K. All slots satisfy strict error bound b-epsilon, which also gives the requested closed bound with that exact epsilon, and the original literal futures have zero error.

The family remains an arbitrary set of finite return lists, with unbounded exponents m, histories, list depths and weights. Both actual models and every ownership assignment remain parameters. The full-family equivalence uses the exact necessary epsilon lower bound and the ownership-sensitive closed high-guard law.

Theorem 1.10 (The supplied epsilon bounds every actual high-return gap).

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

Source. Repository-derived.

Commentary.

actualFamilyHighGaps(model,b,K,family) is the real set of execute(high,before,initial(high,model))-(lam-b)/g^2/chi^K, for every literal decomposition before++(a::after) belonging to family with a.r=K. Each decomposition selects the actual state before that return. This includes every high-return position of every family list; no return-length, list-depth, weight or family-cardinality bound is imposed.

The same supplied epsilon is used for every record and both sides. Its closed error budget b-eps is not required as an extra premise to belong to the transition interval. If a control cost exceeded that budget, the complete-boundary inequality D<h_H would permit an intermediate budget strictly above q_K and strictly below both b and that cost. Monotonicity preserves the identical errors, observations and literal futures at that intermediate budget. The existing ownership-sensitive closed guard then contradicts its control cost. Thus the original eps, without shrinking, gives gap>=eps/(g^2*chi^K). This bound is consumed by the family equivalence.

Theorem 1.11 (Positive extended-real infimum is equivalent to one family margin).

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

Source. Repository-derived.

Commentary.

actualFamilyDelta is sInf of the image of actualFamilyHighGaps under the signed real inclusion into EReal. Negative gaps are preserved. The empty high-return set has infimum top, namely positive infinity. The family itself may be empty, and a nonempty family may have no high return. No compactness, attained minimum, finite codebook or common weight is assumed.

ActualUniformFamilyMargin means there exists one real eps>0 such that every execution in family satisfies ActualPairSupply(model,o,b-eps,closed,execution). Unfolding that existing supply predicate, every side has its own error function bounded by b-eps at all natural positions, reads every departure of the complete history from the same sourcePrefix, is zero at and beyond the history length, and gives the original tailPrefix zero-error readout after the observedPrefix. The stem, paid anchor, all repetitions, literal external block order and unchanged eventual-empty tail therefore remain those of the existing source construction.

The reverse implication directly consumes actual_exact_uniform_family_margin. It chooses the original C_auto-based epsilon for the nonempty or empty actual high-gap set, then uses those same whole-source witnesses with the closed b-eps bound. The exact sufficient-margin supplier remains valid even when that new budget is below q_K. This works for either original or anchored model and every ownership assignment. Individual-record margins and ownership-sensitive equality at the original closed budget remain the separate existing statements.

The forward implication consumes the exact necessary bound for the original supplied epsilon; the reverse implication consumes the precise two-branch C_auto margin. Together they give the whole-family infimum criterion.

The finite configuration lower bound uses full actual supply, safety and positionwise liveness. A lower or upper occurrence map alone does not supply a common positive margin for an infinite family.

References