WordEstimate.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Binning the weights: entropy.tex, equation (entropy-bins).

abbrev OAI.TorsionFreeZeroDivisors.WordEstimate.Letter line 12
def OAI.TorsionFreeZeroDivisors.WordEstimate.inverse line 14
def OAI.TorsionFreeZeroDivisors.WordEstimate.IsExtra line 16
instance OAI.TorsionFreeZeroDivisors.WordEstimate.(instance at line 18) line 18
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.isExtra_inl line 20
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.not_isExtra_inr line 23
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.inverse_inverse line 26
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.inverse_ne line 29
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.extra_inverse_not_extra line 33
def OAI.TorsionFreeZeroDivisors.WordEstimate.p line 38
Source documentation
The exact marginal letter frequency p=129/16513.
```
def p : ℝ := 129 / 16513
```
def OAI.TorsionFreeZeroDivisors.WordEstimate.baseWeight line 41
Source documentation
Conditional turn weights on side B before setting cancelling turns to zero.
```
def baseWeight (t u : Letter) : ℝ :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter
def OAI.TorsionFreeZeroDivisors.WordEstimate.weight line 46
Source documentation
Source w(t,u), including zero on cancelling turns.
```
def weight (t u : Letter) : ℝ := if u = inverse t then 0 else baseWeight t u
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.inverse, OAI.TorsionFreeZeroDivisors.WordEstimate.baseWeight
def OAI.TorsionFreeZeroDivisors.WordEstimate.f line 49
Source documentation
The positive test vector in the manuscript's matrix argument.
```
def f (t : Letter) : ℝ := if IsExtra (inverse t) then 5 else 1
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.IsExtra, OAI.TorsionFreeZeroDivisors.WordEstimate.inverse
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.one_le_f line 51
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.f_extra line 55
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.sum_f line 58
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.base_row_mass line 64
Source documentation
The two row types have the exact untruncated mass given by the source.
```
theorem base_row_mass (t : Letter) :
    (∑ u : Letter, baseWeight t u ^ 2 * f u) =
      if IsExtra (inverse t) then 3 + 16525 * p ^ 2
      else 3 * p ^ 2 + 16525 / 129 ^ 2 := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.baseWeight, OAI.TorsionFreeZeroDivisors.WordEstimate.f, OAI.TorsionFreeZeroDivisors.WordEstimate.IsExtra, OAI.TorsionFreeZeroDivisors.WordEstimate.inverse, OAI.TorsionFreeZeroDivisors.WordEstimate.p
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.row_mass line 78
Source documentation
Removing the cancelling turn removes precisely its diagonal summand.
```
theorem row_mass (t : Letter) :
    (∑ u : Letter, weight t u ^ 2 * f u) =
      (∑ u : Letter, baseWeight t u ^ 2 * f u) -
        baseWeight t (inverse t) ^ 2 * f (inverse t) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.weight, OAI.TorsionFreeZeroDivisors.WordEstimate.f, OAI.TorsionFreeZeroDivisors.WordEstimate.baseWeight, OAI.TorsionFreeZeroDivisors.WordEstimate.inverse
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.matrix_contraction line 91
Source documentation
Mf ≤ (149/150)f, with the exact alphabet, weights and constants.
```
theorem matrix_contraction (t : Letter) :
    (∑ u : Letter, weight t u ^ 2 * f u) ≤ (149 / 150 : ℝ) * f t := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.weight, OAI.TorsionFreeZeroDivisors.WordEstimate.f
def OAI.TorsionFreeZeroDivisors.WordEstimate.continuation line 106
Source documentation
Product of the turn weights from a starting letter through a tail.
```
def continuation : (n : ℕ) → Letter → (Fin n → Letter) → ℝ
  | 0, _, _ => 1
  | n + 1, t, W => weight t (W 0) * continuation n (W 0) (Fin.tail W)

/-- Source `P(W)`, with empty products equal to one. -/
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.weight
def OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight line 111
Source documentation
Source P(W), with empty products equal to one.
```
def wordWeight : (h : ℕ) → (Fin h → Letter) → ℝ
  | 0, _ => 1
  | h + 1, W => continuation h (W 0) (Fin.tail W)
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.continuation
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.sum_cons line 115
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.continuation_mass line 122
Source documentation
Iterating the exact matrix contraction controls all tails simultaneously.
```
theorem continuation_mass (n : ℕ) (t : Letter) :
    (∑ W : Fin n → Letter, continuation n t W ^ 2) ≤
      (149 / 150 : ℝ) ^ n * f t := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.continuation, OAI.TorsionFreeZeroDivisors.WordEstimate.f
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.squared_word_geometric_bound line 148
Source documentation
The matrix form of the squared-word estimate, before exponent conversion.
```
theorem squared_word_geometric_bound (h : ℕ) :
    (∑ W : Fin (h + 1) → Letter, wordWeight (h + 1) W ^ 2) ≤
      16528 * (149 / 150 : ℝ) ^ h := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.continuation_eq_product line 161
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight_eq_product line 173
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.constant_le_exp line 178
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.ratio_le_exp line 186
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.geometric_exponential_bound line 191
Source documentation
The manuscript's exact numerical cutoff, without asymptotic weakening.
```
theorem geometric_exponential_bound (n : ℕ) (hn : 3001 ≤ n) :
    16528 * (149 / 150 : ℝ) ^ n ≤ Real.exp (-((n : ℝ) + 1) / 300) := by
…
```
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.squared_word_estimate line 208
Source documentation
Source lemma lem:squared-words, with its exhibited delta=1/600.
```
theorem squared_word_estimate (h : ℕ) (hh : 3002 ≤ h) :
    (∑ W : Fin h → Letter, wordWeight h W ^ 2) ≤
      Real.exp (-2 * (1 / 600 : ℝ) * h) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.weight_nonneg line 222
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.weight_le_one line 226
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.weight_pos_lower line 230
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.continuation_nonneg line 235
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight_nonneg line 240
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight_upper line 245
def OAI.TorsionFreeZeroDivisors.WordEstimate.binWords line 260
Source documentation
Exact logarithmic bins, excluding zero weights just as in the source.
```
def binWords (h : ℕ) (d : ℤ) : Finset (Fin h → Letter) :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.bin_sq_lower line 263
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.bin_card_bound line 277
Source documentation
The exact finite bin-count bound before replacing h by its common scale.
```
theorem bin_card_bound (h : ℕ) (hh : 3002 ≤ h) (d : ℤ) :
    ((binWords h d).card : ℝ) ≤
      Real.exp (2 * (d : ℝ) + 2 - 2 * (1 / 600 : ℝ) * h) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.binWords
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.bin_scale_bounds line 297
Source documentation
Both the lower bin cutoff and the counting bound at the scalar block scale s. The displayed threshold absorbs the manuscript's rounding errors.
```
theorem bin_scale_bounds (h : ℕ) (hh : 3002 ≤ h) (s : ℝ)
    (hscale : s + 1200 ≤ 2 * h) (d : ℤ) (W : Fin h → Letter)
    (hW : W ∈ binWords h d) :
    (1 / 600 : ℝ) * s / 2 ≤ (d : ℝ) ∧
      ((binWords h d).card : ℝ) ≤ Real.exp (2 * d - (1 / 600 : ℝ) * s) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.binWords
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.continuation_lower line 323
Source documentation
Every positive continuation has the uniform lower product bound from its smallest allowed turn weight.
```
theorem continuation_lower (n : ℕ) (t : Letter) (W : Fin n → Letter)
    (hp : 0 < continuation n t W) :
    (1/129 : ℝ)^n ≤ continuation n t W := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.continuation
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.wordWeight_lower line 339
theorem OAI.TorsionFreeZeroDivisors.WordEstimate.bin_upper_bound line 352
Source documentation
A coarse fixed upper bin constant; the manuscript leaves a₀ unspecified. We choose a₀=256, avoiding any numerical transcendental oracle.
```
theorem bin_upper_bound (h : ℕ) (s : ℝ) (hscale : (h : ℝ) ≤ 2*s)
    (d : ℤ) (W : Fin h → Letter) (hW : W ∈ binWords h d) : (d : ℝ) ≤ 256*s := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.binWords

theorem OAI.TorsionFreeZeroDivisors.WordEstimate.bin_full_bounds line 369

Source documentation

Both bin cutoffs and the squared-word count with literal δ=1/600 and one universal upper constant.

theorem bin_full_bounds (h : ℕ) (hh : 3002 ≤ h) (s : ℝ)
    (hscale : s+1200 ≤ 2*h) (hscale' : (h : ℝ) ≤ 2*s)
    (d : ℤ) (W : Fin h → Letter) (hW : W ∈ binWords h d) :
    (1/600 : ℝ)*s/2 ≤ d ∧ (d : ℝ) ≤ 256*s ∧
      ((binWords h d).card : ℝ) ≤ Real.exp (2*d-(1/600 : ℝ)*s) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.WordEstimate.Letter, OAI.TorsionFreeZeroDivisors.WordEstimate.binWords