/-
Small runs, checked by the kernel alone (`decide`), to show what the certificate accepts and rejects.
SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-/
import Growth.Theorems

namespace Growth
open Run

/-- Four points in a row, 10 apart. Origin 0 starts at 0 and origin 3 at 4 (slots every 4); budget 2.
    Each claims one neighbour (at 10 and 14), and their waves meet on link 1–2 at (10 + 10 + 14) / 2 = 17. -/
def tiny : Run := {
  points := [(0, 0), (10, 0), (20, 0), (30, 0)],
  edges := [(0, 1, 10), (1, 2, 10), (2, 3, 10)],
  pace := 1, cap := 2, every := 4, hold := 1, fade := 1,
  trees := [(0, 0, none, some 34), (1, 4, none, some 34)],
  claims := [(0, 0, 0, 0), (3, 1, 4, 1), (1, 0, 10, 0), (2, 1, 14, 1)],
  halves := [(0, 1, 20, 1), (1, 2, 28, 1), (2, 2, 34, 2), (3, 1, 34, 2)],
  meetings := [(2, 3)]
}

theorem tiny_valid : tiny.Valid := by decide

/-- Point 1 claimed at 9: its branch is not as long as the time it took. -/
def notTight : Run := { tiny with claims := [(0, 0, 0, 0), (3, 1, 4, 1), (1, 0, 9, 0), (2, 1, 14, 1)] }

theorem notTight_rejected : ¬ notTight.Tight := by decide

/-- The same trees without their meeting, under a budget of zero: each grows a branch it may not have. -/
def overBudget : Run := { tiny with cap := 0, trees := [(0, 0, none, none), (1, 4, none, none)], halves := [(0, 1, 20, 1), (1, 2, 28, 1), (2, 2, 34, 0), (3, 1, 34, 0)], meetings := [] }

theorem overBudget_rejected : ¬ overBudget.Budget := by decide

/-- Origin 3's tree also claims point 1 at 24 while origin 0's tree still holds it. -/
def heldTwice : Run := { tiny with claims := [(0, 0, 0, 0), (3, 1, 4, 1), (1, 0, 10, 0), (2, 1, 14, 1), (1, 1, 24, 3)] }

theorem heldTwice_rejected : ¬ heldTwice.Exclusive := by decide

/-- A half from point 2 drawn 26 along a link only 10 long. -/
def overlong : Run := { tiny with halves := [(0, 1, 20, 1), (1, 2, 28, 1), (2, 2, 34, 2), (3, 1, 80, 2)] }

theorem overlong_rejected : ¬ overlong.Halves := by decide

/-- The meeting placed at 16 instead of where the waves meet, at 17. -/
def misplacedMeeting : Run := { tiny with trees := [(0, 0, none, some 32), (1, 4, none, some 32)], halves := [(0, 1, 20, 1), (1, 2, 28, 1), (2, 2, 32, 2), (3, 1, 32, 2)] }

theorem misplacedMeeting_rejected : ¬ misplacedMeeting.Meetings := by decide

/-- The second origin starting at 3, between origin slots. -/
def offSlot : Run := { tiny with trees := [(0, 0, none, some 34), (1, 3, none, some 34)], claims := [(0, 0, 0, 0), (3, 1, 3, 1), (1, 0, 10, 0), (2, 1, 13, 1)] }

theorem offSlot_rejected : ¬ offSlot.Origins := by decide

end Growth