Reset codebooks on one bilateral realization

Abstract

A common reset and exact weighted gain support finite actual records and bilateral lower-memory realizations.

Definition 1.1 (forwardCut).

$$\forall W\in Int\to \mathrm{List}\left(CuLetter\right),\mathrm{forwardCut}\left(W,0\right)=0\wedge \left(\forall n\in Nat,\mathrm{forwardCut}\left(W,\mathrm{add}\left(n,1\right)\right)=\mathrm{add}\left(\mathrm{forwardCut}\left(W,n\right),\mathrm{toInt}\left(\mathrm{length}\left(\mathrm{apply}\left(W,\mathrm{toInt}\left(n\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.forwardCut (✓ std3).

Source. Repository-derived.

Commentary.

Forward cuts add the next block’s positive letter length.

Definition 1.2 (backwardCut).

$$\forall W\in Int\to \mathrm{List}\left(CuLetter\right),\mathrm{backwardCut}\left(W,0\right)=0\wedge \left(\forall n\in Nat,\mathrm{backwardCut}\left(W,\mathrm{add}\left(n,1\right)\right)=\mathrm{add}\left(\mathrm{backwardCut}\left(W,n\right),\mathrm{toInt}\left(\mathrm{length}\left(\mathrm{apply}\left(W,\mathrm{negate}\left(\mathrm{add}\left(\mathrm{toInt}\left(n\right),1\right)\right)\right)\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.backwardCut (✓ std3).

Source. Repository-derived.

Commentary.

Backward cuts sum the blocks at indices minus one, minus two and so on.

Definition 1.3 (blockCut).

$$\forall W\in Int\to \mathrm{List}\left(CuLetter\right),\left(\forall n\in Nat,\mathrm{blockCut}\left(W,\mathrm{toInt}\left(n\right)\right)=\mathrm{forwardCut}\left(W,n\right)\right)\wedge \left(\forall n\in Nat,\mathrm{blockCut}\left(W,\mathrm{negSucc}\left(n\right)\right)=\mathrm{negate}\left(\mathrm{backwardCut}\left(W,\mathrm{add}\left(n,1\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.blockCut (✓ std3).

Source. Repository-derived.

Commentary.

The origin is fixed. Negative cuts use the negative backward sum; negSucc(n) denotes minus n minus one.

Theorem 1.4 (positive block tiling).

$$\forall W\in Int\to \mathrm{List}\left(CuLetter\right),\left(\forall j\in Int,\mathrm{lt}\left(0,\mathrm{length}\left(\mathrm{apply}\left(W,j\right)\right)\right)\right)\Rightarrow \left(\left(\mathrm{blockCut}\left(W,0\right)=0\wedge \left(\left(\forall j\in Int,\mathrm{blockCut}\left(W,\mathrm{add}\left(j,1\right)\right)=\mathrm{add}\left(\mathrm{blockCut}\left(W,j\right),\mathrm{toInt}\left(\mathrm{length}\left(\mathrm{apply}\left(W,j\right)\right)\right)\right)\right)\wedge \mathrm{StrictMono}\left(\mathrm{blockCut}\left(W\right)\right)\right)\right)\wedge \left(\exists omega\in Int\to CuLetter,\forall j\in Int,k\in \mathrm{Fin}\left(\mathrm{length}\left(\mathrm{apply}\left(W,j\right)\right)\right),\mathrm{apply}\left(omega,\mathrm{add}\left(\mathrm{blockCut}\left(W,j\right),\mathrm{toInt}\left(k\right)\right)\right)=\mathrm{getElem}\left(\mathrm{apply}\left(W,j\right),k\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Every indexed family of nonempty words determines disjoint consecutive block intervals covering all integer letter positions. Each prescribed letter belongs to one bilateral sequence, even when block letter lengths vary.

Theorem 1.5 (execute seed difference).

$$\forall xs\in \mathrm{List}\left(Return\right),x\in Real,y\in Real,\mathrm{subtract}\left(\mathrm{execute}\left(high,xs,y\right),\mathrm{execute}\left(high,xs,x\right)\right)=\mathrm{multiply}\left(\mathrm{power}\left(g,\mathrm{listWeight}\left(xs\right)\right),\mathrm{subtract}\left(y,x\right)\right)$$

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

Source. Repository-derived.

Commentary.

The original literal affine maps give the exact gain g raised to the original list weight. Positive return exponents make that weight even.

Theorem 1.6 (exact guard gain).

$$\forall K\in Nat,N\in Nat,d\in Real,B\in Real,model\in Model,xs\in \mathrm{List}\left(Return\right),E\in Real,\left(\mathrm{GuardTrace}\left(K,d,false,high,xs,\mathrm{initial}\left(high,model\right)\right)\wedge \left(\mathrm{listWeight}\left(xs\right)=N\wedge \left(\mathrm{lt}\left(\mathrm{initial}\left(high,model\right),B\right)\wedge \mathrm{le}\left(B,E\right)\right)\right)\right)\Rightarrow \left(\mathrm{GuardTrace}\left(K,\mathrm{add}\left(d,\mathrm{multiply}\left(\mathrm{subtract}\left(B,\mathrm{initial}\left(high,model\right)\right),\mathrm{power}\left(g,N\right)\right)\right),false,high,xs,E\right)\wedge \mathrm{lt}\left(\mathrm{aSide}\left(high\right),\mathrm{execute}\left(high,xs,E\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

An initial gain at least B minus the original initial displacement remains at least that gain times g to the full word weight at every high return prefix. The same execution also stays above the original lower boundary.

Theorem 1.7 (reset codebook construction).

$$\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),\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)\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,\mathrm{lt}\left(0,N\right)\Rightarrow \left(\mathrm{lt}\left(0,\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)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\wedge \left(\mathrm{lt}\left(0,\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{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right),2\right)\right)\wedge \left(\left(\forall targetModel\in Model,words\in \mathrm{List}\left(\mathrm{Subtype}\left({\left(\mathrm{GuardTrace}\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),false,high,xs,\mathrm{initial}\left(high,sourceModel\right)\right)\wedge \mathrm{listWeight}\left(xs\right)=N\right)}_{xs\in \mathrm{List}\left(Return\right)}\right)\right),\mathrm{GuardTrace}\left(K,\mathrm{add}\left(\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),\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right),false,high,\mathrm{resetConcatenation}\left(R,\mathrm{map}\left(val,words\right)\right),\mathrm{initial}\left(high,targetModel\right)\right)\wedge \mathrm{ActualPairSupply}\left(targetModel,o,\mathrm{subtract}\left(b,\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{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right),2\right)\right),strict,\mathrm{resetConcatenation}\left(R,\mathrm{map}\left(val,words\right)\right)\right)\right)\wedge \left(\left(\exists n\in Nat,\mathrm{le}\left(K,n\right)\wedge \mathrm{lt}\left(\mathrm{multiply}\left(\mathrm{hSide}\left(high\right),\mathrm{power}\left(rho,n\right)\right),\mathrm{multiply}\left(\mathrm{power}\left(chi,\mathrm{subtract}\left(K,1\right)\right),\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right)\right)\wedge \left(\forall choices\in Int\to \mathrm{Subtype}\left({\left(\mathrm{GuardTrace}\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),false,high,xs,\mathrm{initial}\left(high,sourceModel\right)\right)\wedge \mathrm{listWeight}\left(xs\right)=N\right)}_{xs\in \mathrm{List}\left(Return\right)}\right),\left(\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},0\right)=0\wedge \left(\left(\forall j\in Int,\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},\mathrm{add}\left(j,1\right)\right)=\mathrm{add}\left(\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right),\mathrm{toInt}\left(\mathrm{length}\left(\mathrm{apply}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right)\right)\right)\right)\right)\wedge \mathrm{StrictMono}\left(\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int}\right)\right)\right)\right)\wedge \left(\exists omega\in Int\to CuLetter,\forall j\in Int,k\in \mathrm{Fin}\left(\mathrm{length}\left(\mathrm{apply}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right)\right)\right),\mathrm{apply}\left(omega,\mathrm{add}\left(\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right),\mathrm{toInt}\left(k\right)\right)\right)=\mathrm{getElem}\left(\mathrm{apply}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right),k\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The codebook subtype contains all weak original execution lists of weight N. One low reset R is fixed before both models and all weights. Its floor B is h minus rho to m(R) times h minus chi A; delta is B minus the selected original initial displacement and gamma is delta times g to N. Every finite joint choice has the exact high guard d plus gamma and the displayed common actual error margin. The margin uses the original automatic-slot bound, and the literal zero-error futures are included in ActualPairSupply. The two-sided symbolic tiling uses exactly the same reset blocks.

Definition 1.8 (blockWindow).

$$\forall W\in Int\to \mathrm{List}\left(CuLetter\right),a\in Int,\mathrm{blockWindow}\left(W,a,0\right)=\mathrm{nil}\left(\right)\wedge \left(\forall n\in Nat,\mathrm{blockWindow}\left(W,a,\mathrm{add}\left(n,1\right)\right)=\mathrm{append}\left(\mathrm{apply}\left(W,a\right),\mathrm{blockWindow}\left(W,\mathrm{add}\left(a,1\right),n\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.blockWindow (✓ std3).

Source. Repository-derived.

Commentary.

A finite window concatenates the blocks at a through a+n-1 in increasing execution order.

Theorem 1.9 (block window positions).

$$\forall W\in Int\to \mathrm{List}\left(CuLetter\right),a\in Int,n\in Nat,\left(\forall j\in Int,\mathrm{lt}\left(0,\mathrm{length}\left(\mathrm{apply}\left(W,j\right)\right)\right)\right)\Rightarrow \left(\mathrm{toInt}\left(\mathrm{length}\left(\mathrm{blockWindow}\left(W,a,n\right)\right)\right)=\mathrm{subtract}\left(\mathrm{blockCut}\left(W,\mathrm{add}\left(a,\mathrm{toInt}\left(n\right)\right)\right),\mathrm{blockCut}\left(W,a\right)\right)\wedge \left(\forall j\in Nat,k\in Nat,\left(\mathrm{lt}\left(j,n\right)\wedge \mathrm{lt}\left(k,\mathrm{length}\left(\mathrm{apply}\left(W,\mathrm{add}\left(a,\mathrm{toInt}\left(j\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{getD}\left(\mathrm{getElemOption}\left(\mathrm{blockWindow}\left(W,a,n\right),\mathrm{add}\left(\mathrm{toNat}\left(\mathrm{subtract}\left(\mathrm{blockCut}\left(W,\mathrm{add}\left(a,\mathrm{toInt}\left(j\right)\right)\right),\mathrm{blockCut}\left(W,a\right)\right)\right),k\right)\right),u\right)=\mathrm{getD}\left(\mathrm{getElemOption}\left(\mathrm{apply}\left(W,\mathrm{add}\left(a,\mathrm{toInt}\left(j\right)\right)\right),k\right),u\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The finite window has precisely the difference of its endpoint cuts as its length. Each internal block letter occurs at the cut difference plus its local index.

Theorem 1.10 (compact block tiling).

$$\forall K\in Nat,d\in Real,W\in Int\to \mathrm{List}\left(CuLetter\right),\left(\mathrm{le}\left(1,K\right)\wedge \left(\left(\forall j\in Int,\mathrm{lt}\left(0,\mathrm{length}\left(\mathrm{apply}\left(W,j\right)\right)\right)\right)\wedge \left(\forall a\in Int,n\in Nat,\mathrm{member}\left(\mathrm{uPadding}\left(\mathrm{blockWindow}\left(W,a,n\right)\right),\mathrm{AuxiliaryLanguage}\left(K,d\right)\right)\right)\right)\right)\Rightarrow \left(\exists omega\in Int\to CuLetter,\mathrm{member}\left(omega,\mathrm{AuxiliaryLanguage}\left(K,d\right)\right)\wedge \left(\forall j\in Int,k\in \mathrm{Fin}\left(\mathrm{length}\left(\mathrm{apply}\left(W,j\right)\right)\right),\mathrm{apply}\left(omega,\mathrm{add}\left(\mathrm{blockCut}\left(W,j\right),\mathrm{toInt}\left(k\right)\right)\right)=\mathrm{getElem}\left(\mathrm{apply}\left(W,j\right),k\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Centered finite block windows, shifted to their prescribed cuts, lie in one compact auxiliary language. A convergent subsequence preserves every eventually fixed block letter and the same closed guard. The result is one bilateral realization of the entire two-sided choice.

Definition 1.11 (LowerMemoryLanguage).

$$\forall n\in Nat,K\in Nat,d\in Real,omega\in Int\to CuLetter,\mathrm{member}\left(omega,\mathrm{LowerMemoryLanguage}\left(n,K,d\right)\right)\iff \left(\left(\forall i\in Int,\mathrm{not}\left(\forall q\in \mathrm{Fin}\left(\mathrm{add}\left(K,1\right)\right),\mathrm{apply}\left(omega,\mathrm{add}\left(i,\mathrm{toInt}\left(q\right)\right)\right)=c\right)\right)\wedge \left(\forall i\in Int,\left(\forall q\in \mathrm{Fin}\left(K\right),\mathrm{apply}\left(omega,\mathrm{subtract}\left(i,\mathrm{toInt}\left(q\right)\right)\right)=c\right)\Rightarrow \mathrm{lt}\left(\mathrm{multiply}\left(\mathrm{power}\left(chi,\mathrm{subtract}\left(K,1\right)\right),d\right),\mathrm{finitePast}\left(omega,i,n,0\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.LowerMemoryLanguage (✓ std3).

Source. Repository-derived.

Commentary.

The lower graph forbids K+1 consecutive c letters and checks the zero-seed past before the current Kth c transition. Membership retains the original strict inequality and the original high-edge timing.

Theorem 1.12 (uniform guard lower memory).

$$\forall omega\in Int\to CuLetter,n\in Nat,K\in Nat,d\in Real,gamma\in Real,\left(\mathrm{member}\left(omega,\mathrm{AuxiliaryLanguage}\left(K,\mathrm{add}\left(d,gamma\right)\right)\right)\wedge \mathrm{lt}\left(\mathrm{multiply}\left(\mathrm{hSide}\left(high\right),\mathrm{power}\left(rho,n\right)\right),\mathrm{multiply}\left(\mathrm{power}\left(chi,\mathrm{subtract}\left(K,1\right)\right),gamma\right)\right)\right)\Rightarrow \mathrm{member}\left(omega,\mathrm{LowerMemoryLanguage}\left(n,K,d\right)\right)$$

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

Source. Repository-derived.

Commentary.

The bilateral state exceeds its zero-seed n-past by at most h times rho to n. A common state margin larger than that error gives every strict lower-graph guard on the same sequence.

Definition 1.13 (choiceWindow).

$$\forall V\in Type,choices\in Int\to V,a\in Int,\mathrm{choiceWindow}\left(choices,a,0\right)=\mathrm{nil}\left(\right)\wedge \left(\forall n\in Nat,\mathrm{choiceWindow}\left(choices,a,\mathrm{add}\left(n,1\right)\right)=\mathrm{cons}\left(\mathrm{apply}\left(choices,a\right),\mathrm{choiceWindow}\left(choices,\mathrm{add}\left(a,1\right),n\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.choiceWindow (✓ std3).

Source. Repository-derived.

Commentary.

A finite window of indexed choices keeps their order and their actual subtype membership.

Theorem 1.14 (bilateral reset codebook).

$$\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),\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)\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,\mathrm{lt}\left(0,N\right)\Rightarrow \left(\mathrm{lt}\left(0,\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)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\wedge \left(\mathrm{lt}\left(0,\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{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right),2\right)\right)\wedge \left(\left(\forall targetModel\in Model,words\in \mathrm{List}\left(\mathrm{Subtype}\left({\left(\mathrm{GuardTrace}\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),false,high,xs,\mathrm{initial}\left(high,sourceModel\right)\right)\wedge \mathrm{listWeight}\left(xs\right)=N\right)}_{xs\in \mathrm{List}\left(Return\right)}\right)\right),\mathrm{GuardTrace}\left(K,\mathrm{add}\left(\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),\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right),false,high,\mathrm{resetConcatenation}\left(R,\mathrm{map}\left(val,words\right)\right),\mathrm{initial}\left(high,targetModel\right)\right)\wedge \mathrm{ActualPairSupply}\left(targetModel,o,\mathrm{subtract}\left(b,\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{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right),2\right)\right),strict,\mathrm{resetConcatenation}\left(R,\mathrm{map}\left(val,words\right)\right)\right)\right)\wedge \left(\exists n\in Nat,\mathrm{le}\left(K,n\right)\wedge \left(\mathrm{lt}\left(\mathrm{multiply}\left(\mathrm{hSide}\left(high\right),\mathrm{power}\left(rho,n\right)\right),\mathrm{multiply}\left(\mathrm{power}\left(chi,\mathrm{subtract}\left(K,1\right)\right),\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right)\wedge \left(\forall choices\in Int\to \mathrm{Subtype}\left({\left(\mathrm{GuardTrace}\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),false,high,xs,\mathrm{initial}\left(high,sourceModel\right)\right)\wedge \mathrm{listWeight}\left(xs\right)=N\right)}_{xs\in \mathrm{List}\left(Return\right)}\right),\exists omega\in Int\to CuLetter,\mathrm{member}\left(omega,\mathrm{AuxiliaryLanguage}\left(K,\mathrm{add}\left(\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),\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right)\right)\right)\wedge \left(\mathrm{member}\left(omega,\mathrm{LowerMemoryLanguage}\left(n,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)\right)\right)\wedge \left(\left(\forall j\in Int,k\in \mathrm{Fin}\left(\mathrm{length}\left(\mathrm{apply}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right)\right)\right),\mathrm{apply}\left(omega,\mathrm{add}\left(\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right),\mathrm{toInt}\left(k\right)\right)\right)=\mathrm{getElem}\left(\mathrm{apply}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\right),k\right)\right)\wedge \left(\forall j\in Int,\mathrm{GuardTrace}\left(K,\mathrm{add}\left(\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),\mathrm{multiply}\left(\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),\mathrm{power}\left(g,N\right)\right)\right),false,high,\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right),\mathrm{pastState}\left(omega,\mathrm{blockCut}\left({\left(\mathrm{executionWord}\left(\mathrm{cons}\left(R,\mathrm{val}\left(\mathrm{apply}\left(choices,j\right)\right)\right)\right)\right)}_{j\in Int},j\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/ResetCodebook.bilateral_reset_codebook (✓ std3). ∎

Source. Repository-derived.

Commentary.

One reset floor exceeds both actual initial states and d. For the full weak equal-weight original codebook, the finite actual supply retains the positive displayed half-minimum error margin. Fix delta and gamma first and then choose n at least K with h rho to n less than chi to K-1 times gamma. Every two-sided choice uses that same reset and has one bilateral sequence in AuxiliaryLanguage at d plus gamma and in the original lower-memory language at d. Every reset block occurs at its prescribed cut, and its complete return trace on that same sequence has high-start margin gamma. Thus the before-Kth-c state margin is chi to K-1 times delta times g to N. The weighted factor-count and factor-rate conclusions follow from the counting argument.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.LowerMemoryLanguage
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.backwardCut
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.bilateral_reset_codebook
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.blockCut
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.blockWindow
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.block_window_positions
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.choiceWindow
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.compact_block_tiling
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.exact_guard_gain
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.execute_seed_difference
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.forwardCut
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.positive_block_tiling
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.reset_codebook_construction
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook.uniform_guard_lower_memory
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FibonacciFactorCompletion