MaxLeafFormal.RSCFinalExtras

Source file MaxLeafFormal/RSCFinalExtras.lean of the Lean project (how it is built).

Statements of the paper formalised here: Proposition D.5.23.

import MaxLeafFormal.RSCFinal
import MaxLeafFormal.RSCCheckExtras
import MaxLeafFormal.RSCData.Extras.All

/-!
# The exact `c_Z` and `prop:rsc-cert` with its stages

`certZ_cZ_eq` gives the exact value of `c_Z` for `certZ`; `rsc_cert_full` is `prop:rsc-cert`
with its stage clause and the scalar hypotheses of `lem:rsc-cert`.
The shard theorems of `MaxLeafFormal.RSCData` and `MaxLeafFormal.RSCData.Extras` are decided by
`native_decide`, so the theorems here that use the data also trust the Lean compiler:
`#print axioms` lists one auxiliary axiom per shard theorem used. `rsc_stage_j` and `rsc_j_one` use
no data.

This module is not imported by `MaxLeafFormal.lean`. Build with
`lake build MaxLeafFormal.RSCFinalExtras` after generating the data (see `RSCFinal`) and checking
`RSCData/Extras/MANIFEST.sha256`.
-/

namespace MaxLeafFormal.RSCFinal
open MaxLeafFormal.RSCCert MaxLeafFormal.RSCParams
open MaxLeafFormal.Antinorm8 (RTree size PZ fin cZ initInf)
open Pointwise
noncomputable section

/-- The exact value of c_Z for the certificate. -/
theorem certZ_cZ_eq : cZ p₂ certZ certZ_nonempty =
    (123019910197327428728743 / 202985322574630920671369 : ℝ) := by
  have h := RSCCheck.checkCZ_sound RSCData.Extras.cZ_ok certZ_nonempty
  show cZ p₂ (RSCCheck.finsetOf RSCData.Z) certZ_nonempty = _
  rw [h]
  norm_num

/-- "c_Z = 0.60605…" in the proof of `prop:rsc-cert`. -/
theorem certZ_cZ_digits :
    (60605/100000 : ℝ) < cZ p₂ certZ certZ_nonempty ∧ cZ p₂ certZ certZ_nonempty < 60606/100000 := by
  rw [certZ_cZ_eq]
  constructor <;> norm_num

/-- The chain lengths j of (C5) for the five staged points. -/
theorem rsc_stage_j : jOf d₃ 1 = 2 ∧ jOf d₂ 1 = 3 ∧ jOf d₂ 2 = 2 := by
  refine ⟨?_, ?_, ?_⟩ <;> decide

/-- Every other point of (C5) has j = 1 (the remark after `prop:rsc-cert`). -/
theorem rsc_j_one : ∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
    ¬ (ν = 1 ∨ (ν = 2 ∧ 1 ≤ c₂)) → (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) = 1 := by
  intro ν h1 _ c₂ c₃ _ _ h5
  have hn1 : ν ≠ 1 := fun h => h5 (Or.inl h)
  have hn2 : ν = 2 → c₂ = 0 := fun h => by
    by_contra hc
    exact h5 (Or.inr ⟨h, Nat.one_le_iff_ne_zero.2 hc⟩)
  unfold jOf
  split_ifs with hc
  · have : d₃ ν ≤ 2 := by
      unfold d₃
      split_ifs <;> omega
    exact max_eq_left (by omega)
  · have hne2 : ν ≠ 2 := fun h => hc (hn2 h)
    have : d₂ ν ≤ 2 := by
      unfold d₂
      split_ifs <;> omega
    exact max_eq_left (by omega)

/-- prop:rsc-cert as stated, with its stage clause, and with the scalar hypotheses of
lem:rsc-cert that its proof checks and that the proof of prop:rsc-bound takes from it. -/
theorem rsc_cert_full :
    ∃ (Z : Finset (Fin 8 → ℝ)) (hZ : Z.Nonempty),
      Z.card = 1024 ∧ (∀ z ∈ Z, 0 ≤ z ∧ ∀ s, ∃ r : ℚ, z s = (r : ℝ)) ∧
      (6060/10000 : ℝ) < cZ p₂ Z hZ ∧
      (∀ z ∈ Z, ∀ z' ∈ Z, merge p₂ p₃ z z' ∈ PZ Z) ∧                                   -- (C1)
      ((∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ Z) ∧
        initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ Z) ∧                                          -- (C2)
      (∀ ν, 1 ≤ ν → ν ≤ νE → (∀ d, 1 ≤ d → d < d₃ ν → Light₃ p₂ p₃ y ν d) ∧
        (∀ d, 1 ≤ d → d < d₂ ν → Light₂ p₂ p₃ y ν d)) ∧                                 -- (C3)
      (∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
        (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ Z) ∧
        (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
          init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ Z)) ∧                          -- (C4)
      (∀ ν, 1 ≤ ν → ν ≤ νE → ∀ c₂ c₃, 1 ≤ c₂ + c₃ → c₂ + c₃ ≤ ν →
        ∀ Qs : List (Fin 8 → ℝ), Qs.length = (if c₂ = 0 then jOf d₃ ν else jOf d₂ ν) →
        (∀ Q ∈ Qs, Q ∈ PZ Z ∧ 0 ≤ Q) →
        Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ Z) ∧ -- (C5)
      ((1 - p₃) / ê) ^ (νE + 1) ≥ ê⁻¹ ^ (ν₀ + 1) ∧                                     -- (C6)
      -- stages; each chain has the length j of (C5)
      (∃ Y₁ : Finset (Fin 8 → ℝ), Y₁.card = 62 ∧ [Y₁].length + 1 = jOf d₃ 1 ∧
        IsStages p₂ p₃ Z ((ê ^ (1 + 1))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ 1 0 1) [Y₁]) ∧
      (∃ Y₁ Y₂ : Finset (Fin 8 → ℝ), Y₁.card = 62 ∧ Y₂.card = 304 ∧ [Y₁, Y₂].length + 1 = jOf d₂ 1 ∧
        IsStages p₂ p₃ Z ((ê ^ (1 + 1))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ 1 1 0) [Y₁, Y₂]) ∧
      (∃ Y₁ : Finset (Fin 8 → ℝ), Y₁.card = 61 ∧ [Y₁].length + 1 = jOf d₂ 2 ∧
        IsStages p₂ p₃ Z ((ê ^ (1 + 2))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ 2 1 0) [Y₁]) ∧
      (∃ Y₁ : Finset (Fin 8 → ℝ), Y₁.card = 62 ∧ [Y₁].length + 1 = jOf d₂ 2 ∧
        IsStages p₂ p₃ Z ((ê ^ (1 + 2))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ 2 1 1) [Y₁]) ∧
      (∃ Y₁ : Finset (Fin 8 → ℝ), Y₁.card = 62 ∧ [Y₁].length + 1 = jOf d₂ 2 ∧
        IsStages p₂ p₃ Z ((ê ^ (1 + 2))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ 2 2 0) [Y₁]) ∧
      -- scalar hypotheses of lem:rsc-cert, as in rsc_side and rsc_rsccredits.1
      ((0 < p₂ ∧ p₂ ≤ p₃ ∧ p₃ < 1/2) ∧ 0 < y ∧
        (1 ≤ ϖ₂ ∧ ϖ₂ ≤ 2 * (1 - p₂) ∧ 1 ≤ ϖ₃ ∧ ϖ₃ ≤ 2 * (1 - p₃)) ∧
        (0 < ê ∧ ê < 1 - p₃) ∧ 1 ≤ νE ∧ ∀ ν, 1 ≤ ν → ν ≤ νE → 1 ≤ d₃ ν ∧ d₃ ν ≤ d₂ ν) := by
  obtain ⟨A0, hA0c, hA0⟩ := RSCCheck.stages_one RSCData.Z_ok RSCData.St_0_pts.key
    RSCData.Extras.sz_0 RSCData.Extras.facts_0
  obtain ⟨A1, B1, hA1c, hB1c, hAB1⟩ := RSCCheck.stages_two RSCData.Z_ok RSCData.St_1_pts.key
    RSCData.Extras.sz_1 RSCData.Extras.facts_1
  obtain ⟨A2, hA2c, hA2⟩ := RSCCheck.stages_one RSCData.Z_ok RSCData.St_2_pts.key
    RSCData.Extras.sz_2 RSCData.Extras.facts_2
  obtain ⟨A3, hA3c, hA3⟩ := RSCCheck.stages_one RSCData.Z_ok RSCData.St_3_pts.key
    RSCData.Extras.sz_3 RSCData.Extras.facts_3
  obtain ⟨A4, hA4c, hA4⟩ := RSCCheck.stages_one RSCData.Z_ok RSCData.St_4_pts.key
    RSCData.Extras.sz_4 RSCData.Extras.facts_4
  exact ⟨certZ, certZ_nonempty, certZ_card, fun z hz => ⟨certZ_nonneg z hz, certZ_rational z hz⟩,
    certZ_cZ, certZ_C1, certZ_C2, rsc_C3, certZ_C4, certZ_C5, rsc_C6,
    ⟨A0, hA0c, by simp [rsc_stage_j], hA0⟩,
    ⟨A1, B1, hA1c, hB1c, by simp [rsc_stage_j], hAB1⟩,
    ⟨A2, hA2c, by simp [rsc_stage_j], hA2⟩,
    ⟨A3, hA3c, by simp [rsc_stage_j], hA3⟩,
    ⟨A4, hA4c, by simp [rsc_stage_j], hA4⟩,
    ⟨rsc_side.1, rsc_side.2.1, rsc_rsccredits.1, rsc_side.2.2.1, rsc_side.2.2.2.1,
      rsc_side.2.2.2.2⟩⟩

end
end MaxLeafFormal.RSCFinal
Back to top