RawDensityParameters.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.Problem337.RawDensityParameters.DM line 11
Source documentation
The fixed denominator constant from the residue construction.
```
abbrev DM : ℝ := 204204
```
abbrev OAI.Problem337.RawDensityParameters.D₀ line 13
Source documentation
The terminal binary cutoff exponent.
```
abbrev D₀ : ℝ := 100000
```
abbrev OAI.Problem337.RawDensityParameters.η line 15
Source documentation
The fixed geometric contraction rate.
```
abbrev η : ℝ := 1 / 10000
```
abbrev OAI.Problem337.RawDensityParameters.c line 17
Source documentation
The exponent in the exceptional-set estimate.
```
abbrev c : ℝ := 1 / 1000
```
abbrev OAI.Problem337.RawDensityParameters.K line 19
Source documentation
The logarithmic bound for the number of geometric levels.
```
abbrev K : ℝ := 3 * (DM + 2) / η
```
Mentions: OAI.Problem337.RawDensityParameters.DM, OAI.Problem337.RawDensityParameters.η
abbrev OAI.Problem337.RawDensityParameters.r line 21
Source documentation
A fixed moment exponent sufficient for the density recurrence.
```
abbrev r : ℝ := 8 * K
```
Mentions: OAI.Problem337.RawDensityParameters.K
abbrev OAI.Problem337.RawDensityParameters.L line 23
Source documentation
The terminal expansion budget plus the backward descent budget.
```
abbrev L : ℝ := TerminalAssembly.terminalCoefficient D₀ (1 - η) + K + 1
```
Mentions: OAI.Problem337.TerminalAssembly.terminalCoefficient, OAI.Problem337.RawDensityParameters.D₀, OAI.Problem337.RawDensityParameters.η, OAI.Problem337.RawDensityParameters.K
theorem OAI.Problem337.RawDensityParameters.DM_gt_one line 25
theorem OAI.Problem337.RawDensityParameters.D₀_ge_one line 26
theorem OAI.Problem337.RawDensityParameters.eta_pos line 27
theorem OAI.Problem337.RawDensityParameters.eta_le_half line 28
theorem OAI.Problem337.RawDensityParameters.c_pos line 29
theorem OAI.Problem337.RawDensityParameters.K_nonneg line 30
theorem OAI.Problem337.RawDensityParameters.r_ge_two line 31
theorem OAI.Problem337.RawDensityParameters.eight_K_le_r line 32
theorem OAI.Problem337.RawDensityParameters.L_pos line 33
theorem OAI.Problem337.RawDensityParameters.eventually_constructor_conditions line 41
Source documentation
All scalar conditions required by the fixed-loss geometric constructor hold at one common onset, independently of the natural values C and M.
```
theorem eventually_constructor_conditions : ∀ᶠ S : ℝ in atTop,
    1 ≤ S ∧ 1 ≤ Real.log S ∧ 2 ≤ ResidueLevels.scale S ∧
    S / (2 * Real.log S) ≤ (ResidueLevels.scale S : ℝ) ∧
    1 + 2 * Real.exp (S ^ (1 / 4 : ℝ) / r) ≤
      Real.exp (2 * S ^ (1 / 4 : ℝ)) := by
…
```
Mentions: OAI.Problem337.ResidueLevels.scale, OAI.Problem337.RawDensityParameters.r
theorem OAI.Problem337.RawDensityParameters.eventually_raw_density_supply_of_residue_data line 56
Source documentation
Canonical numerical specialization of the geometric constructor. This lemma supplies only scalar conditions: genuine residue data, the denominator window, and binary divisibility are still required explicitly.
```
theorem eventually_raw_density_supply_of_residue_data :
    ∀ᶠ S : ℝ in atTop, ∀ C M : ℕ,
      Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
      Real.exp S < (M : ℝ) →
      (M : ℝ) ≤ Real.exp (DM * S) →
      2 ^ TerminalDepth.binaryExponent D₀ S ∣ M →
      GeometricDensity.ResidueData DM D₀ η c r S 2 C M →
      RawDensitySupply DM L c K r S C := by
…
```
Mentions: OAI.Problem337.RawDensityParameters.DM, OAI.Problem337.TerminalDepth.binaryExponent, OAI.Problem337.RawDensityParameters.D₀, OAI.Problem337.GeometricDensity.ResidueData, OAI.Problem337.RawDensityParameters.η, OAI.Problem337.RawDensityParameters.c, OAI.Problem337.RawDensityParameters.r, OAI.Problem337.RawDensitySupply, OAI.Problem337.RawDensityParameters.L, OAI.Problem337.RawDensityParameters.K