import LeanMlir.Proofs.Certificates.IbpConvScorecardImgsA
import LeanMlir.Proofs.Certificates.IbpConvScorecardImgsB

/-! # IBP `L∞` conv scorecard — the aggregate

The counts, tied to the per-image `CertifiedAtLinf3` theorems of
`IbpConvScorecardImgsA/B.lean` over the net of `IbpConvScorecardNet.lean`.
See the net module's header for the certificate, the perturbation model, and
the theorem-vs-measurement split. Generated by `scripts/ibp_conv_scorecard.py`. -/

namespace Proofs
namespace IBP
namespace ConvNet

-- ═══════════════════════ the scorecard ═══════════════════════

/-- Certificate witnesses at ε = 1/255: `(test index, image, class)`. -/
noncomputable def certsE1 : List (ℕ × Tensor3 1 8 8 × Fin 10) :=
  [(0, img0, 7), (1, img1, 2), (2, img2, 1), (3, img3, 0), (4, img4, 4), (5, img5, 1), (8, img8, 5), (9, img9, 9)]

theorem certsE1_certified :
    ∀ p ∈ certsE1, CertifiedAtLinf3 net ((1:ℝ)/255) p.2.1 p.2.2 :=
  List.forall_iff_forall_mem.mp
    ⟨cert0e1, cert1e1, cert2e1, cert3e1, cert4e1, cert5e1, cert8e1, cert9e1⟩

/-- Certificate witnesses at ε = 2/255: `(test index, image, class)`. -/
noncomputable def certsE2 : List (ℕ × Tensor3 1 8 8 × Fin 10) :=
  [(0, img0, 7), (1, img1, 2), (2, img2, 1), (3, img3, 0), (4, img4, 4), (5, img5, 1), (8, img8, 5)]

theorem certsE2_certified :
    ∀ p ∈ certsE2, CertifiedAtLinf3 net ((2:ℝ)/255) p.2.1 p.2.2 :=
  List.forall_iff_forall_mem.mp
    ⟨cert0e2, cert1e2, cert2e2, cert3e2, cert4e2, cert5e2, cert8e2⟩

/-- Certificate witnesses at ε = 4/255: `(test index, image, class)`. -/
noncomputable def certsE4 : List (ℕ × Tensor3 1 8 8 × Fin 10) :=
  [(0, img0, 7), (1, img1, 2), (2, img2, 1), (3, img3, 0), (4, img4, 4), (5, img5, 1)]

theorem certsE4_certified :
    ∀ p ∈ certsE4, CertifiedAtLinf3 net ((4:ℝ)/255) p.2.1 p.2.2 :=
  List.forall_iff_forall_mem.mp
    ⟨cert0e4, cert1e4, cert2e4, cert3e4, cert4e4, cert5e4⟩

/-- Certificate witnesses at ε = 8/255: `(test index, image, class)`. -/
noncomputable def certsE8 : List (ℕ × Tensor3 1 8 8 × Fin 10) :=
  [(0, img0, 7), (2, img2, 1), (5, img5, 1)]

theorem certsE8_certified :
    ∀ p ∈ certsE8, CertifiedAtLinf3 net ((8:ℝ)/255) p.2.1 p.2.2 :=
  List.forall_iff_forall_mem.mp
    ⟨cert0e8, cert2e8, cert5e8⟩

/-- **The proved core of the scorecard.** Each count is tied to its per-image
    `CertifiedAtLinf3` proofs, not to a list length. These are the 8 images
    that carry Lean certificates — NOT the measured dataset counts (see the header:
    79/100, 73/100, 47/100, 13/100 at
    ε = 1, 2, 4, 8/255), which are exact-rational measurements rather than theorems.
    The engine is what makes them sound; the images only witness non-vacuity. -/
theorem scorecard_ibp_conv :
(certsE1.length = 8 ∧
      ∀ p ∈ certsE1, CertifiedAtLinf3 net ((1:ℝ)/255) p.2.1 p.2.2)
  ∧ (certsE2.length = 7 ∧
      ∀ p ∈ certsE2, CertifiedAtLinf3 net ((2:ℝ)/255) p.2.1 p.2.2)
  ∧ (certsE4.length = 6 ∧
      ∀ p ∈ certsE4, CertifiedAtLinf3 net ((4:ℝ)/255) p.2.1 p.2.2)
  ∧ (certsE8.length = 3 ∧
      ∀ p ∈ certsE8, CertifiedAtLinf3 net ((8:ℝ)/255) p.2.1 p.2.2) :=
  ⟨⟨rfl, certsE1_certified⟩, ⟨rfl, certsE2_certified⟩, ⟨rfl, certsE4_certified⟩, ⟨rfl, certsE8_certified⟩⟩

end ConvNet
end IBP
end Proofs