Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual codebooks and the lower rate limit

Abstract

Actual complete low words have positive rate, and codebooks from the original weak limsup approximate that rate with one fixed reset. The original lower-memory rates converge increasingly to the same value.

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.

Definition 1.1 (lowReturns).

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/LowerRateLimit.lowReturns (✓ std3).

Source. Repository-derived.

Commentary.

The false choice is the complete return list (1,1),(2,1), and the true choice is (2,1),(1,1). Both m and r are positive. Their execution words are exactly c u c u u and c u u c u, and each has weight 58. Execution goes from the original tail toward the outside; the literal source uses the reversed list and retains each original block’s label order.

Definition 1.2 (lowChoices).

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/LowerRateLimit.lowChoices (✓ std3).

Source. Repository-derived.

Commentary.

Flatten the chosen complete lists in their finite execution order. The empty choice has the empty list and weight zero. Both actual initial models retain their original high and low tails, with observation offsets 26 and 52.

Theorem 1.3 (actual low choice count).

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

Source. Repository-derived.

Commentary.

Every return has r=1<K, so every finite choice is strictly legal from either actual start. The actual paired-source supply includes the common prescribed history, all departure slots, and each original tail with zero future error. Positive weighted cuts and the complete execution parser recover every binary choice; the original history parser also distinguishes them. There are at least 2 to q strict lists and at least as many weak lists at weight 58q, including q=0 and q=1.

Theorem 1.4 (actual rate positive).

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

Source. Repository-derived.

Commentary.

Actual counts at unbounded multiples of 58 give a frequent normalized logarithmic lower bound of 1/58. This is the original actual rate for both starts and both guard flags, rather than a rate per letter. Ownership is arbitrary and does not enter this rate or the budget inequalities.

Definition 1.5 (FixedCodebook).

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/LowerRateLimit.FixedCodebook (✓ std3).

Source. Repository-derived.

Commentary.

The dictionary contains every original weak list of exact weight N. Its reset floor B, delta=B-D0, gain=delta times g to N, and positive half-minimum error are kept together. All finite actual choices share the strengthened guard and the strict budget b-error, with original zero-error futures. One memory n is selected after that entire fixed dictionary and satisfies n>=K and h rho to n<chi to K-1 times gain. Every bilateral choice has one sequence for its auxiliary membership, lower-memory membership, tiling at every integer cut, and all block guards. These auxiliary infinite sequences are distinct from the finite actual sources. For every q, positive cumulative-weight cuts give an injective choice map, its exact-weight image, cardinality a to q and bilateral occurrence in that same lower language. These conditions characterize the displayed proposition.

Theorem 1.6 (original count codebook approximation).

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

Source. Repository-derived.

Commentary.

One reset is selected before either source model or any weight. The bounded original weak logarithmic sequence has a limsup sequence tending to infinity. Actual positivity makes its weights and counts positive after discarding only a finite prefix. Thus max(1,count) equals count throughout the retained sequence. The ratio N/(N+20+6m(R)) tends to one, so both the raw normalized logarithm and the fixed-overhead codebook slope tend to eta_b. Each codebook retains its complete finite actual and bilateral package; its common margin is obtained before its memory is selected.

Theorem 1.7 (original lower rate limit).

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

Source. Repository-derived.

Commentary.

For any positive epsilon, fix one codebook whose slope exceeds eta_b-epsilon, then select its memory n_j. Lower-memory monotonicity preserves that bound for every n>=max(K,n_j). The actual-to-auxiliary rate equality gives the common upper bound eta_b, so the lower rates increase to eta_b. The nested-language theorem supplies the same actual eta_b for the upper rates, which decrease to eta_b. One original root family records both exact MemoryLanguage sides on n>=K, their radius-one equations and rate identities, the lower and upper root monotonicities, and the natural lower n+K shift. It also retains the actual rate equality for both models and both strictness flags. Codebook margins may shrink as N grows; the statement selects memory separately for each fixed codebook. Ownership is arbitrary and does not enter these rates, roots or budget inequalities.

References