The formally encoded scalar spectral gap

FORM.SPECTRALGAP.01

Original ledger classification: Formal [F] (Lean kernel; no extra axioms) -- the scalar core + the finite-dimensional diagonalisable case of the spectral-gap meta-theorem (v383): gap => unique attractor + geometric decay => parameter-free

Original claim text

LEAN 4 FORMALISATION of the SCALAR CORE of the universal spectral-gap principle (door #4, 2026-06-24) -- new module TfptCarrier/SpectralGapAttractor.lean, lake build OK (target TfptCarrier.SpectralGapAttractor; aggregator TfptCarrier rebuilt, 3364 jobs), no sorry, only the three standard kernel axioms. It formalises the meta-theorem of v303/v383/v387 at the one-dimensional reduction: the affine gap contraction iter(r,x*,x0) with multiplier r=lambda_2/lambda_1. [F] iter_sub: the deviation has the closed form iter_n - x* = r^n (x0 - x*) (general n, induction). [F] iter_tendsto: 0<=r<1 (the spectral gap) => iter_n -> x* (the unique attractor), via Mathlib tendsto_pow_atTop_nhds_zero_of_lt_one. [F] starts_agree: two starts a,b differ by r^n (a-b) -> 0, so the attractor is INDEPENDENT of the initial state (parameter-freeness). [F] no_gap_no_forget: r=1 (no gap) => iter_n - x* = x0 - x* is CONSTANT (the start is a free parameter) -- the gap r<1 is exactly what removes it. [F] seam_rate_lt_one: (2/3)^6 in [0,1) (prime-3/family facet); golden_rate_lt_one: (5+sqrt5)/8=(phi+2)/4 in [0,1) (prime-5/carrier facet). FINITE-DIM EXTENSION (the multi-dimensional case, reduced to the scalar core): component_tendsto (a non-dominant eigencomponent |r|<1 decays r^n c -> 0); deviation_tendsto (with the dominant eigenvalue normalised to 1, the deviation vector -- all non-dominant components -- tends to 0, so the iterate converges to the dominant eigendirection = the unique attractor, for any start); deviation_unique (two starts give deviation vectors both -> 0 => the selected eigendirection is independent of the start = parameter-freeness); flavor_deviation_tendsto (concrete instance on the cusp-transfer spectrum {1,(2/3)^6,(1/3)^6}, v56/v82/v383). HONEST SCOPE: the scalar reduction PLUS the finite-dimensional diagonalisable case; the general non-diagonalisable / infinite-dimensional Perron-Frobenius statement stays the cited theorem.

Original classification detail

Formal: iter_sub (closed form r^n), iter_tendsto (gap => attractor), starts_agree (parameter-freeness), no_gap_no_forget (gap is essential), seam/golden rates in [0,1); PLUS the finite-dim case (component_tendsto, deviation_tendsto = convergence to the dominant eigendirection, deviation_unique = parameter-free, flavor_deviation_tendsto on {1,(2/3)^6,(1/3)^6}); the general non-diagonalisable / infinite-dim PF stays cited

Dependencies as recorded

DYNAMICS.UNIVERSAL.01; CORRECTIONS.GAP.01; FR.DYNAMICS.01