aime-1983-p9

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

import Mathlib

set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat

theorem aime_1983_p9 (x : ℝ) (h₀ : 0 < x ∧ x < Real.pi) :
  12 ≤ (9 * (x ^ 2 * Real.sin x ^ 2) + 4) / (x * Real.sin x) := by
  sorry

The swarm split this goal into helper sub-lemmas, proved them separately, and composed them back into the parent proof (unsorry ADR-009). Decomposed by afnz-zbook-b336.

• aime-1983-p9-s1

  proved

  Attribution inferred from git history (no explicit solver credit).

• aime-1983-p9-s2

  proved

  Attribution inferred from git history (no explicit solver credit).

• aime-1983-p9-s3

  proved

  Attribution inferred from git history (no explicit solver credit).

Runs (6)