The singular slow space Vⱼ — unconditional on the tempered class (Wave-5, Angle 5A)

For a possibly-singular (non-invertible) matrix cocycle generator A : X → Matrix (Fin d) (Fin d) ℝ, the intermediate slow space Vⱼ(ω) of the singular forward Oseledets filtration (Quas, MET and Applications, 2013, Theorem 2; Ruelle, Publ. IHES 50, 1979, Lemma 1.4) is — by the landed structural reduction Oseledets.tendsto_orthProjMatrix_vSlowSingularStep_of_tendsto_bandProjector (SingularSlowSpace.lean) — reduced unconditionally to a single input: convergence of the fast band projector bandProjector A T (𝟙_{(c,∞)}) n x at a Lyapunov cut c. That band convergence follows by the root test from any per-step increment upper bound b n with (1/n)·log b n → L < 0. This module supplies that — with the negative log-limit obtained from the a.e.-constant genuine singular spectrum's strict gap at the cut (SingularSpectrumConstant.lean, via Oseledets.ae_singularSpectralValue_eq_const) — and pins, with cruxStatus-quality precision, exactly which hypothesis the resulting Vⱼ carries.

What Wave-5 establishes, and the precise residual

The forward-ratio crack (Angle 5A) sought a det-free, inverse-free per-step bound

(R5A) ‖P_slow(n+1) − P_slow(n)‖ ≤ C · σ_{k+1}(M_{n+1}) / σ_k(M_{n+1}),

M_{n+1} = cocycle (n+1) x, controlling the slow increment by a forward singular-value ratio of the single cocycle M_{n+1} (no inverse). We record (bandProjector_increment_eq_aperture, a statement-level identity, not a proof of a false claim) that (R5A) is false at the per-step granularity: the band increment ‖P_slow(n+1) − P_slow(n)‖ is the aperture sin∠(S_n, S_{n+1}) between the top-k right-singular spaces of M_n and M_{n+1} = B·M_n (B = A(Tⁿx)); a single ill-conditioned step B (with σ_k(B) small, k < d, det B possibly 0) can rotate S_n by an O(1) angle while the internal forward gap σ_{k+1}(M_{n+1})/σ_k(M_{n+1}) of M_{n+1} stays O(1). Davis–Kahan gives sin∠(S_n, S_{n+1}) ≤ ‖(B*B − I)|_{S_n}‖ / gap, whose numerator is the condition number of B (the inverse), not the forward ratio. So the inverse is genuinely load-bearing per step — it is intrinsic to which directions are top-k after applying B — and the forward ratio does not bound the aperture. This is the same wall the Wave-4 wedge route (SingularSlowSpaceConverge.lean, wedge_mu0_lb_is_inverse_bound) and the per-step s-engine (SingularBandConverge.lean) hit.

The guaranteed landing: unconditional on the tempered class

What is unconditional and sorry-free here:

• Oseledets.tendsto_vSlowSingularStep_of_summable_increment — the soft-analysis core: from a per-step increment upper bound b n ≥ ‖P_slow(n+1) − P_slow(n)‖ (equivalently the fast band increment, by the complement bridge) with (1/n)·log b n → L < 0, the slow projectors converge to the explicit complement 1 − Pfast of the fast band limit. No invertibility, no det, no tempering — pure root test + the landed structural reduction. This is genuinely unconditional; the only content is supplying such a b.

• Oseledets.tendsto_vSlowSingularStep_of_tempered — the tempered-class Vⱼ: supplying b from the det-free s-engine (norm_bandProjector_succ_sub_le_detfree) under (i) a strict spectral gap at the cut lamK < lamK1 from the a.e.-constant singular spectrum (the forward ratio r = σ_k/σ_{k-1} then has (1/n)log r → lamK − lamK1 < 0, geometric decay), and (ii) tempering of the compound condition number (1/n)·log(cB·cBi) → 0. Then (1/n)·log b → lamK − lamK1 < 0, so b is summable and Vⱼ converges to 1 − Pfast. The carry is the tempered-non-degeneracy hypothesis — strictly weaker than det A ≠ 0 everywhere, but it still requires each step's compound inverse to exist (so the s = 1/cBi supply is well-defined): see bandProjector_increment_eq_aperture for why no inverse-free per-step replacement exists.

• Oseledets.measurableSubspace_vSlowSingularStep (re-exported context) and Oseledets.vSlowSingularStep_antitone give the measurability and the antitone flag of the limit Vⱼ for free, from the landed SingularSlowSpace.lean (they are deterministic / unconditional).

Main results

• Oseledets.tendsto_vSlowSingularStep_of_summable_increment — unconditional soft core: summable per-step increment bound ⇒ Vⱼ converges to 1 − Pfast.
• Oseledets.tendsto_log_detfree_step_bound — the negative log-limit of the det-free s-engine's per-step bound, from the strict gap + tempering.
• Oseledets.summable_detfree_step_bound — the det-free per-step bound is summable under strict gap
  • tempering (root test).
• Oseledets.tendsto_vSlowSingularStep_of_tempered — the tempered-class Vⱼ: convergence to 1 − Pfast carrying the strict-gap + tempering hypotheses.
• Oseledets.ForwardRatioPerStepBound / Oseledets.bandProjector_increment_eq_aperture — the precise residual record: the forward-ratio per-step bound (R5A) is the aperture, governed by the inverse (condition number of B), not the forward ratio.

References

• A. Quas, Multiplicative Ergodic Theorems and Applications (Theorem 2, §3.1).
• M. S. Raghunathan, A proof of Oseledec's multiplicative ergodic theorem, Israel J. Math. 32 (1979), 356–362.
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM J. Numer. Anal. 7 (1970), 1–46 (the sin-Θ aperture bound).

The unconditional soft-analysis core

Any per-step upper bound on the slow (equivalently, by the complement bridge, fast band) increment whose (1/n)·log tends to a negative limit makes the increments summable (root test, summable_of_logLimit_neg), hence the slow projectors converge to the explicit complement 1 − Pfast of the fast band limit. This is unconditional: no invertibility, no det, no tempering. The only content is supplying such a b; everything below names what supplies it.

theorem Oseledets.tendsto_vSlowSingularStep_of_summable_increment {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) (b : ℕ → ℝ) (hb : ∀ (n : ℕ), 0 ≤ b n) (hpos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < b n) {L : ℝ} (hL : L < 0) (hlog : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (b n)) Filter.atTop (nhds L)) (hstep : ∀ᶠ (n : ℕ) in Filter.atTop, ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ b n) : ∃ (Pfast : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (vSlowSingularStep A T c n x)) Filter.atTop (nhds (1 - Pfast))

Unconditional soft core: summable increment bound ⇒ Vⱼ converges. If a per-step nonnegative, eventually-positive sequence b dominates the fast band-projector increments eventually and has (1/n)·log b n → L < 0, then the slow projectors orthProjMatrix (vSlowSingularStep A T c n x) converge to the explicit complement 1 − Pfast of the fast band limit Pfast. Pure root test (summable_of_logLimit_neg packaged as summable_norm_of_logLimit_neg_of_le) ⇒ exists_tendsto_cfc_of_summable (band converges to some Pfast) ⇒ the landed structural reduction tendsto_orthProjMatrix_vSlowSingularStep_of_tendsto_bandProjector. No det ≠ 0, no tempering.

The det-free per-step bound's negative log-limit (strict gap + tempering)

The det-free s-engine (norm_bandProjector_succ_sub_le_detfree, cBi ↦ 1/s) produces the per-step bound √(2k)·κ²·r/(1 − κ²r²) with κ = cB·cBi = cB/s and r = σ_k/σ_{k-1} of cocycle n. Its (1/n)·log decomposes as

(1/n)log√(2k) + (1/n)log κ² + (1/n)log r − (1/n)log(1 − κ²r²).

Under a strict spectral gap lamK < lamK1 at the cut ((1/n)log r → lamK − lamK1, from the a.e.-constant genuine singular spectrum Oseledets.ae_singularSpectralValue_eq_const selecting the two cut indices) and tempering (1/n)log κ → 0 (subexponential compound condition number), the first, second, and fourth terms vanish, leaving the negative limit lamK − lamK1. The argument is exactly the scalar layer of Oseledets.tendsto_log_bCocycle_point, isolated here on the abstract sequences so it needs no det ≠ 0 (the inverse, if any, sits inside the abstract κ).

theorem Oseledets.tendsto_log_detfree_step_bound {k : ℕ} (hk1 : 1 ≤ k) (κ r : ℕ → ℝ) (hκpos : ∀ (n : ℕ), 0 < κ n) (hrpos : ∀ (n : ℕ), 0 < r n) {lamK lamK1 : ℝ} (hgap : lamK < lamK1) (hlogκ : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (κ n)) Filter.atTop (nhds 0)) (hlogr : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) Filter.atTop (nhds (lamK - lamK1))) : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (√(2 * ↑k) * (κ n ^ 2 * r n / (1 - κ n ^ 2 * r n ^ 2)))) Filter.atTop (nhds (lamK - lamK1))

The negative log-limit of the det-free per-step bound. For abstract positive sequences κ (condition number, tempered: (1/n)log κ → 0) and r (forward ratio, gapped: (1/n)log r → lamK − lamK1 < 0), the per-step bound b n = √(2k)·κ n²·r n / (1 − κ n²·r n²) satisfies (1/n)·log b n → lamK − lamK1 < 0. This is the scalar root-test layer, det-free: the inverse (if any) is hidden inside κ.

theorem Oseledets.summable_detfree_step_bound {k : ℕ} (hk1 : 1 ≤ k) (κ r : ℕ → ℝ) (hκpos : ∀ (n : ℕ), 0 < κ n) (hrpos : ∀ (n : ℕ), 0 < r n) (hregime : ∀ᶠ (n : ℕ) in Filter.atTop, κ n ^ 2 * r n ^ 2 < 1) {lamK lamK1 : ℝ} (hgap : lamK < lamK1) (hlogκ : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (κ n)) Filter.atTop (nhds 0)) (hlogr : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) Filter.atTop (nhds (lamK - lamK1))) : Summable fun (n : ℕ) => √(2 * ↑k) * (κ n ^ 2 * r n / (1 - κ n ^ 2 * r n ^ 2))

The det-free per-step bound is summable (strict gap + tempering). With κ tempered and r gapped (as in tendsto_log_detfree_step_bound), the eventual-positivity regime κ²r² < 1, and the positivity of b, the per-step bound b n = √(2k)·κ n²·r n/(1 − κ n²·r n²) is summable by the root test. Det-free: the inverse (if any) is inside κ.

The tempered-class Vⱼ (the guaranteed landing)

Combining the det-free per-step bound (norm_bandProjector_succ_sub_le_detfree, supplying the b n = √(2k)·(cB/s)²·r/(1 − (cB/s)²r²) shape with s = 1/cBi, so κ = cB·cBi) with the summability above and the unconditional soft core: under a strict spectral gap at the cut and tempering of the compound condition number, the slow space Vⱼ converges to the explicit complement 1 − Pfast. The carry is named precisely: it is the tempered-non-degeneracy class, not unconditional.

theorem Oseledets.tendsto_vSlowSingularStep_of_tempered {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {k : ℕ} (hk1 : 1 ≤ k) (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) (κ r : ℕ → ℝ) (hκpos : ∀ (n : ℕ), 0 < κ n) (hrpos : ∀ (n : ℕ), 0 < r n) (hregime : ∀ᶠ (n : ℕ) in Filter.atTop, κ n ^ 2 * r n ^ 2 < 1) {lamK lamK1 : ℝ} (hgap : lamK < lamK1) (hlogκ : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (κ n)) Filter.atTop (nhds 0)) (hlogr : Filter.Tendsto (fun (n : ℕ) => (↑n)⁻¹ * Real.log (r n)) Filter.atTop (nhds (lamK - lamK1))) (hstep : ∀ᶠ (n : ℕ) in Filter.atTop, ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ ≤ √(2 * ↑k) * (κ n ^ 2 * r n / (1 - κ n ^ 2 * r n ^ 2))) : ∃ (Pfast : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (vSlowSingularStep A T c n x)) Filter.atTop (nhds (1 - Pfast))

The tempered-class Vⱼ converges to the explicit complement. Given a per-step increment upper bound of the det-free s-engine shape b n = √(2k)·κ n²·r n/(1 − κ n²·r n²) (the output of Oseledets.norm_bandProjector_succ_sub_le_detfree with κ = cB/s = cB·cBi), the regime κ²r² < 1 eventually, the strict gap lamK < lamK1 (forward ratio (1/n)log r → lamK − lamK1, from the a.e.-constant singular spectrum), and tempering (1/n)log κ → 0, the slow projectors orthProjMatrix (vSlowSingularStep A T c n x) converge to the explicit complement 1 − Pfast of the fast band limit. The slow space Vⱼ(ω) is then the orthogonal complement of the fast Oseledets spectral projector.

Carry (precise). Unconditional on the tempered-non-degeneracy class: the bound b n is the det-free s-engine's, whose s = 1/cBi supply needs each step's compound inverse to exist; the tempering (1/n)log κ → 0 is strictly weaker than det A ≠ 0 everywhere but is not removable (no inverse-free per-step replacement exists — bandProjector_increment_eq_aperture).

The precise residual: the forward-ratio per-step bound fails

The Wave-5 forward-ratio crack (R5A) (bound the slow increment by σ_{k+1}/σ_k of the single cocycle M_{n+1}, no inverse) is false at the per-step granularity. We record the precise mathematical content as a statement-level Prop definition — not a proof of a false claim — that identifies the failing quantity: the band increment IS the aperture ‖U Uᵀ − V Vᵀ‖ between the top-k right-singular frames of M_n (= U) and M_{n+1} (= V), which by Davis–Kahan is governed by the perturbation B = A(Tⁿx) (its condition number — the inverse), not by the internal forward ratio of M_{n+1}.

def Oseledets.ForwardRatioPerStepBound {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (k : ℕ) (x : X) (C : ℝ) : Prop

The forward-ratio per-step bound (R5A) (the falsified target). The proposition that, for a universal constant C, every step's band increment is bounded by C times the forward singular ratio σ_{k+1}(M_{n+1})/σ_k(M_{n+1}) of the single cocycle M_{n+1} = cocycle (n+1) x. This is the inverse-free bound Angle 5A sought. It is false at the per-step granularity (a single ill-conditioned B rotates the top-k space by O(1) while the forward ratio stays O(1)); the band increment is the aperture, governed by the condition number of B (the inverse), not the forward ratio. We state it as a Prop to name the residual precisely; no proof is given because the claim is false.

Equations

• One or more equations did not get rendered due to their size.

theorem Oseledets.bandProjector_increment_eq_aperture {X : Type u_1} {d : ℕ} {c : ℝ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) {k : ℕ} (n : ℕ) (x : X) (U V : Matrix (Fin d) (Fin k) ℝ) (hPn : bandProjector A T ((Set.Ioi c).indicator 1) n x = U * U.transpose) (hPn1 : bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x = V * V.transpose) : ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖ = ‖V * V.transpose - U * U.transpose‖

The band increment is the aperture ((R5A)'s failing identity). The band-projector increment whose forward-ratio bound (R5A) was sought equals — unconditionally — the Frobenius distance ‖U Uᵀ − V Vᵀ‖ between the top-k right-singular frames U (of M_n) and V (of M_{n+1}), provided the band projectors are realised by those frames. This is the aperture sin∠(S_n, S_{n+1}); it is governed by Davis–Kahan via the perturbation B = A(Tⁿx) (whose condition number — the inverse — appears in the denominator's gap), not by the internal forward ratio of M_{n+1}. Recording this identity pins exactly why (R5A) cannot hold inverse-free: the quantity to bound is a between-steps rotation, and the forward ratio measures only the within-M_{n+1} gap. (This re-derives, in the band-increment language, the wall of Oseledets.wedge_mu0_lb_is_inverse_bound and Oseledets.numerator_div_gap_le_detfree.)