Zeckendorf FST — Mathlib peel plan

• Parent: README.md
• Math sandbox: MATH_SANDBOX.md

ZeckendorfFST.lean is a large mechanized development that now has import Init only (no Mathlib). Earlier peels removed Mathlib.Tactic.Ring and Mathlib.Data.List.Basic; list lemmas use Init.Data.List (including List.replicate_succ'), and omega is the core arithmetic tactic. Proofs that previously used Mathlib-only conveniences were rewritten (set → let, conv_lhs → conv => lhs; …, by_contra → Nat.le_of_not_lt + order lemmas).

Target architecture (maintenance)

1. Keep the file Mathlib-free: avoid reintroducing import Mathlib.* so ForkRaceFoldTheorems.ZeckendorfFST stays in the Init-only import-closure roots (see init-only-import-closure.json).
2. Tactics: prefer omega / simp / explicit Nat lemmas; avoid ring and Mathlib tactic imports.
3. Shared list material: if Zeckendorf and GnosisMath.ListNat overlap, factor into GnosisMath rather than duplicating — optional, not required for Zeckendorf to compile.

Promotion rule

Mathlib is no longer a blocker for hub integration: the module’s import closure is Init-only. Whether to import it from MathSandbox remains a hub-size / narrative decision (large surface area), not a Mathlib dependency decision.