Hereditary Finiteness of Zeckendorf Set Codes
Abstract
Hereditary Finiteness of Zeckendorf Set Codes.
Theorem 1.1 (Preservation and reflection of hereditary finiteness).
Lean statement: D5/S0/History/Spacetime/AllSetZeckendorfHereditaryFiniteness.enc_isHF_iff
Proof. Machine-checked in Lean as D5/S0/History/Spacetime/AllSetZeckendorfHereditaryFiniteness.enc_isHF_iff (✓ std3). ∎
Source. Repository-derived.
Commentary.
In any universe, a set has rank less than omega if and only if its recursive Zeckendorf encoding has rank less than omega. Natural leaves are pairs of finite ordinals and finite digit graphs. For every other set, the encoding pairs tag one with the encodings of its members. Membership induction and injectivity transfer finiteness of the member set in both directions.