Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Actual boundaries for Fibonacci completion

Abstract

Both actual Fibonacci starts retain the complete-boundary, closed and strict source laws and one finite actual reset map.

Theorem 1.1 (Closed supply and owned high-guard equality).

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

Source. Repository-derived.

Commentary.

For either fixed original or anchored source pair, closed acquisition is equivalent to the cap and high guard. Owning the first cut point permits equality; otherwise the high guard is strict. The proof assembles all departure errors on those same literal sources, through every six- and twenty-slot repetition, stem and paid anchor, and extends them by zero on the unchanged original futures. The proof applies the original affine suffix law, interval existence and finite normalization locally at those actual inputs; its twenty-slot errors are the strict witnesses weakened to the closed bound. High equality uses the owned nearest point from the actual clipped readout law. The complete block application is given in the Literal source exposition. The paired low costs are strictly smaller. All five flags remain parameters, and returns beyond the cap fail at the actual control slot.

Theorem 1.2 (One paid actual reset and first-return output dominance).

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

Source. Repository-derived.

Commentary.

A single positive finite reset length M gives B_M greater than X_H, Y_H and d. Its actual input above A gives output strictly above B_M; an input at least A gives the stated weak bound. Prepending this same reset to any weakly guarded complete list from either actual start supplies the complete paired record strictly from either target start, including the stems, anchor and original zero-error futures. The weight increases by exactly 20+6M. The exact first-run insertion identity gives strict output dominance after one added u for every original m,r,z in the stated domain. This extra u follows the first visible c-run even when it is low; no undiminished reset margin is assigned to a later return.

References