Reverse-side entry bound for Ruelle's Lemma 1.4

entry_reverse_bound_of_orthogonal: for an orthogonal matrix S (here S * Sᵀ = 1) whose entries obey the graded forward bound |S a b| ≤ c · exp(-(max (g b - g a) 0)), every entry obeys the reverse bound at the full pairwise rate:

|S i j| ≤ (d-1)! · c^(d-1) · exp(-(g i - g j)).

The argument is Ruelle's cofactor expansion: S⁻¹ = Sᵀ, entries of S⁻¹ are (det S)-scaled cofactors with |det S| = 1, and each surviving Leibniz term of the cofactor minor pays exactly the level imbalance g i - g j by telescoping.

theorem Oseledets.RuelleCofactor.abs_det_le_sum_abs_prod {d : ℕ} (M : Matrix (Fin d) (Fin d) ℝ) : |M.det| ≤ ∑ σ : Equiv.Perm (Fin d), ∏ k : Fin d, |M (σ k) k|

A bare-handed Leibniz bound on |det M|: it is at most the number of permutations σ with nonzero ∏ times the worst per-permutation product bound. Here we directly bound |det M| ≤ ∑_σ ∏_k |M (σ k) k|.

theorem Oseledets.RuelleCofactor.card_filter_apply_eq_le {d : ℕ} (i j : Fin d) : {σ : Equiv.Perm (Fin d) | σ j = i}.card ≤ (d - 1).factorial

The number of permutations σ of Fin d with σ j = i is at most (d-1)!. Injection into Perm {x // x ≠ j} via the swap that pulls i back to j.

theorem Oseledets.RuelleCofactor.sum_level_telescope {d : ℕ} (g : Fin d → ℝ) (σ : Equiv.Perm (Fin d)) (i j : Fin d) (hσ : σ j = i) : ∑ k ∈ Finset.univ.erase j, (g k - g (σ k)) = g i - g j

The telescoping level identity: for a permutation σ of Fin d with σ j = i, ∑_{k ≠ j} (g k - g (σ k)) = g i - g j.

theorem Oseledets.RuelleCofactor.prod_entry_bound {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ) (g : Fin d → ℝ) (c : ℝ) (hc : 0 ≤ c) (hfwd : ∀ (a b : Fin d), |S a b| ≤ c * Real.exp (-max (g b - g a) 0)) (σ : Equiv.Perm (Fin d)) (i j : Fin d) (hσ : σ j = i) : ∏ k ∈ Finset.univ.erase j, |S (σ k) k| ≤ c ^ (d - 1) * Real.exp (-(g i - g j))

Per-permutation product bound. For a permutation σ of Fin d with σ j = i, the product of the (d-1) entry-magnitudes off the j-column, bounded by the graded forward bound, is at most c^(d-1) · exp(-(g i - g j)).

theorem Oseledets.RuelleCofactor.entry_reverse_bound_of_orthogonal {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ) (hS : S * S.transpose = 1) (g : Fin d → ℝ) (c : ℝ) (hc : 1 ≤ c) (hfwd : ∀ (a b : Fin d), |S a b| ≤ c * Real.exp (-max (g b - g a) 0)) (i j : Fin d) : |S i j| ≤ ↑(d - 1).factorial * c ^ (d - 1) * Real.exp (-(g i - g j))

Reverse-side entry bound (Ruelle Lemma 1.4, reverse half).

Let S be an orthogonal matrix (S * Sᵀ = 1) whose entries obey the graded forward bound |S a b| ≤ c · exp(-(max (g b - g a) 0)) (entries where the level g increases are exponentially small). Then every entry obeys the reverse bound at the full pairwise rate:

|S i j| ≤ (d-1)! · c^(d-1) · exp(-(g i - g j)).

Proof: S⁻¹ = Sᵀ, so S i j is a (det S)-scaled cofactor with |det S| = 1; expanding the cofactor minor by the Leibniz formula, every surviving permutation term pays exactly the level imbalance g i - g j (telescoping), and there are at most (d-1)! of them.