Actual complete counts on all even lengths

Abstract

The raw logarithms of actual strict and weak complete-list counts equal eta_b times the literal weight plus a little-o error on all even weights. Actual histories and both literal sources retain the same coefficient at the original observation offsets twenty-six and fifty-two.

Shared notation

The following functions abbreviate exactly the displayed expressions. Every occurrence uses the arguments shown, within the scope of the same quantified parameters and witnesses. Expanding these definitions recovers all guards, weights and shared margins.

$\forall b\in Real,K\in Nat,d\left(b,K\right)=\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)$

$\forall R\in Return,sourceModel\in Model,\mathrm{delta}\left(R,sourceModel\right)=\mathrm{subtract}\left(\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(\mathrm{power}\left(rho,m\left(R\right)\right),\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(chi,\mathrm{aSide}\left(high\right)\right)\right)\right)\right),\mathrm{initial}\left(high,sourceModel\right)\right)$

$\forall R\in Return,sourceModel\in Model,N\in Nat,\mathrm{gamma}\left(R,sourceModel,N\right)=\mathrm{multiply}\left(\mathrm{delta}\left(R,sourceModel\right),\mathrm{power}\left(g,N\right)\right)$

$\forall R\in Return,sourceModel\in Model,b\in Real,K\in Nat,N\in Nat,\mathrm{epsilon}\left(R,sourceModel,b,K,N\right)=\mathrm{divide}\left(\min \left(\mathrm{subtract}\left(b,\mathrm{actualAutomaticCost}\left(K\right)\right),\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{gamma}\left(R,sourceModel,N\right)\right)\right),2\right)$

$\forall R\in Return,N\in Nat,\mathrm{blockWeight}\left(R,N\right)=\mathrm{add}\left(\mathrm{add}\left(N,20\right),\mathrm{multiply}\left(6,m\left(R\right)\right)\right)$

$\forall sourceModel\in Model,b\in Real,K\in Nat,N\in Nat,\mathrm{weakBook}\left(sourceModel,b,K,N\right)=\mathrm{Subtype}\left((xs:\mathrm{List}\left(Return\right)\mapsto \mathrm{GuardTrace}\left(K,d\left(b,K\right),false,high,xs,\mathrm{initial}\left(high,sourceModel\right)\right)\wedge \mathrm{listWeight}\left(xs\right)=N)\right)$

Return lists are in execution order from the literal tail outward. Their literal weights are six times m plus twenty times r. The two models start at X_H and Y_H on the high side and at the corresponding X_L and Y_L on the low side. All source supplies use the original U/V and C blocks, the same stems and paid anchors, and the original literal tails. The external source reverses the return list without reversing the labels inside any block. Natural-number division and subtraction below use the natural quotient and truncated subtraction.

The weak complete-list count uses the non-strict high guard. It corresponds to the closed source contract when the nearest high endpoint is owned, o(0)=true; otherwise the closed contract uses the strict high guard. The strict and recordMargin source contracts always use the strict high guard.

Definition 1.1 (fillerJ).

$$\forall F\in Nat,\mathrm{fillerJ}\left(F\right)=\mathrm{ifThenElse}\left(\mathrm{mod}\left(\mathrm{divide}\left(F,2\right),3\right)=0,3,\mathrm{mod}\left(\mathrm{divide}\left(F,2\right),3\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.fillerJ (✓ std3).

Source. Repository-derived.

Commentary.

The residue zero is represented by three; the other two residues are represented by one and two.

Definition 1.2 (fillerQ).

$$\forall F\in Nat,\mathrm{fillerQ}\left(F\right)=\mathrm{divide}\left(\mathrm{subtract}\left(\mathrm{divide}\left(F,2\right),\mathrm{multiply}\left(13,\mathrm{fillerJ}\left(F\right)\right)\right),3\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.fillerQ (✓ std3).

Source. Repository-derived.

Commentary.

For even F at least seventy-eight, the numerator is nonnegative and divisible by three.

Definition 1.3 (lowReturn).

$$\forall q\in Nat,m\left(\mathrm{lowReturn}\left(q\right)\right)=\mathrm{add}\left(1,q\right)\wedge r\left(\mathrm{lowReturn}\left(q\right)\right)=1$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.lowReturn (✓ std3).

Source. Repository-derived.

Commentary.

This is the positive return (1+q,1), of literal weight twenty-six plus six times q.

Definition 1.4 (lowFiller).

$$\forall F\in Nat,\mathrm{lowFiller}\left(F\right)=\mathrm{cons}\left(\mathrm{lowReturn}\left(\mathrm{fillerQ}\left(F\right)\right),\mathrm{replicate}\left(\mathrm{subtract}\left(\mathrm{fillerJ}\left(F\right),1\right),\mathrm{lowReturn}\left(0\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.lowFiller (✓ std3).

Source. Repository-derived.

Commentary.

The first return carries all additional six-letter blocks. The remaining j-1 returns are (1,1). This one filler depends only on F.

Theorem 1.5 (actual list weight even).

$$\forall xs\in \mathrm{List}\left(Return\right),\mathrm{Even}\left(\mathrm{listWeight}\left(xs\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every summand six times m plus twenty times r is even. The empty list has weight zero.

Theorem 1.6 (low filler geometry).

$$\forall F\in Nat,\left(\mathrm{Even}\left(F\right)\wedge \mathrm{le}\left(78,F\right)\right)\Rightarrow \left(\mathrm{le}\left(1,\mathrm{fillerJ}\left(F\right)\right)\wedge \left(\mathrm{le}\left(\mathrm{fillerJ}\left(F\right),3\right)\wedge \left(\left(\forall i\in Nat,\left(\mathrm{le}\left(1,i\right)\wedge \left(\mathrm{le}\left(i,3\right)\wedge \mathrm{mod}\left(\mathrm{divide}\left(F,2\right),3\right)=\mathrm{mod}\left(i,3\right)\right)\right)\Rightarrow i=\mathrm{fillerJ}\left(F\right)\right)\wedge \left(\mathrm{mod}\left(\mathrm{divide}\left(F,2\right),3\right)=\mathrm{mod}\left(\mathrm{fillerJ}\left(F\right),3\right)\wedge \left(\mathrm{le}\left(\mathrm{multiply}\left(13,\mathrm{fillerJ}\left(F\right)\right),\mathrm{divide}\left(F,2\right)\right)\wedge \left(\mathrm{dvd}\left(3,\mathrm{subtract}\left(\mathrm{divide}\left(F,2\right),\mathrm{multiply}\left(13,\mathrm{fillerJ}\left(F\right)\right)\right)\right)\wedge \left(\mathrm{add}\left(\mathrm{multiply}\left(26,\mathrm{fillerJ}\left(F\right)\right),\mathrm{multiply}\left(6,\mathrm{fillerQ}\left(F\right)\right)\right)=F\wedge \left(\mathrm{listWeight}\left(\mathrm{lowFiller}\left(F\right)\right)=F\wedge \left(\left(\forall a\in Return,\mathrm{member}\left(a,\mathrm{lowFiller}\left(F\right)\right)\Rightarrow r\left(a\right)=1\right)\wedge \left(\forall K\in Nat,\mathrm{le}\left(2,K\right)\Rightarrow \left(\forall d\in Real,strict\in Bool,side\in Side,D\in Real,\mathrm{GuardTrace}\left(K,d,strict,side,\mathrm{lowFiller}\left(F\right),D\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For F=2v at least seventy-eight, v is at least thirty-nine. The unique representative j lies between one and three, so 13j is at most v. Dividing v-13j by three gives q and the exact weight 26j+6q=F. Every return has r=1<K, hence its guard passes for either strictness flag, either side and every input displacement. The three smallest residues are F=78 with (j,q)=(3,0), F=80 with (1,9), and F=82 with (2,5).

Definition 1.7 (paddingCopies).

$$\forall L\in Nat,T\in Nat,\mathrm{paddingCopies}\left(L,T\right)=\mathrm{divide}\left(\mathrm{subtract}\left(T,78\right),L\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.paddingCopies (✓ std3).

Source. Repository-derived.

Commentary.

The number of complete reset codewords is the quotient of T-78 by L.

Definition 1.8 (paddingWeight).

$$\forall L\in Nat,T\in Nat,\mathrm{paddingWeight}\left(L,T\right)=\mathrm{subtract}\left(T,\mathrm{multiply}\left(\mathrm{paddingCopies}\left(L,T\right),L\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.paddingWeight (✓ std3).

Source. Repository-derived.

Commentary.

The remainder includes the reserved seventy-eight units for the outer filler.

Theorem 1.9 (even padding arithmetic).

$$\forall L\in Nat,T\in Nat,\left(\mathrm{lt}\left(0,L\right)\wedge \left(\mathrm{Even}\left(L\right)\wedge \left(\mathrm{le}\left(78,T\right)\wedge \mathrm{Even}\left(T\right)\right)\right)\right)\Rightarrow \left(\mathrm{Even}\left(\mathrm{paddingWeight}\left(L,T\right)\right)\wedge \left(\mathrm{le}\left(78,\mathrm{paddingWeight}\left(L,T\right)\right)\wedge \left(\mathrm{lt}\left(\mathrm{paddingWeight}\left(L,T\right),\mathrm{add}\left(78,L\right)\right)\wedge \mathrm{add}\left(\mathrm{multiply}\left(\mathrm{paddingCopies}\left(L,T\right),L\right),\mathrm{paddingWeight}\left(L,T\right)\right)=T\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The exact decomposition is T=kL+F with even F in [78,78+L). At T=78, k is zero. At T=78+L, k is one and F returns to seventy-eight.

Theorem 1.10 (reset execution word).

$$\forall R\in Return,words\in \mathrm{List}\left(\mathrm{List}\left(Return\right)\right),\mathrm{executionWord}\left(\mathrm{resetConcatenation}\left(R,words\right)\right)=\mathrm{resetFactor}\left(R,words\right)$$

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

Source. Repository-derived.

Commentary.

Reading the execution letters after concatenating reset-prefixed return lists gives exactly the concatenation of their reset-prefixed letter words. Thus the equal-weight reset parser applies to the original actual return lists.

Definition 1.11 (paddedExecution).

$$\forall R\in Return,words\in \mathrm{List}\left(\mathrm{List}\left(Return\right)\right),F\in Nat,\mathrm{paddedExecution}\left(R,words,F\right)=\mathrm{append}\left(\mathrm{resetConcatenation}\left(R,words\right),\mathrm{lowFiller}\left(F\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.paddedExecution (✓ std3).

Source. Repository-derived.

Commentary.

The filler follows all codewords in execution order. It therefore precedes the original codeword list in the external source, on its outer side.

Theorem 1.12 (same reset all even counts).

$$\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(\mathrm{lt}\left(\max \left(\max \left(\mathrm{xSide}\left(high\right),\mathrm{ySide}\left(high\right)\right),d\left(b,K\right)\right),\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(\mathrm{power}\left(rho,m\left(R\right)\right),\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(chi,\mathrm{aSide}\left(high\right)\right)\right)\right)\right)\right)\wedge \left(\forall sourceModel\in Model,N\in Nat,\left(\mathrm{lt}\left(0,N\right)\wedge \mathrm{le}\left(1,\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right)\right)\right)\Rightarrow \left(\mathrm{Even}\left(N\right)\wedge \left(\mathrm{Even}\left(\mathrm{blockWeight}\left(R,N\right)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{blockWeight}\left(R,N\right)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{delta}\left(R,sourceModel\right)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{gamma}\left(R,sourceModel,N\right)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{epsilon}\left(R,sourceModel,b,K,N\right)\right)\wedge \left(\forall targetModel\in Model,T\in Nat,\left(\mathrm{le}\left(78,T\right)\wedge \mathrm{Even}\left(T\right)\right)\Rightarrow \left(\left(\mathrm{Even}\left(\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\wedge \left(\mathrm{le}\left(78,\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\wedge \left(\mathrm{lt}\left(\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right),\mathrm{add}\left(78,\mathrm{blockWeight}\left(R,N\right)\right)\right)\wedge \mathrm{add}\left(\mathrm{multiply}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right),\mathrm{blockWeight}\left(R,N\right)\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)=T\right)\right)\right)\wedge \left(\mathrm{Injective}\left((z:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\to \mathrm{weakBook}\left(sourceModel,b,K,N\right)\mapsto \mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right))\right)\wedge \left(\left(\forall z\in \mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\to \mathrm{weakBook}\left(sourceModel,b,K,N\right),\mathrm{listWeight}\left(\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right)=T\wedge \left(\mathrm{GuardTrace}\left(K,\mathrm{add}\left(d\left(b,K\right),\mathrm{gamma}\left(R,sourceModel,N\right)\right),false,high,\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right),\mathrm{initial}\left(high,targetModel\right)\right)\wedge \left(\mathrm{ActualPairSupply}\left(targetModel,o,\mathrm{subtract}\left(b,\mathrm{epsilon}\left(R,sourceModel,b,K,N\right)\right),strict,\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right)\wedge \left(\left(\forall contract\in Contract,\mathrm{ActualPairSupply}\left(targetModel,o,b,contract,\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right)\right)\wedge \left(\left(\forall before\in \mathrm{List}\left(Return\right),a\in Return,after\in \mathrm{List}\left(Return\right),\left(\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)=\mathrm{append}\left(before,\mathrm{cons}\left(a,after\right)\right)\wedge r\left(a\right)=K\right)\Rightarrow \left(\exists rest\in \mathrm{List}\left(Return\right),\mathrm{resetConcatenation}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right)\right)=\mathrm{append}\left(before,\mathrm{cons}\left(a,rest\right)\right)\right)\right)\wedge \left(\forall side\in Side,\mathrm{externalWord}\left(side,\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right)=\mathrm{append}\left(\mathrm{externalWord}\left(side,\mathrm{lowFiller}\left(\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right),\mathrm{externalWord}\left(side,\mathrm{resetConcatenation}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\wedge \left(\left(\left(\forall strict\in Bool,\mathrm{le}\left(\mathrm{power}\left(\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right),\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right),\mathrm{actualCount}\left(targetModel,K,d\left(b,K\right),strict,T\right)\right)\right)\wedge \left(\forall contract\in Contract,\mathrm{le}\left(\mathrm{power}\left(\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right),\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right),\mathrm{contractCount}\left(targetModel,o,b,contract,T\right)\right)\right)\right)\wedge \left(\mathrm{Injective}\left((z:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\to \mathrm{weakBook}\left(sourceModel,b,K,N\right)\mapsto \mathrm{history}\left(targetModel,\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right))\right)\wedge \left(\forall side\in Side,\mathrm{Injective}\left((z:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\to \mathrm{weakBook}\left(sourceModel,b,K,N\right)\mapsto \mathrm{source}\left(side,targetModel,\mathrm{paddedExecution}\left(R,\mathrm{ofFn}\left((i:\mathrm{Fin}\left(\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\mapsto \mathrm{val}\left(\mathrm{apply}\left(z,i\right)\right))\right),\mathrm{paddingWeight}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right)\right))\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The budget inequalities fix d=(lambda-b)/(g squared times chi to K). One low reset R is fixed before all source models and all N. Its floor B exceeds X_H, Y_H and d. For the full nonempty weak exact-N codebook, delta=B-D0, gamma=delta times g to N, and epsilon is half the minimum of b-C_auto and g squared times chi to K times gamma. Nonemptiness gives even N from an actual list, so L=N+20+6m(R) is positive and even. Append the same filler to every k-tuple. Every old high return has exactly its old execution prefix, while all filler returns are low. The original actual supply at b-epsilon extends to the same literal sources and zero-error futures. Cancelling the common filler and applying the reset parser with positive cumulative-weight cuts recovers all choices even when codeword letter lengths differ. The resulting exact-T actual dictionaries, every source contract, the color histories and both literal source sides all preserve those distinct choices.

Theorem 1.13 (odd actual counts).

$$\forall T\in Nat,\mathrm{Odd}\left(T\right)\Rightarrow \left(\left(\forall model\in Model,K\in Nat,d\in Real,strict\in Bool,\mathrm{actualCount}\left(model,K,d,strict,T\right)=0\right)\wedge \left(\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,\mathrm{contractCount}\left(model,o,b,contract,T\right)=0\right)\right)$$

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

Source. Repository-derived.

Commentary.

No list of positive actual returns can have odd literal weight. Every strict, weak and source-contract dictionary at an odd weight is empty.

Theorem 1.14 (even actual positivity).

$$\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(\forall T\in Nat,\left(\mathrm{Even}\left(T\right)\wedge \mathrm{le}\left(78,T\right)\right)\Rightarrow \left(\mathrm{listWeight}\left(\mathrm{lowFiller}\left(T\right)\right)=T\wedge \left(\left(\forall model\in Model,contract\in Contract,\mathrm{ActualPairSupply}\left(model,o,b,contract,\mathrm{lowFiller}\left(T\right)\right)\wedge \mathrm{lt}\left(0,\mathrm{contractCount}\left(model,o,b,contract,T\right)\right)\right)\wedge \left(\forall model\in Model,strict\in Bool,\mathrm{lt}\left(0,\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,T\right)\right)\wedge \mathrm{actualLogRate}\left(model,K,d\left(b,K\right),strict,T\right)=\mathrm{divide}\left(\mathrm{logb}\left(2,\mathrm{toReal}\left(\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,T\right)\right)\right),\mathrm{toReal}\left(T\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The standalone low filler is strictly feasible from both models and supplies all original contracts. Every raw even count is positive at T at least seventy-eight. On this range, positivity permits max-one normalization to be removed from the logarithm.

Theorem 1.15 (full even floor ratio).

$$\forall L\in Nat,\left(\mathrm{lt}\left(0,L\right)\wedge \mathrm{Even}\left(L\right)\right)\Rightarrow \mathrm{Tendsto}\left((v:Nat\mapsto \mathrm{divide}\left(\mathrm{toReal}\left(\mathrm{paddingCopies}\left(L,\mathrm{multiply}\left(2,v\right)\right)\right),\mathrm{toReal}\left(\mathrm{multiply}\left(2,v\right)\right)\right)),atTop,\mathrm{nhds}\left(\mathrm{divide}\left(1,\mathrm{toReal}\left(L\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The bounded filler weight divided by T tends to zero on all T=2v. The exact decomposition kL+F=T gives k/T tending to 1/L on this full even filter.

Theorem 1.16 (original finite even bridge).

$$\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(\left(\forall T\in Nat,\mathrm{Odd}\left(T\right)\Rightarrow \left(\left(\forall model\in Model,strict\in Bool,\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,T\right)=0\right)\wedge \left(\forall model\in Model,contract\in Contract,\mathrm{contractCount}\left(model,o,b,contract,T\right)=0\right)\right)\right)\wedge \left(\left(\forall T\in Nat,\left(\mathrm{Even}\left(T\right)\wedge \mathrm{le}\left(78,T\right)\right)\Rightarrow \left(\mathrm{listWeight}\left(\mathrm{lowFiller}\left(T\right)\right)=T\wedge \left(\left(\forall model\in Model,contract\in Contract,\mathrm{ActualPairSupply}\left(model,o,b,contract,\mathrm{lowFiller}\left(T\right)\right)\wedge \mathrm{lt}\left(0,\mathrm{contractCount}\left(model,o,b,contract,T\right)\right)\right)\wedge \left(\forall model\in Model,strict\in Bool,\mathrm{lt}\left(0,\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,T\right)\right)\wedge \mathrm{actualLogRate}\left(model,K,d\left(b,K\right),strict,T\right)=\mathrm{divide}\left(\mathrm{logb}\left(2,\mathrm{toReal}\left(\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,T\right)\right)\right),\mathrm{toReal}\left(T\right)\right)\right)\right)\right)\right)\wedge \left(\exists R\in Return,r\left(R\right)=1\wedge \left(\mathrm{lt}\left(\max \left(\max \left(\mathrm{xSide}\left(high\right),\mathrm{ySide}\left(high\right)\right),d\left(b,K\right)\right),\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(\mathrm{power}\left(rho,m\left(R\right)\right),\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(chi,\mathrm{aSide}\left(high\right)\right)\right)\right)\right)\right)\wedge \left(\forall sourceModel\in Model,N\in Nat,\left(\mathrm{lt}\left(0,N\right)\wedge \mathrm{le}\left(1,\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right)\right)\right)\Rightarrow \left(\mathrm{Even}\left(N\right)\wedge \left(\mathrm{Even}\left(\mathrm{blockWeight}\left(R,N\right)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{blockWeight}\left(R,N\right)\right)\wedge \left(\left(\forall targetModel\in Model,T\in Nat,\left(\mathrm{le}\left(78,T\right)\wedge \mathrm{Even}\left(T\right)\right)\Rightarrow \left(\left(\forall strict\in Bool,\mathrm{le}\left(\mathrm{power}\left(\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right),\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right),\mathrm{actualCount}\left(targetModel,K,d\left(b,K\right),strict,T\right)\right)\right)\wedge \left(\forall contract\in Contract,\mathrm{le}\left(\mathrm{power}\left(\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right),\mathrm{paddingCopies}\left(\mathrm{blockWeight}\left(R,N\right),T\right)\right),\mathrm{contractCount}\left(targetModel,o,b,contract,T\right)\right)\right)\right)\right)\wedge \left(\forall targetModel\in Model,strict\in Bool,\mathrm{le}\left(\mathrm{divide}\left(\mathrm{logb}\left(2,\mathrm{toReal}\left(\mathrm{actualCount}\left(sourceModel,K,d\left(b,K\right),false,N\right)\right)\right),\mathrm{toReal}\left(\mathrm{blockWeight}\left(R,N\right)\right)\right),\mathrm{liminf}\left((v:Nat\mapsto \mathrm{actualLogRate}\left(targetModel,K,d\left(b,K\right),strict,\mathrm{multiply}\left(2,v\right)\right)),atTop\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Odd counts vanish, and all even raw counts are positive from weight seventy-eight onward. The same reset works for every fixed nonempty full weak codebook, for both target starts and both guard flags. Its exact-T power counts imply the normalized full-even liminf is at least log base two of a_N divided by N+C_R. The fixed-codebook bound holds on the entire even-weight filter. Positive-count codebook slopes approaching eta_b therefore bound this same liminf from below.

Theorem 1.17 (actual even raw asymptotics).

$$\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(\forall model\in Model,strict\in Bool,\mathrm{Tendsto}\left((v:Nat\mapsto \mathrm{divide}\left(\mathrm{logb}\left(2,\mathrm{toReal}\left(\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,\mathrm{multiply}\left(2,v\right)\right)\right)\right),\mathrm{toReal}\left(\mathrm{multiply}\left(2,v\right)\right)\right)),atTop,\mathrm{nhds}\left(\mathrm{etaB}\left(K,b\right)\right)\right)\wedge \mathrm{IsLittleO}\left(atTop,(v:Nat\mapsto \mathrm{subtract}\left(\mathrm{logb}\left(2,\mathrm{toReal}\left(\mathrm{actualCount}\left(model,K,d\left(b,K\right),strict,\mathrm{multiply}\left(2,v\right)\right)\right)\right),\mathrm{multiply}\left(\mathrm{etaB}\left(K,b\right),\mathrm{toReal}\left(\mathrm{multiply}\left(2,v\right)\right)\right)\right)),(v:Nat\mapsto \mathrm{toReal}\left(\mathrm{multiply}\left(2,v\right)\right))\right)\right)$$

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

Source. Repository-derived.

Commentary.

Fix one reset of the all-even construction before choosing any source weight or target model. An unbounded positive-count sequence of original weak actual dictionaries has raw slope log2(a_N)/N tending to eta_b. For this exact fixed reset, N/(N+C_R) tends to one, so its codebook slopes also tend to eta_b. The full-even liminf is at least every one of these slopes for both target models and both guard flags. Boundedness of the original normalized sequence gives a full-even limsup at most its unrestricted limsup eta_b. The two bounds give the limit. The actual low filler makes every raw count positive at even T at least seventy-eight; only there is max-one normalization removed. Subtracting eta_b from the raw quotient gives zero limit, exactly the stated little-o error.

Definition 1.18 (ObservedContractDictionary).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\mathrm{ObservedContractDictionary}\left(model,o,b,contract,Nobs\right)=\mathrm{Subtype}\left((xs:\mathrm{List}\left(Return\right)\mapsto \mathrm{ActualPairSupply}\left(model,o,b,contract,xs\right)\wedge \mathrm{length}\left(\mathrm{history}\left(model,xs\right)\right)=Nobs)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.ObservedContractDictionary (✓ std3).

Source. Repository-derived.

Commentary.

The indexing length is the length of the original color history. The underlying list has the original ActualPairSupply contract, including both source sides and their literal zero-error futures.

Definition 1.19 (ActualHistoryImage).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\mathrm{ActualHistoryImage}\left(model,o,b,contract,Nobs\right)=\mathrm{range}\left((xs:\mathrm{ObservedContractDictionary}\left(model,o,b,contract,Nobs\right)\mapsto \mathrm{history}\left(model,\mathrm{val}\left(xs\right)\right))\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.ActualHistoryImage (✓ std3).

Source. Repository-derived.

Commentary.

This set contains exactly the original color histories obtained from the actual contract lists at the specified departure length.

Definition 1.20 (ActualSourceImage).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\forall side\in Side,\mathrm{ActualSourceImage}\left(side,model,o,b,contract,Nobs\right)=\mathrm{range}\left((xs:\mathrm{ObservedContractDictionary}\left(model,o,b,contract,Nobs\right)\mapsto \mathrm{source}\left(side,model,\mathrm{val}\left(xs\right)\right))\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.ActualSourceImage (✓ std3).

Source. Repository-derived.

Commentary.

The image uses the original full literal source constructor on a chosen side. Its prefix includes the original stem and the paid anchor precisely when the model is anchored; its tail is the prescribed original tail.

Definition 1.21 (ActualSourcePairImage).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\mathrm{ActualSourcePairImage}\left(model,o,b,contract,Nobs\right)=\mathrm{range}\left((xs:\mathrm{ObservedContractDictionary}\left(model,o,b,contract,Nobs\right)\mapsto \mathrm{pair}\left(\mathrm{source}\left(high,model,\mathrm{val}\left(xs\right)\right),\mathrm{source}\left(low,model,\mathrm{val}\left(xs\right)\right)\right))\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.ActualSourcePairImage (✓ std3).

Source. Repository-derived.

Commentary.

The high and low sources are constructed from the same execution list and share its color history. The two respective literal future tails are retained.

Definition 1.22 (historyImageCount).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\mathrm{historyImageCount}\left(model,o,b,contract,Nobs\right)=\mathrm{card}\left(\mathrm{ActualHistoryImage}\left(model,o,b,contract,Nobs\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.historyImageCount (✓ std3).

Source. Repository-derived.

Commentary.

This is the cardinality of the actual history image at observation length Nobs.

Definition 1.23 (sourceImageCount).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\forall side\in Side,\mathrm{sourceImageCount}\left(side,model,o,b,contract,Nobs\right)=\mathrm{card}\left(\mathrm{ActualSourceImage}\left(side,model,o,b,contract,Nobs\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/EvenLengthAsymptotics.sourceImageCount (✓ std3).

Source. Repository-derived.

Commentary.

This is the cardinality of one actual full-source image at observation length Nobs.

Definition 1.24 (sourcePairImageCount).

$$\forall model\in Model,o\in Ownership,b\in Real,contract\in Contract,Nobs\in Nat,\mathrm{sourcePairImageCount}\left(model,o,b,contract,Nobs\right)=\mathrm{card}\left(\mathrm{ActualSourcePairImage}\left(model,o,b,contract,Nobs\right)\right)$$