Same-reset weighted factor dictionaries
Abstract
The original equal-weight weak codebook has distinct factors in one lower-memory language, with exact reset overhead and a weighted limsup bound.
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 (FactorDictionary).
Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.FactorDictionary (✓ std3).
Source. Repository-derived.
Commentary.
The dictionary contains every word of exact original weight T that occurs in a bilateral sequence of X. Occurrence retains a single sequence and one integer starting position; transient graph paths are not substituted.
Definition 1.2 (factorCount).
Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.factorCount (✓ std3).
Source. Repository-derived.
Commentary.
The count is the natural cardinality of that entire factor dictionary, including the empty word at weight zero when the language is nonempty.
Definition 1.3 (weightedFactorRate).
Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.weightedFactorRate (✓ std3).
Source. Repository-derived.
Commentary.
The rate is the real upper limit over total actual weight T, with max(1,count) and total real division at T=0. It uses the original weights 20 and 6, rather than letter length.
Definition 1.4 (resetFactor).
Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.resetFactor (✓ std3).
Source. Repository-derived.
Commentary.
Every finite ordered choice receives the same original reset before its execution word. Flattening concatenates these words without prescribing a common letter length.
Theorem 1.5 (word weight geometry).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.word_weight_geometry (✓ std3). ∎
Source. Repository-derived.
Commentary.
Original letter weights are positive and additive. A zero-weight word is empty; letter length is bounded by its actual weight.
Theorem 1.6 (factor dictionary bound).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.factor_dictionary_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Every word of weight T has at most T letters. Its optional letters at the first T+1 indices determine it uniquely, giving a finite dictionary and the bound 3 to T+1.
Theorem 1.7 (equal weight concatenation injective).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.equal_weight_concatenation_injective (✓ std3). ∎
Source. Repository-derived.
Commentary.
At each common accumulated positive weight, prefix comparison recovers the next whole block. This proves unique parsing with variable block letter lengths; equality of weights never asserts equality of lengths.
Theorem 1.8 (reset factor parser).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.reset_factor_parser (✓ std3). ∎
Source. Repository-derived.
Commentary.
The existing complete execution-word parser identifies each original return list after the fixed reset is removed. Equal weighted cuts identify the ordered choices. No reset exponent restriction is needed here; the weight includes the actual r(R).
Theorem 1.9 (tiled window occurs).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.tiled_window_occurs (✓ std3). ∎
Source. Repository-derived.
Commentary.
The indexed tiling supplies every letter of each consecutive finite block window at its original integer cut. All blocks, including the negative-index past, belong to the same bilateral realization.
Theorem 1.10 (choice window ofFn).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.choice_window_ofFn (✓ std3). ∎
Source. Repository-derived.
Commentary.
The recursive finite choice window equals the list of choices at consecutive integer indices a through a+q-1.
Theorem 1.11 (factor rate of power count).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.factor_rate_of_power_count (✓ std3). ∎
Source. Repository-derived.
Commentary.
The finite alphabet supplies a uniform bound on the real logarithmic quotients. Counts at all multiples of a positive L give a frequent lower bound and hence the weighted limsup bound. Empty and singleton codebooks have the displayed zero lower bound.
Theorem 1.12 (same reset factor cardinality).
Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.same_reset_factor_cardinality (✓ std3). ∎
Source. Repository-derived.
Commentary.
One reset with r=1 has floor B above both actual initial states and d, and is fixed before both source models and all N>0. For the full weak codebook, delta=B-D0 and gamma=delta times g to N. Every finite choice has high guard d+gamma and actual strict supply with the positive half-minimum error margin, including the original zero-error futures. The same reset admits every bilateral choice on one sequence with all block guards, in one lower-memory language n chosen after the fixed codebook. Here n is at least K and h rho to n is below chi to K-1 times gamma. For every q, the choice map is injective, its exact-weight image has cardinality a to q, and every image word extends bilaterally in that same lower language. The resulting weighted rate is at least log base two of max(1,a), divided by N+20+6m(R). Positive accumulated-weight cuts recover the choices even when their letter lengths differ. The empty choice q=0 uses the all-u sequence.
References
- Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.FactorDictionary - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.choice_window_ofFn - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.equal_weight_concatenation_injective - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.factorCount - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.factor_dictionary_bound - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.factor_rate_of_power_count - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.resetFactor - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.reset_factor_parser - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.same_reset_factor_cardinality - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.tiled_window_occurs - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.weightedFactorRate - Truth anchor:
D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetFactors.word_weight_geometry - Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/ResetCodebook