Pisot Vickrey Table — Mathlib peel notes

• Parent: README.md
• Related: ZECKENDORF_FST_PEEL.md, MATH_SANDBOX.md

PisotVickreyTable.lean formalizes the φ-indexed Vickrey / Pisot lattice story (Fibonacci tower, skip/doubling, Cassini parity, bounded Zeckendorf wire-length witnesses).

Done

• Mathlib.Tactic.Ring removed. Tensor-style equalities use simp with Nat.mul_assoc / Nat.mul_left_comm; linear index arithmetic uses omega; the heavy induction step in phi_product_pair closes with nlinarith instead of ring.

Still Mathlib (heritage)

• Mathlib.Tactic.Linarith — linarith / nlinarith (including Cassini branches and phi_product_pair succ case).
• Mathlib.Data.Nat.Log — statements use Nat.log 2 n in bounded wire-length theorems.
• Mathlib.Tactic.IntervalCases — pisot_decoder_total_bounded enumerates small n.

Target

Replace Nat.log 2 with Nat.log2 where semantics align, peel interval_cases into explicit fin_cases/cases for fixed small ranges, and reduce linarith to omega where goals stay linear — then re-audit import closure for a possible Init-only root (same machinery as validate-init-only-import-closure.mjs).