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 (Literal auxiliary padding of weak complete actual lists).

$$\forall K\in Nat,d\in Real,model\in Model,xs\in \mathrm{List}\left(Return\right),\left(\mathrm{le}\left(1,K\right)\wedge \mathrm{GuardTrace}\left(K,d,false,high,xs,\mathrm{initial}\left(high,model\right)\right)\right)\Rightarrow \left(\mathrm{pastState}\left(\mathrm{uPadding}\left(\mathrm{executionWord}\left(xs\right)\right),0\right)=\mathrm{hSide}\left(high\right)\wedge \left(\left(\forall p\in Nat,\mathrm{le}\left(p,\mathrm{length}\left(xs\right)\right)\Rightarrow \mathrm{lt}\left(\mathrm{execute}\left(high,\mathrm{take}\left(xs,p\right),\mathrm{initial}\left(high,model\right)\right),\mathrm{pastState}\left(\mathrm{uPadding}\left(\mathrm{executionWord}\left(xs\right)\right),\mathrm{castInt}\left(\mathrm{length}\left(\mathrm{executionWord}\left(\mathrm{take}\left(xs,p\right)\right)\right)\right)\right)\right)\right)\wedge \left(\mathrm{member}\left(\mathrm{uPadding}\left(\mathrm{executionWord}\left(xs\right)\right),\mathrm{AuxiliaryLanguage}\left(K,d\right)\right)\wedge \left(\mathrm{Occurs}\left(\mathrm{uPadding}\left(\mathrm{executionWord}\left(xs\right)\right),\mathrm{executionWord}\left(xs\right)\right)\wedge \left(\mathrm{AuxiliaryFactor}\left(K,d,\mathrm{executionWord}\left(xs\right)\right)\wedge \mathrm{wordWeight}\left(\mathrm{executionWord}\left(xs\right)\right)=\mathrm{listWeight}\left(xs\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For K at least one, any real guard d and either actual initial model, a weakly guarded complete return list has its exact execution word at the origin of uPadding. This sequence equals that finite word at nonnegative positions inside it, and equals u at every other integer position. Its infinite-past state at zero is h_H. At every complete return boundary its state strictly exceeds the state of the original actual recurrence. Every c position is located in an original return; the intervening positive u runs prevent a K-letter guard from crossing a return boundary. The cap excludes K+1 consecutive c letters, and the weak actual guard transfers to the independent before-Kth-c auxiliary guard. The exact finite word occurs at zero and is an AuxiliaryFactor, with weight equal to listWeight. Combined directly with the existing complete execution parser, this supplies an injection of exact-weight weak complete lists into distinct occurrence factors. Empty lists are included. The auxiliary u tails do not replace either original eventually-empty literal source or its zero-error future. castInt is the natural-to-integer inclusion.

Theorem 1.2 (Strict actual completion of every c-containing occurrence factor).

$$\forall o\in Ownership,b\in Real,K\in Nat,\left(\mathrm{le}\left(2,K\right)\wedge \left(\mathrm{lt}\left(\mathrm{subtract}\left(lam,\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{hSide}\left(high\right)\right)\right),b\right)\wedge \mathrm{lt}\left(b,\mathrm{subtract}\left(lam,\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{divide}\left(\mathrm{aSide}\left(high\right),\mathrm{subtract}\left(1,\mathrm{multiply}\left(rho,\mathrm{power}\left(chi,K\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists R\in Return,r\left(R\right)=1\wedge \left(\forall model\in Model,w\in \mathrm{List}\left(CuLetter\right),\left(\mathrm{AuxiliaryFactor}\left(K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right),w\right)\wedge \mathrm{member}\left(c,w\right)\right)\Rightarrow \left(\exists a\in Nat,first\in Return,rest\in \mathrm{List}\left(Return\right),\mathrm{if}\left(\mathrm{getLastOption}\left(w\right)=\mathrm{some}\left(c\right),\mathrm{append}\left(w,\mathrm{singleton}\left(u\right)\right),w\right)=\mathrm{append}\left(\mathrm{replicate}\left(a,u\right),\mathrm{executionWord}\left(\mathrm{cons}\left(first,rest\right)\right)\right)\wedge \left(\left(\forall ap\in Nat,xp\in \mathrm{List}\left(Return\right),\mathrm{if}\left(\mathrm{getLastOption}\left(w\right)=\mathrm{some}\left(c\right),\mathrm{append}\left(w,\mathrm{singleton}\left(u\right)\right),w\right)=\mathrm{append}\left(\mathrm{replicate}\left(ap,u\right),\mathrm{executionWord}\left(xp\right)\right)\Rightarrow \left(ap=a\wedge xp=\mathrm{cons}\left(first,rest\right)\right)\right)\wedge \left(\mathrm{ActualPairSupply}\left(model,o,b,strict,\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(R\right),a\right),1\right),\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(first\right),1\right),r\left(first\right)\right),rest\right)\right)\right)\wedge \left(\mathrm{executionWord}\left(\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(R\right),a\right),1\right),\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(first\right),1\right),r\left(first\right)\right),rest\right)\right)\right)=\mathrm{cons}\left(c,\mathrm{append}\left(\mathrm{replicate}\left(\mathrm{add}\left(m\left(R\right),a\right),u\right),\mathrm{append}\left(\mathrm{replicate}\left(r\left(first\right),c\right),\mathrm{append}\left(\mathrm{replicate}\left(\mathrm{add}\left(m\left(first\right),1\right),u\right),\mathrm{executionWord}\left(rest\right)\right)\right)\right)\right)\wedge \mathrm{listWeight}\left(\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(R\right),a\right),1\right),\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(first\right),1\right),r\left(first\right)\right),rest\right)\right)\right)=\mathrm{add}\left(\mathrm{add}\left(\mathrm{wordWeight}\left(w\right),\mathrm{add}\left(20,\mathrm{multiply}\left(6,m\left(R\right)\right)\right)\right),\mathrm{if}\left(\mathrm{getLastOption}\left(w\right)=\mathrm{some}\left(c\right),12,6\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

One fixed reset R has r equal to one. For either actual model and every independently occurring factor containing c, append one terminal u precisely when its last letter is c. The filled word has a unique leading u run of length a followed by first and rest positive returns. Merge that leading run into the reset by replacing its m with R.m+a; add one u after the first visible c-run by replacing first.m with first.m+1. The resulting complete list strictly supplies the original actual paired sources, with all endpoint flags, stems, paid anchor and unchanged zero-error futures. The proof uses the occurrence guards, the reset output bound and the original first-return strict output dominance. Subsequent common transitions strictly preserve dominance. Truncated first and last runs, a low first return and first equal to last are all included; no common family margin follows.

Serialization is the displayed normal form c u^(R.m+a) c^first.r u^(first.m+1) executionWord(rest). The exact weight overhead is 20+6R.m+6 for an original u ending and 20+6R.m+12 for an original c ending. Return(m,r) in the formula specifies the two positive exponents; the Lean constructors include their positivity proofs. This theorem proves actual membership and the unique run decomposition, not a finite-cardinality count or a rate.

Theorem 1.3 (Actual equal-weight source addresses determine their lists).

$$\forall j\in Side,model\in Model,xs\in \mathrm{List}\left(Return\right),ys\in \mathrm{List}\left(Return\right),\left(\mathrm{listWeight}\left(xs\right)=\mathrm{listWeight}\left(ys\right)\wedge \mathrm{source}\left(j,model,xs\right)=\mathrm{source}\left(j,model,ys\right)\right)\Rightarrow xs=ys$$

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

Source. Repository-derived.

Commentary.

For either actual side and either model, two return lists of the same variable weight have equal full eventually-empty source addresses only if the lists are equal. Equality of addresses determines the finite observed prefixes because their original lengths coincide. Removing the same stem and paid anchor leaves equal external label words. On the high side U and C have different second labels; on the low side V and C have different first labels. The label-block encoding is therefore uniquely recoverable. Reversing the execution-letter order preserves the letters inside each original block, and the existing complete execution parser recovers the return list. The two literal tails remain unchanged. This is a statement about literal addresses; it does not assert injectivity of the scalar coordinate or establish an asymptotic rate.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Completion.actual_source_address_injection
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Completion.auxiliary_factor_upper_completion
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Completion.auxiliary_lower_padding
• Dependency: D5/S3/ConceptDynamics/Coding/DecoderOperationTrace
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Bilateral
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ClosedSupply
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/StrictSupply