The intermediate slow space Vⱼ of the singular forward flag — det-free structural reduction

This module constructs the finite-step approximants of an intermediate slow space Vⱼ(ω) of the singular (non-invertible) Oseledets forward filtration (Quas, Multiplicative Ergodic Theorems and Applications, 2013, Theorem 2; Ruelle, Publ. IHES 50, 1979, Lemma 1.4), and reduces its convergence — det-free, unconditionally — to the convergence of the fast band projector Oseledets.bandProjector.

It promotes the reusable structural lemmas of the Wave-2 de-risk scratch (Oseledets.Lyapunov.Extensions.SingularSlowSpaceCauchyScratch) from the fixed raw-Gram threshold (which is not Cauchy — threshold-scale mismatch) to the qpow / Lyapunov-scale cut (the cut at which the existing fast engine actually converges), defining the slow space as the orthogonal complement of the fast band at a Lyapunov gap value c.

The construction

The n-step slow approximant at a Lyapunov gap value c is

vSlowSingularStep A T c n x := the range of 1 − bandProjector A T (𝟙_{(c,∞)}) n x,

the orthogonal complement of the fast band (the span of qpow eigenvectors with eigenvalue > c). Equivalently it is the span of the qpow eigenvectors with eigenvalue ≤ c, i.e. the singular directions with σᵢ(cocycle n x)^{1/n} ≤ exp c (the slow / Lyapunov-subthreshold side).

The structural finding (det-free, unconditional)

Because bandProjector is a self-adjoint idempotent (bandProjector_isSelfAdjoint, bandProjector_indicator_mul_self), its complement 1 − bandProjector is again a self-adjoint idempotent, and orthProjMatrix (vSlowSingularStep …) = 1 − bandProjector … (orthProjMatrix_vSlowSingularStep). The two 1s then cancel in the consecutive-step difference, so the slow projector increments equal — in operator norm — the fast band increments:

‖P_slow(n+1) − P_slow(n)‖ = ‖bandProjector(n+1) − bandProjector(n)‖ (norm_vSlowSingularStep_proj_succ_sub_eq_band).

Hence summability of the slow increments is definitionally the summability of the fast increments (summable_vSlowSingularStep_increment_iff_band), and feeding it through Wave-1's exists_tendsto_orthProjMatrix_of_summable produces the limit slow projector (exists_tendsto_orthProjMatrix_vSlowSingularStep_of_summable). No invertibility, no separate small-σ leakage bound: the det-free norm_proj_sub_le_wedge engine that bounds the fast band increments controls the slow projector increments verbatim.

This is the genuine advance over the scratch: the cut is now the moving Lyapunov cut, at which the fast band increments are the very increments the existing engine (norm_bandProjector_succ_sub_le ⇒ exists_tendsto_bandProjector) makes summable — so the slow space converges along exactly the same a.e. set.

The wall (precisely pinned; the honest stopping point of Track 3B)

The structural reduction above is unconditional. What it reduces to — the summable fast-band increments — is supplied by exists_tendsto_bandProjector (which takes the per-step bound as a hypothesis) only after the per-step bound is discharged, and the unconditional cocycle discharge exists_tendsto_bandProjector_cocycle (via norm_bandProjector_succ_sub_le_cocycle) requires invertibility hA : ∀ x, (A x).det ≠ 0.

The invertibility is load-bearing in exactly one estimate, the rank-1 lower bound on the perturbed top eigenvalue μ̃₀ ≥ cM²/cBi² (Oseledets.ExteriorNorm.norm_sq_compound_mul_ge / …rayleigh_deficit_le), whose only route uses the compound inverse cBi = ‖compound k (A(Tⁿx))⁻¹‖ through the factorisation compound k M = compound k B⁻¹ · compound k (B·M) (compoundMatrix_eq_inv_mul). That bound is what makes the spectral-gap denominator μ̃₀ − ν of the Davis–Kahan sin-Θ step positive and large enough for the increment to decay. The det-free RuelleCore engine (SVDData.oneStep_sandwich, chain_leakage_exp) only delivers a one-sided upper mass envelope (a limsup spectral bound on a fixed slow space, e.g. Oseledets.limsup_le_of_mem_vslow); it does not lower-bound the perturbed top eigenvalue, hence cannot, by itself, bound the projector increment / aperture distance that the Cauchy construction of Vⱼ consumes. See the cruxStatus of the report.

So this module lands the full unconditional structural reduction (definition, complement bridge, increment identity, summability transfer, conditional limit, measurability, antitone flag) and names the single remaining input — and its single invertibility-using estimate — precisely.

Main definitions

• Oseledets.vSlowSingularStep — the n-step slow approximant (range of 1 − bandProjector).

Main results (all sorry-free, all det-free / unconditional)

• Oseledets.orthProjMatrix_vSlowSingularStep — the complement bridge orthProjMatrix (vSlowSingularStep …) = 1 − bandProjector ….
• Oseledets.norm_vSlowSingularStep_proj_succ_sub_eq_band — slow increment = fast band increment in norm.
• Oseledets.summable_vSlowSingularStep_increment_iff_band — summability transfer (definitional).
• Oseledets.exists_tendsto_orthProjMatrix_vSlowSingularStep_of_summable — the limit slow projector from summable fast-band increments (the Vⱼ construction crux, given the fast summability).
• Oseledets.measurableSubspace_vSlowSingularStep — measurability of each n-step slow space.
• Oseledets.vSlowSingularStep_antitone — the n-step slow spaces are antitone in the cut c (a larger Lyapunov threshold admits more slow directions): the finite-step flag.

The complement-projector algebra at the qpow (Lyapunov) cut

The fast band bandProjector A T (𝟙_{(c,∞)}) n x = cfc (𝟙_{(c,∞)}) (qpow A T n x) is a self-adjoint idempotent (unconditionally — bandProjector_isSelfAdjoint, bandProjector_indicator_mul_self). We record that its complement 1 − bandProjector is one too; this is the qpow-scale analogue of the scratch's raw-Gram cfc_indicator_Iic_eq_one_sub_Ioi, but stated directly on the band projector so it composes with the existing convergence engine.

theorem Oseledets.isSelfAdjoint_one_sub_bandProjector {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : IsSelfAdjoint (1 - bandProjector A T ((Set.Ioi c).indicator 1) n x)

The complement 1 − bandProjector A T (𝟙_{(c,∞)}) n x of the fast band is self-adjoint: the difference of the self-adjoint identity and the self-adjoint band projector.

theorem Oseledets.one_sub_bandProjector_mul_self {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : (1 - bandProjector A T ((Set.Ioi c).indicator 1) n x) * (1 - bandProjector A T ((Set.Ioi c).indicator 1) n x) = 1 - bandProjector A T ((Set.Ioi c).indicator 1) n x

The complement 1 − bandProjector A T (𝟙_{(c,∞)}) n x of the fast band is idempotent: (1 − P)² = 1 − 2P + P² = 1 − P since P² = P (bandProjector_indicator_mul_self).

The n-step slow approximant and the complement bridge

noncomputable def Oseledets.vSlowSingularStep {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : Submodule ℝ (EuclideanSpace ℝ (Fin d))

The n-step slow approximant at the Lyapunov gap value c: the range of the complement 1 − bandProjector A T (𝟙_{(c,∞)}) n x of the fast band, transported to a subspace of EuclideanSpace ℝ (Fin d). It is the orthogonal complement of the span of the qpow eigenvectors with eigenvalue > c, i.e. the span of the singular directions with σᵢ^{1/n} ≤ exp c — the finite-step approximant of an intermediate slow space Vⱼ(ω) of the singular Oseledets flag (Quas, MET and Applications, 2013, Theorem 2).

Equations

• Oseledets.vSlowSingularStep A T c n x = (↑(Matrix.toEuclideanCLM (1 - Oseledets.bandProjector A T ((Set.Ioi c).indicator 1) n x))).range

theorem Oseledets.orthProjMatrix_vSlowSingularStep {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : orthProjMatrix (vSlowSingularStep A T c n x) = 1 - bandProjector A T ((Set.Ioi c).indicator 1) n x

The complement bridge. The orthogonal-projection matrix onto the n-step slow space equals 1 − bandProjector A T (𝟙_{(c,∞)}) n x, the complement of the fast band projector. Direct from the projector/range bridge orthProjMatrix_range_toEuclideanCLM and the complement-projector algebra (isSelfAdjoint_one_sub_bandProjector, one_sub_bandProjector_mul_self).

Slow increment = fast (band) increment in norm

The complement bridge turns the consecutive slow projector increment into the consecutive fast band increment: the 1s cancel and the difference flips sign, which is norm-invariant. This is the det-free structural heart — the slow-side increment estimate IS the fast-side increment estimate, verbatim, with no invertibility and no new small-σ leakage bound.

theorem Oseledets.norm_vSlowSingularStep_proj_succ_sub_eq_band {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : ‖orthProjMatrix (vSlowSingularStep A T c (n + 1) x) - orthProjMatrix (vSlowSingularStep A T c n x)‖ = ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖

Slow increment equals fast (band) increment in norm. The consecutive slow-projector increment has the same operator norm as the consecutive fast band-projector increment at the same Lyapunov cut c:

‖P_slow(n+1) − P_slow(n)‖ = ‖bandProjector(n+1) − bandProjector(n)‖.

Proof: the complement bridge writes each slow projector as 1 − bandProjector; the 1s cancel in the difference, the sign flips, and ‖−M‖ = ‖M‖.

Summability transfer and the limit slow projector

The norm identity makes summability of the slow increments literally the same proposition as summability of the fast band increments. Feeding it through Wave-1's exists_tendsto_orthProjMatrix_of_summable produces the limit slow projector — the analytic crux of the Vⱼ construction, given the summable fast-band increments (which the existing engine supplies under the named invertibility hypothesis; see the module docstring's wall).

theorem Oseledets.summable_vSlowSingularStep_increment_iff_band {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) : (Summable fun (n : ℕ) => ‖orthProjMatrix (vSlowSingularStep A T c (n + 1) x) - orthProjMatrix (vSlowSingularStep A T c n x)‖) ↔ Summable fun (n : ℕ) => ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖

Summability transfer. The slow-projector increments are summable iff the fast band-projector increments are. Immediate from the per-step norm identity norm_vSlowSingularStep_proj_succ_sub_eq_band.

theorem Oseledets.exists_tendsto_orthProjMatrix_vSlowSingularStep_of_summable {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) (hsum : Summable fun (n : ℕ) => ‖bandProjector A T ((Set.Ioi c).indicator 1) (n + 1) x - bandProjector A T ((Set.Ioi c).indicator 1) n x‖) : ∃ (P : Matrix (Fin d) (Fin d) ℝ), Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (vSlowSingularStep A T c n x)) Filter.atTop (nhds P) ∧ IsSelfAdjoint P ∧ P * P = P

The limit slow projector (the Vⱼ construction crux). If the fast band-projector increments are summable, then the slow orthogonal projectors orthProjMatrix (vSlowSingularStep A T c n x) converge to a matrix P that is again an orthogonal projector (self-adjoint and idempotent, P * P = P) — the candidate limit slow projector encoding Vⱼ(ω) = limₙ vSlowSingularStep A T c n x.

This is the assembly of the det-free reduction: the summability transfer (summable_vSlowSingularStep_increment_iff_band) feeds Wave-1's exists_tendsto_orthProjMatrix_of_summable. The only remaining input is the fast-band increment summability — supplied by the existing det-free leakage engine (norm_bandProjector_succ_sub_le ⇒ exists_tendsto_bandProjector), whose UNCONDITIONAL cocycle discharge requires invertibility in exactly one rank-1 lower bound; see the module docstring.

Convergence of the slow projector to a concrete limit (the band-limit complement)

Beyond mere existence of a limit projector, the slow projector converges to the explicit complement 1 − P_fast of the fast band limit P_fast. This is the cleanest packaging of the reduction: the slow space limit is literally the orthogonal complement of the fast Oseledets spectral projector, with no extra analysis once bandProjector converges.

theorem Oseledets.tendsto_orthProjMatrix_vSlowSingularStep_of_tendsto_bandProjector {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (x : X) {Pfast : Matrix (Fin d) (Fin d) ℝ} (hP : Filter.Tendsto (fun (n : ℕ) => bandProjector A T ((Set.Ioi c).indicator 1) n x) Filter.atTop (nhds Pfast)) : Filter.Tendsto (fun (n : ℕ) => orthProjMatrix (vSlowSingularStep A T c n x)) Filter.atTop (nhds (1 - Pfast))

Slow projector → complement of the fast limit. If the fast band projectors converge to P_fast, then the slow projectors orthProjMatrix (vSlowSingularStep A T c n x) converge to the complement 1 − P_fast. Continuity of M ↦ 1 − M applied to the complement bridge orthProjMatrix_vSlowSingularStep.

Measurability of the n-step slow space

Each n-step slow space is a MeasurableSubspace (in x), unconditionally. The complement of the fast band is the slow spectral projector cfc (𝟙_{(-∞,c]}) (qpow), which is measurable by measurable_spectralProjector applied to the measurable, self-adjoint qpow family.

theorem Oseledets.one_sub_bandProjector_eq_cfc_Iic {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : 1 - bandProjector A T ((Set.Ioi c).indicator 1) n x = cfc ((Set.Iic c).indicator 1) (qpow A T n x)

The complement 1 − bandProjector A T (𝟙_{(c,∞)}) n x equals the slow spectral projector cfc (𝟙_{(-∞,c]} 1) (qpow A T n x) — the qpow-scale orthogonal-complement cfc identity (the qpow analogue of the scratch's raw-Gram cfc_indicator_Iic_eq_one_sub_Ioi). The {0,1} indicators of (-∞,c] and (c,∞) sum to 1 and cfc is additive, so the slow projector is 1 minus the fast projector at the same qpow cut.

theorem Oseledets.vSlowSingularStep_eq_range_cfc {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) (c : ℝ) (n : ℕ) (x : X) : vSlowSingularStep A T c n x = (↑(Matrix.toEuclideanCLM (cfc ((Set.Iic c).indicator 1) (qpow A T n x)))).range

The slow space is the range of the slow qpow spectral projector. vSlowSingularStep A T c n x equals the range of cfc (𝟙_{(-∞,c]} 1) (qpow A T n x), the orthogonal projector onto the span of the qpow eigenvectors with eigenvalue ≤ c. Rewriting the defining complement via the orthogonal-complement cfc identity one_sub_bandProjector_eq_cfc_Iic.

theorem Oseledets.measurableSubspace_vSlowSingularStep {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] {A : X → Matrix (Fin d) (Fin d) ℝ} (hA : Measurable A) {T : X → X} (hT : Measurable T) (c : ℝ) (n : ℕ) : MeasurableSubspace fun (x : X) => vSlowSingularStep A T c n x

Measurability of the n-step slow space. For each fixed step n and Lyapunov cut c, the family x ↦ vSlowSingularStep A T c n x is a MeasurableSubspace. The defining matrix is the slow qpow spectral projector cfc (𝟙_{(-∞,c]} 1) (qpow A T n x) (vSlowSingularStep_eq_range_cfc), a measurable (measurable_spectralProjector on the measurable, self-adjoint qpow family measurable_qpow / qpow_isSelfAdjoint) self-adjoint idempotent; the projector/range bridge measurableSubspace_range_of_measurable closes it. Unconditional.

The antitone finite-step flag

The n-step slow spaces are antitone in the Lyapunov cut c: a larger threshold admits more slow (subthreshold) singular directions, so c ≤ c' gives vSlowSingularStep … c … ≤ vSlowSingularStep … c' …. This is the finite-step incarnation of the nested slow flag V₁ ⊆ V₂ ⊆ ⋯ of Oseledets' filtration. The range of a spectral ≤ c projector is the ≤ c eigenspace, and ≤ c eigenspaces nest as c grows.

theorem Oseledets.cfc_Iic_mul_Iic_of_le {X : Type u_1} {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) {c c' : ℝ} (hcc : c ≤ c') (n : ℕ) (x : X) : cfc ((Set.Iic c').indicator 1) (qpow A T n x) * cfc ((Set.Iic c).indicator 1) (qpow A T n x) = cfc ((Set.Iic c).indicator 1) (qpow A T n x)

The slow qpow spectral projector fixes every slow eigenvector at a smaller cut: if c ≤ c', then cfc (𝟙_{(-∞,c']}) (qpow) ∘ cfc (𝟙_{(-∞,c]}) (qpow) = cfc (𝟙_{(-∞,c]}) (qpow), because on the spectrum the larger indicator dominates the smaller (𝟙_{(-∞,c']}·𝟙_{(-∞,c]} = 𝟙_{(-∞,c]}). This is the projector-nesting that yields the subspace inclusion.

theorem Oseledets.vSlowSingularStep_antitone {X : Type u_1} [MeasurableSpace X] {d : ℕ} [NeZero d] (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X → X) {c c' : ℝ} (hcc : c ≤ c') (n : ℕ) (x : X) : vSlowSingularStep A T c n x ≤ vSlowSingularStep A T c' n x

The antitone finite-step slow flag. For c ≤ c', the n-step slow space at cut c is contained in the one at cut c': vSlowSingularStep A T c n x ≤ vSlowSingularStep A T c' n x. The smaller-cut slow projector factors through the larger-cut one (cfc_Iic_mul_Iic_of_le), so each vector of the smaller range lies in the larger range. This is the nested slow flag of the singular forward filtration at finite step n.