Ordered Zeckendorf Paths and the Inversion Potential

Abstract

Concrete greedy continuation, weighted split promotion and finite cascade exchanges.

A state is one list of natural-number raw W indices. Decode maps each index through successor to the positive paper indices; n zeros thus represent n ones. Multiplicities are obtained through Multiset.toFinsupp. Move records the position of its adjacent window and one of five actions: an inversion switch, combining ones, splitting twos, a general split, or a consecutive merge. No predecessor map is used.

Theorem 1.1 (Concrete greedy continuation attains its reward).

$$\forall c,\exists d,RawGreedyPath\left(c,d,G\left(c\right)\right)\wedge CanonicalRaw\left(d\right)$$

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.greedy_attainment (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite raw multiplicity state, the concrete continuation G is attained by a finite RawGreedyPath to binary nonadjacent digits. Each decision combines ones first, otherwise splits the highest duplicate, otherwise merges the least occupied consecutive pair. Priority is recomputed after every move. G recurses on the existing strict carry measure and is not defined as a maximum over paths. Labels remain data. This establishes raw attainment, not the comparison with competitors or ordered LGS completion.

Theorem 1.2 (Every complete raw greedy path has the same reward).

$$RawGreedyPath\left(c,e,w\right)\wedge CanonicalRaw\left(e\right)\Rightarrow w=G\left(c\right)$$

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.complete_greedy_reward (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every complete raw path obeying the stated priorities has reward G at its initial state. Legality and priority determine the first action and successor uniquely: ones exclude every other preferred action, otherwise the highest duplicate fixes the split, and a binary state fixes the least consecutive merge. Induction along the actual path then agrees with the recursive continuation. A canonical endpoint admits no carry. This equality covers all complete RawGreedyPath witnesses; it does not compare an arbitrary legal competitor with G.

Theorem 1.3 (All five shared-input merge repairs).

Lean statement: D5/S1/Digit/Carry/OrderedGame.shared_input_merge_repair

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.shared_input_merge_repair (✓ std3). ∎

Source. Repository-derived.

Commentary.

With unrestricted spectators, a legal merge sharing an input with an enabled split has a split-first legal path to the exact merge endpoint. If the lower input is duplicated it is split first; otherwise the upper input is split. In positive paper indices the lower-input detours are S1;S2, S2;S3;S1, and Sa;S(a+1);C(a-2), with gains c1-1, 2c2+c1-2, and 2c(a-1)+2ca-2. The upper-input detours are S2;S1 at a=1, gaining zero, and S(a+1);C(a-1) at a>=2, gaining one. The theorem gives exact reward equality with a natural-number gain. Replacement tails are legal; no greedy-tail assertion is made.

Theorem 1.4 (Ones first against arbitrary interleaved terminal paths).

$$RawPath\left(c,e,w\right)\wedge CanonicalRaw\left(e\right)\wedge SplitStep\left(0,c,cPrime\right)\Rightarrow \exists v,RawPath\left(cPrime,e,v\right)\wedge w\le splitReward\left(c,0\right)+v$$

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.ones_terminal_promotion (✓ std3). ∎

Source. Repository-derived.

Commentary.

If combining ones is enabled, every raw path to binary nonadjacent digits can be replaced by one beginning with that split, retaining its endpoint and at least its full reward. The competing path may interleave merges and splits arbitrarily. The proof promotes ones through split steps, repairs a merge consuming a one, and commutes past higher merges. This closes the ones-first promotion branch. The dependent Optimality module supplies the nonzero-split and least-binary-merge comparisons inside its complete raw terminal bound.

Theorem 1.5 (Promote the preferred split through the actual initial split phase).

Lean statement: D5/S1/Digit/Carry/OrderedGame.split_greedy_terminal_promotion

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.split_greedy_terminal_promotion (✓ std3). ∎

Source. Repository-derived.

Commentary.

A competing split followed by a complete raw greedy path admits a legal replacement beginning with the currently highest split, with the same terminal endpoint and at least its reward. The proof cuts the actual greedy continuation immediately before its first merge, or at its canonical endpoint. The cut state is binary. Only that complete WeightedSplitPath is passed to split_phase_promotion; the entire remaining raw suffix is preserved. No split-only comparison is applied across merges.

Theorem 1.6 (Finite high cascade and boundary-independent legal replay).

Lean statement: D5/S1/Digit/Carry/OrderedGame.high_cascade

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.high_cascade (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive raw k, assume holes at k and k+1, at most two tokens at k+2, binary digits above k+2 and at most one zero. A finite greedy split cascade makes the tail at and above k binary and preserves all lower coordinates. Finite support supplies the first zero; induction on its distance proves the coordinate invariant. Every split has unit reward. The same word replays from any state agreeing strictly above k, with the same reward and exact additive endpoint balance. Lower coordinates in the replay are unrestricted; its moves are not asserted to be greedy.

Theorem 1.7 (Erasure preserves the complete reward).

$$Path\left(s,t,length,weight\right)\Rightarrow RawPath\left(rawCounts\left(s\right),rawCounts\left(t\right),weight\right)$$

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.path_raw_erasure (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite legal ordered path erases to a labelled raw path with exactly the same accumulated reward. Switches preserve multiplicities and contribute zero reward. Each remaining label retains its actual CarryStep and its consumed and produced digits in the same spectator context. Labels are explicit and are not reconstructed from an unlabelled proposition. The theorem neither assumes terminality nor asserts optimality.

Theorem 1.8 (The path potential bound).

$$Path\left(s,t,length,weight\right)\Rightarrow length+inv\left(decode\left(t\right)\right)\le inv\left(decode\left(s\right)\right)+weight$$

Proof. Machine-checked in Lean as D5/S1/Digit/Carry/OrderedGame.path_potential (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every finite legal path, actual move count plus final inversions is at most initial inversions plus summed carry reward. Switch reward is zero. In positive indices the other rewards are c1-1, c2-1, c(i-1)+ci-1 for a split at i greater than two, and c(a+1) for a merge at a. Thus rewards include the carry itself. The proof telescopes the existing four local inversion bounds; a switch removes exactly one inversion. There is no terminality or strategy assumption.

LGSPath keeps every permitted inversion-switch choice. Its priority restarts after every move: switches, leftmost ones, rightmost split, then leftmost consecutive merge. Conjecture17 records nonvacuous complete LGS existence for every positive n and the comparison of every complete LGS run with every legal terminal competitor. Its proof is OrderedGame/Completion.result, which combines these path bounds with ordered attainment, raw greedy optimality and finite completion.

References

• Truth anchor: D5/S1/Digit/Carry/OrderedGame.complete_greedy_reward
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.greedy_attainment
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.high_cascade
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.ones_terminal_promotion
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.path_potential
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.path_raw_erasure
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.shared_input_merge_repair
• Truth anchor: D5/S1/Digit/Carry/OrderedGame.split_greedy_terminal_promotion
• Dependency: D5/S1/Digit/Carry/ListInversions
• Dependency: D5/S1/Digit/Carry/SplitStabilization
• Dependency: D5/S1/Digit/Raw