ConstructionDichotomyScales.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual scale consequences for the geometric dichotomy

These bounds use the numerical GeometryScales inequalities and the literal construction mesh. No geometric conclusion is supplied as a hypothesis.

theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.geometry_dimension_ge_three line 22
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.geometry_cutoff_pos line 31
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.geometry_two_cutoff_le_length line 34
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.velocity_le_mesh line 38
Source documentation
The rational-return velocity is no larger than the second mesh width.
```
theorem velocity_le_mesh (s : Data k) (hk : 3 ≤ k) (g : GeometryScales k)
    {v : ℝ} (hv : |v| ≤ 4 * cutoff k * (mesh s hk).H / k) :
    |v| ≤ (mesh s hk).H := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.velocity_lt_cut line 54
Source documentation
The same velocity lies strictly inside the actual cut-off scale.
```
theorem velocity_lt_cut (s : Data k) (hk : 3 ≤ k) (g : GeometryScales k)
    {v : ℝ} (hv : |v| ≤ 4 * cutoff k * (mesh s hk).H / k) :
    |v| < cutScale k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.velocity_div_small line 61
Source documentation
The total drift over the progression is less than half a unit.
```
theorem velocity_div_small (s : Data k) (hk : 3 ≤ k) (g : GeometryScales k)
    {h : ℕ} (hh : 0 < h) {v : ℝ}
    (hv : |v| ≤ 4 * cutoff k * (mesh s hk).H / k) :
    (k : ℝ) * |v / (h : ℝ)| < 1 / 2 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.lattice_error_small line 79
Source documentation
The error in the lattice lifting argument remains below one integer.
```
theorem lattice_error_small (s : Data k) (hk : 3 ≤ k) (g : GeometryScales k)
    {h : ℕ} (hh : 0 < h) :
    2 * (mesh s hk).H + 4 * cutoff k * (mesh s hk).H / (h : ℝ) < 1 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.mesh
theorem OAI.QuantitativeVanDerWaerden.ConstructionModel.twice_period_uniformWidth_lt_one line 93
Source documentation
Distinct rational returns cannot hide inside one first-system cell.
```
theorem twice_period_uniformWidth_lt_one (s : Data k) (hk : 3 ≤ k)
    (g : GeometryScales k) {h : ℕ} (hmax : h ≤ 2 * cutoff k) :
    2 * (h : ℝ) * (1 / (uniformCount k : ℝ)) < 1 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.ConstructionModel.Data, OAI.QuantitativeVanDerWaerden.ConstructionModel.uniformCount