MaxLeafFormal.RSCFinal

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

Statements of the paper formalised here: Lemma D.5.20, Proposition D.5.23.

import MaxLeafFormal.RSCCheck
import MaxLeafFormal.RSCData.All

/-!
# `prop:rsc-cert` and the assembled RSC tree bound

`certZ` is the point set of `rsc-certificate.json`, exported to `MaxLeafFormal.RSCData` and checked
by the checkers of `MaxLeafFormal.RSCCheck`. 466 of the generated shard theorems 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 such theorem. The 11 size side conditions (`nb_…`) are
decided by `decide +kernel`. Everything else, the soundness theorems
of `RSCCheck` included, is kernel-checked. The data conditions (C1), (C2), (C4), (C5) of
`lem:rsc-cert` follow from the shard checks through those soundness theorems; (C3) and (C6) are
`RSCParams.rsc_C3` and `RSCParams.rsc_C6`. The final bound applies
`RSCParams.rsc_tree_bound_of_data` to these.

This module is not imported by `MaxLeafFormal.lean`. The data modules are generated, not shipped:
from the top folder of the ancillary files run
`python3 formal/scripts/export_rsc_cert.py rsc/rsc-certificate.json.gz formal/MaxLeafFormal/RSCData`,
compare with `MaxLeafFormal/RSCData/MANIFEST.sha256`, then build with
`lake build MaxLeafFormal.RSCFinal` in `formal/`.
-/

namespace MaxLeafFormal.RSCFinal

open MaxLeafFormal.RSCCert MaxLeafFormal.RSCParams
open MaxLeafFormal.Antinorm8 (RTree size PZ fin cZ initInf)
open Pointwise

noncomputable section

/-- The point set Z of prop:rsc-cert: the 1024 rational points of `rsc-certificate.json`. -/
def certZ : Finset (Fin 8 → ℝ) := RSCCheck.finsetOf RSCData.Z

theorem certZ_card : certZ.card = 1024 := by
  unfold certZ RSCCheck.finsetOf
  rw [List.toFinset_card_of_nodup (RSCCheck.checkZ_nodup RSCData.Z_ok), List.length_map,
    RSCCheck.checkZ_length RSCData.Z_ok]

theorem certZ_nonempty : certZ.Nonempty :=
  Finset.card_pos.1 (by rw [certZ_card]; norm_num)

theorem certZ_nonneg : ∀ z ∈ certZ, 0 ≤ z := by
  intro z hz
  unfold certZ RSCCheck.finsetOf at hz
  obtain ⟨P, -, rfl⟩ := List.mem_map.1 (List.mem_toFinset.1 hz)
  exact RSCCheck.val_nonneg P

theorem certZ_rational : ∀ z ∈ certZ, ∀ s, ∃ r : ℚ, z s = (r : ℝ) := by
  intro z hz s
  unfold certZ RSCCheck.finsetOf at hz
  obtain ⟨P, -, rfl⟩ := List.mem_map.1 (List.mem_toFinset.1 hz)
  exact ⟨((P.1.getD s 0 : ℕ) : ℚ) / (P.2 : ℚ), by simp [RSCCheck.val]⟩

theorem certZ_cZ : (6060/10000 : ℝ) < cZ p₂ certZ certZ_nonempty :=
  (Finset.lt_inf'_iff _).2 (RSCCheck.checkZ_fin RSCData.Z_ok)

/-- (C1). -/
theorem certZ_C1 : ∀ z ∈ certZ, ∀ z' ∈ certZ, merge p₂ p₃ z z' ∈ PZ certZ :=
  RSCData.c1_fact

/-- (C2). -/
theorem certZ_C2 : (∀ ν ≤ ν₀, init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ certZ) ∧
    initInf p₂ y ∈ ê ^ (ν₀ + 2) • PZ certZ :=
  RSCCheck.checkC2_sound (RSCCheck.checkZ_okPts RSCData.Z_ok) RSCData.C2.ok

theorem certZ_init00 (ν : ℕ) : init p₂ p₃ y ϖ₂ ϖ₃ ν 0 0 ∈ ê ^ (1 + ν) • PZ certZ :=
  RSCCheck.init00_mem certZ_nonneg certZ_C2 ν

/-- (C4). -/
theorem certZ_C4 : ∀ ν, 2 ≤ ν → ν ≤ νE → d₃ ν ≤ 1 →
    (∀ c₃, 1 ≤ c₃ → c₃ ≤ ν - 1 → init p₂ p₃ y ϖ₂ ϖ₃ ν 0 c₃ ∈ ê ^ (1 + ν) • PZ certZ) ∧
    (d₂ ν ≤ 1 → ∀ c₂ c₃, 1 ≤ c₂ → c₂ + c₃ ≤ ν - 1 →
      init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃ ∈ ê ^ (1 + ν) • PZ certZ) :=
  RSCCheck.checkLattice4_sound (RSCCheck.checkZ_okPts RSCData.Z_ok) certZ_init00
    RSCData.leafTable_ok RSCData.lat4_ok

/-- (C5). -/
theorem certZ_C5 : ∀ ν, 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 certZ ∧ 0 ≤ Q) →
    Qs.foldl (merge p₂ p₃) ((ê ^ (1 + ν))⁻¹ • init p₂ p₃ y ϖ₂ ϖ₃ ν c₂ c₃) ∈ PZ certZ :=
  RSCCheck.checkLattice5_sound (RSCCheck.checkZ_okPts RSCData.Z_ok) certZ_C1 certZ_init00
    RSCData.chainTable_ok RSCData.lat5_ok

/-- prop:rsc-cert (without the stage sizes). -/
theorem rsc_cert :
    ∃ (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)
  ⟨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⟩

/-- The RSC tree bound: lem:rsc-cert for the certificate of prop:rsc-cert. -/
theorem rsc_tree_bound (t : RTree Label) (ht : Admissible p₂ p₃ y t) :
    (6060/10000 : ℝ) * ê ^ (size t + nuSum t) ≤ fin p₂ (message p₂ p₃ y ϖ₂ ϖ₃ t) := by
  have h := rsc_tree_bound_of_data certZ certZ_nonempty certZ_nonneg certZ_C1 certZ_C2 certZ_C4
    certZ_C5 t ht
  have hc := certZ_cZ
  have hê : 0 ≤ ê ^ (size t + nuSum t) := pow_nonneg (by norm_num [ê]) _
  nlinarith

end

end MaxLeafFormal.RSCFinal
Back to top