1. OAI
  2. NumberTheory
  3. DirichletL
  4. CubicSieve
  5. DescentScale
-- Modified in quasi-rh-eleven-twelfths to parameterize the canonical descent scale. import Mathlib.Analysis.SpecialFunctions.Pow.Realnamespace OAInoncomputable section

Numerical data for the finite canonical descent.

denominator is the reciprocal step size, while reserve is the initial power saving. The last field is exactly the compatibility needed by the short-cube argument: twenty-five factors of size Z^(1 / denominator) spend at most half of the reserve. There is deliberately no global instance; public theorems install the scale they need locally.

class CanonicalDescentScale where denominator : ℕ denominator_pos : 0 < denominator reserve : ℝ reserve_pos : 0 < reserve short_budget : 50 ≤ reserve * denominatornamespace CanonicalDescentScaledef step (scale : CanonicalDescentScale) : ℝ := 1 / (scale.denominator : ℝ)def rankCap (scale : CanonicalDescentScale) : ℕ := 3 * scale.denominatordef shortMargin (scale : CanonicalDescentScale) : ℝ := scale.reserve / 2def fixedFactorExponent (scale : CanonicalDescentScale) : ℝ := scale.reserve / 4def strictReserve (scale : CanonicalDescentScale) : ℝ := 3 * scale.reserve / 4theorem denominator_real_pos (scale : CanonicalDescentScale) : (0 : ℝ) < scale.denominator := scale:CanonicalDescentScale⊢ 0 < ↑denominator All goals completed! 🐙theorem denominator_real_ge_one (scale : CanonicalDescentScale) : (1 : ℝ) ≤ scale.denominator := scale:CanonicalDescentScale⊢ 1 ≤ ↑denominator All goals completed! 🐙theorem step_pos (scale : CanonicalDescentScale) : 0 < scale.step := scale:CanonicalDescentScale⊢ 0 < scale.step All goals completed! 🐙theorem step_le_one (scale : CanonicalDescentScale) : scale.step ≤ 1 := scale:CanonicalDescentScale⊢ scale.step ≤ 1 scale:CanonicalDescentScale⊢ 1 ≤ ↑denominator All goals completed! 🐙theorem reserve_nonneg (scale : CanonicalDescentScale) : 0 ≤ scale.reserve := scale.reserve_pos.letheorem shortMargin_pos (scale : CanonicalDescentScale) : 0 < scale.shortMargin := scale:CanonicalDescentScale⊢ 0 < scale.shortMargin exact div_pos scale.reserve_pos (scale:CanonicalDescentScale⊢ 0 < 2 All goals completed! 🐙)theorem fixedFactorExponent_pos (scale : CanonicalDescentScale) : 0 < scale.fixedFactorExponent := scale:CanonicalDescentScale⊢ 0 < scale.fixedFactorExponent exact div_pos scale.reserve_pos (scale:CanonicalDescentScale⊢ 0 < 4 All goals completed! 🐙)theorem fixedFactorExponent_le_shortMargin (scale : CanonicalDescentScale) : scale.fixedFactorExponent ≤ scale.shortMargin := scale:CanonicalDescentScale⊢ scale.fixedFactorExponent ≤ scale.shortMargin scale:CanonicalDescentScale⊢ reserve / 4 ≤ reserve / 2 All goals completed! 🐙theorem rankCap_pos (scale : CanonicalDescentScale) : 0 < scale.rankCap := scale:CanonicalDescentScale⊢ 0 < scale.rankCap scale:CanonicalDescentScale⊢ 0 < 3 * denominator exact Nat.mul_pos (scale:CanonicalDescentScale⊢ 0 < 3 All goals completed! 🐙) scale.denominator_postheorem strictReserve_pos (scale : CanonicalDescentScale) : 0 < scale.strictReserve := scale:CanonicalDescentScale⊢ 0 < scale.strictReserve scale:CanonicalDescentScale⊢ 0 < 3 * reserve / 4 exact div_pos (mul_pos (scale:CanonicalDescentScale⊢ 0 < 3 All goals completed! 🐙) scale.reserve_pos) (scale:CanonicalDescentScale⊢ 0 < 4 All goals completed! 🐙)

The numerical hypothesis used by the short-cube algebra.

theorem short_spend (scale : CanonicalDescentScale) : 25 * scale.step ≤ scale.shortMargin := scale:CanonicalDescentScale⊢ 25 * scale.step ≤ scale.shortMargin scale:CanonicalDescentScalehq:0 < ↑denominator⊢ 25 * scale.step ≤ scale.shortMargin scale:CanonicalDescentScalehq:0 < ↑denominatorhb:50 ≤ reserve * ↑denominator⊢ 25 * scale.step ≤ scale.shortMargin scale:CanonicalDescentScalehq:0 < ↑denominatorhb:50 ≤ reserve * ↑denominator⊢ 25 * (1 / ↑denominator) ≤ reserve / 2 calc 25 * (1 / (scale.denominator : ℝ)) = 25 / scale.denominator := scale:CanonicalDescentScalehq:0 < ↑denominatorhb:50 ≤ reserve * ↑denominator⊢ 25 * (1 / ↑denominator) = 25 / ↑denominator All goals completed! 🐙 _ ≤ scale.reserve / 2 := (div_le_iff₀ hq).2 (scale:CanonicalDescentScalehq:0 < ↑denominatorhb:50 ≤ reserve * ↑denominator⊢ 25 ≤ reserve / 2 * ↑denominator All goals completed! 🐙)theorem reserve_decomposition (scale : CanonicalDescentScale) : scale.strictReserve - scale.fixedFactorExponent = scale.shortMargin := scale:CanonicalDescentScale⊢ scale.strictReserve - scale.fixedFactorExponent = scale.shortMargin scale:CanonicalDescentScale⊢ 3 * reserve / 4 - reserve / 4 = reserve / 2 All goals completed! 🐙

A scale with prescribed positive reserve. The extra + 1 makes the denominator positive without a case split.

Definition `OAI.CanonicalDescentScale.ofReserve` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`. def ofReserve (κ : ℝ) (hκ : 0 < κ) : CanonicalDescentScale where denominator := ⌈50 / κ⌉₊ + 1 denominator_pos := κ:ℝhκ:0 < κ⊢ 0 < ⌈50 / κ⌉₊ + 1 All goals completed! 🐙 reserve := κ reserve_pos := hκ short_budget := κ:ℝhκ:0 < κ⊢ 50 ≤ κ * ↑(⌈50 / κ⌉₊ + 1) κ:ℝhκ:0 < κhceil:50 / κ ≤ ↑⌈50 / κ⌉₊⊢ 50 ≤ κ * ↑(⌈50 / κ⌉₊ + 1) κ:ℝhκ:0 < κhceil:50 / κ ≤ ↑⌈50 / κ⌉₊hadd:↑⌈50 / κ⌉₊ ≤ ↑(⌈50 / κ⌉₊ + 1)⊢ 50 ≤ κ * ↑(⌈50 / κ⌉₊ + 1) κ:ℝhκ:0 < κhceil:50 / κ ≤ ↑⌈50 / κ⌉₊hadd:↑⌈50 / κ⌉₊ ≤ ↑(⌈50 / κ⌉₊ + 1)hdiv:50 / κ ≤ ↑(⌈50 / κ⌉₊ + 1)⊢ 50 ≤ κ * ↑(⌈50 / κ⌉₊ + 1) κ:ℝhκ:0 < κhceil:50 / κ ≤ ↑⌈50 / κ⌉₊hadd:↑⌈50 / κ⌉₊ ≤ ↑(⌈50 / κ⌉₊ + 1)hdiv:50 / κ ≤ ↑(⌈50 / κ⌉₊ + 1)this:50 ≤ ↑(⌈50 / κ⌉₊ + 1) * κ⊢ 50 ≤ κ * ↑(⌈50 / κ⌉₊ + 1) κ:ℝhκ:0 < κhceil:50 / κ ≤ ↑⌈50 / κ⌉₊hadd:↑⌈50 / κ⌉₊ ≤ ↑(⌈50 / κ⌉₊ + 1)hdiv:50 / κ ≤ ↑(⌈50 / κ⌉₊ + 1)this:50 ≤ (↑⌈50 / κ⌉₊ + 1) * κ⊢ 50 ≤ κ * (↑⌈50 / κ⌉₊ + 1) All goals completed! 🐙

Historical parameters, exposed as a value rather than a global instance.

Definition `OAI.CanonicalDescentScale.historical` of class type is semireducible. Most type class instances should be instance-reducible, so consider marking this definition with `@[instance_reducible]`. If it is intentionally semireducible, this warning can be disabled with `set_option warn.classDefReducibility false`. def historical : CanonicalDescentScale where denominator := 1000 denominator_pos := ⊢ 0 < 1000 All goals completed! 🐙 reserve := (1 : ℝ) / 20 reserve_pos := ⊢ 0 < 1 / 20 All goals completed! 🐙 short_budget := ⊢ 50 ≤ 1 / 20 * ↑1000 All goals completed! 🐙end CanonicalDescentScaleendend OAI