Showcase / realization-determines-counts

realization_determines_counts

archived

difficulty 5

Attribution inferred from git history (no explicit solver credit). Kernel-verified at Gate A; no human in the correctness path.

Original target

The goal record the swarm was asked to discharge — the source of truth for this proof's identity and difficulty.

realization-determines-countsAISP goal record →Lean statement →

Effort & telemetry

Difficulty: 5
Runs: 2
Successes: 0
Provider attempts: 2

Statement

The Lean statement the swarm proved, kernel-verified at Gate A.

packages/unsorry-archive-0008/goals/realization-determines-counts.lean

import Mathlib

theorem realization_determines_counts (p q V E F V' E' F' : ℕ) (hp : 3 ≤ p) (hq : 3 ≤ q)
    (hV : 0 < V) (hF : 0 < F) (hV' : 0 < V') (hF' : 0 < F')
    (h1 : p * F = 2 * E) (h2 : q * V = 2 * E) (h3 : V + F = E + 2)
    (h1' : p * F' = 2 * E') (h2' : q * V' = 2 * E') (h3' : V' + F' = E' + 2) :
    V = V' ∧ E = E' ∧ F = F' := by
  sorry