-- Copyright (c) 2026 Kyle Clouthier / Clouthier Simulation Labs.
/-
  Cairn — the TRUSTED STATEMENT SPEC for the comparator CI job.

  This file is the complete list of what the Cairn Lean proofs claim: every
  definition the theorem statements depend on, plus each of the 18 audited
  theorems restated verbatim with a `sorry` proof. The Lean FRO's comparator
  (github.com/leanprover/comparator) guarantees that Cairn's closed proof
  files prove EXACTLY these statements — same names, same types, no more and
  no less — using only the axioms propext / Quot.sound / Classical.choice,
  with every proof replayed in the Lean kernel. Nothing is claimed beyond
  what is written here, and nothing about how the proofs (or the system)
  work is disclosed here. Lean 4 core only; no dependencies.
-/

/-! ## Static partition/revocation bounds

A voucher lives in a partition island and carries a cert-bound region. The
flagged subject sits in island `F`. Admission requires at least `T` vouchers
co-located with the subject (same island — a voucher across a partition
cannot be reached) spanning at least 2 distinct regions. A scoped revocation
removes the vouchers of its scope-island. -/

structure Voucher where
  island : Nat
  region : Nat
deriving DecidableEq

/-- Vouchers reachable by a subject in island `F` (same partition component). -/
def coLocated (vs : List Voucher) (F : Nat) : List Voucher :=
  vs.filter (fun v => v.island == F)

/-- At least two DISTINCT regions appear among `vs`. -/
def twoRegions (vs : List Voucher) : Prop :=
  ∃ a ∈ vs, ∃ b ∈ vs, a.region ≠ b.region

/-- Admission of a subject in island `F`: at least `T` co-located vouchers
    spanning at least 2 distinct regions. -/
def admit (vs : List Voucher) (F T : Nat) : Prop :=
  T ≤ (coLocated vs F).length ∧ twoRegions (coLocated vs F)

/-- A scoped revocation removes the vouchers that belong to scope-island `s`. -/
def revokeScope (vs : List Voucher) (s : Nat) : List Voucher :=
  vs.filter (fun v => v.island != s)

/-- Completeness is partition-local: a voucher in a DIFFERENT island than the
    flagged subject cannot change the subject's admission. -/
theorem completeness_partition_local
    (v : Voucher) (vs : List Voucher) (F T : Nat) (h : v.island ≠ F) :
    admit (v :: vs) F T ↔ admit vs F T := sorry

/-- If the flagged subject is admitted at all, the vouchers CO-LOCATED with it
    already meet the full admission bound. -/
theorem admit_forces_local_bound
    (vs : List Voucher) (F T : Nat) (h : admit vs F T) :
    T ≤ (coLocated vs F).length ∧ twoRegions (coLocated vs F) := sorry

/-- Safety: a subject in island `Ix ≠ s` sees the exact same co-located
    vouchers before and after a scoped revocation aimed at scope `s`. -/
theorem safety_scope_confined
    (vs : List Voucher) (s Ix : Nat) (h : Ix ≠ s) :
    coLocated (revokeScope vs s) Ix = coLocated vs Ix := sorry

/-- Decoupling: a scoped revocation at the flagged island `F` leaves every
    honest out-of-scope subject's admission untouched. -/
theorem decoupling_holds_together
    (vs : List Voucher) (F T Ix : Nat) (hIx : Ix ≠ F) :
    (admit (revokeScope vs F) Ix T ↔ admit vs Ix T) := sorry

/-- Effectiveness: after a scoped revocation aimed at `s`, no voucher
    co-located with a subject in scope `s` remains. -/
theorem revoke_clears_scope (vs : List Voucher) (s : Nat) :
    coLocated (revokeScope vs s) s = [] := sorry

/-- Liveness consequence: a subject whose entire support sits in the revoked
    scope `s` is no longer admitted, for any real threshold `0 < T`. -/
theorem revoked_in_scope_not_admitted
    (vs : List Voucher) (s T : Nat) (hT : 0 < T) : ¬ admit (revokeScope vs s) s T := sorry

/-- Non-vacuity: a concrete honest set — three co-located vouchers spanning
    three regions — IS admitted at `T = 3`. -/
theorem admission_is_satisfiable :
    admit [⟨0, 0⟩, ⟨0, 1⟩, ⟨0, 2⟩] 0 3 := sorry

/-! ## Dynamic complicity-cascade bounds

A voucher that counts as complicit for `k` CONSECUTIVE epochs is itself
flagged; flags persist. `Flagged` is the epoch-indexed flag state, closed
under initial compromise, persistence, and the `k`-window cascade rule. -/

abbrev Node := Nat

/-- `consec complicitAt k t n` : node `n` counted as complicit at every epoch
    of the length-`k` window `[t, t+k)`. -/
def consec (complicitAt : Nat → Node → Prop) (k t n : Nat) : Prop :=
  ∀ i, i < k → complicitAt (t + i) n

/-- Epoch-indexed flag state. `Flagged complicitAt initFlagged k t n` : node
    `n` is flagged at epoch `t`. Closed under three rules:
      * `init` -- an initially-compromised node is flagged (at every epoch);
      * `keep` -- flags persist to the next epoch (monotone; no un-revoke);
      * `casc` -- `k` consecutive complicit epochs flag the node at `t + k`. -/
inductive Flagged (complicitAt : Nat → Node → Prop) (initFlagged : Node → Prop) (k : Nat) :
    Nat → Node → Prop where
  | init {n : Node} (t : Nat) : initFlagged n → Flagged complicitAt initFlagged k t n
  | keep {t : Nat} {n : Node} :
      Flagged complicitAt initFlagged k t n → Flagged complicitAt initFlagged k (t + 1) n
  | casc {t n : Nat} :
      consec complicitAt k t n → Flagged complicitAt initFlagged k (t + k) n

/-- Completeness: `k` consecutive complicit epochs starting at `t` flag the
    node by epoch `t + k`. -/
theorem completeness
    (complicitAt : Nat → Node → Prop) (initFlagged : Node → Prop) (k t n : Nat)
    (h : consec complicitAt k t n) :
    Flagged complicitAt initFlagged k (t + k) n := sorry

/-- Persistence: once flagged at epoch `t`, flagged at every later epoch. -/
theorem persistence
    (complicitAt : Nat → Node → Prop) (initFlagged : Node → Prop) (k t n : Nat) :
    ∀ d, Flagged complicitAt initFlagged k t n → Flagged complicitAt initFlagged k (t + d) n := sorry

/-- Provenance: every flag has a cause — initial compromise or a real
    `k`-epoch complicity window. Flags are never spontaneous. -/
theorem flag_provenance
    (complicitAt : Nat → Node → Prop) (initFlagged : Node → Prop) (k : Nat) :
    ∀ t n, Flagged complicitAt initFlagged k t n →
      initFlagged n ∨ ∃ t', consec complicitAt k t' n := sorry

/-- Safety: a node that was not initially compromised and never sustains a
    `k`-epoch complicit window is NEVER flagged, at any epoch. -/
theorem safety
    (complicitAt : Nat → Node → Prop) (initFlagged : Node → Prop) (k n : Nat)
    (hinit : ¬ initFlagged n)
    (hnever : ∀ t', ¬ consec complicitAt k t' n) :
    ∀ t, ¬ Flagged complicitAt initFlagged k t n := sorry

/-- Grace, made explicit: a raw vouch for the flagged node counts as
    complicity only at or after the grace window closes (`flagEpoch + grace ≤ e`). -/
def counted (vouchedFor : Nat → Node → Prop) (flagEpoch grace : Nat) : Nat → Node → Prop :=
  fun e n => vouchedFor e n ∧ flagEpoch + grace ≤ e

/-- Grace excused: a node that was not initially compromised and whose backing
    of the flagged node stops before the grace window closes is NEVER flagged. -/
theorem grace_window_excused
    (vouchedFor : Nat → Node → Prop) (initFlagged : Node → Prop)
    (k flagEpoch grace n : Nat)
    (hinit : ¬ initFlagged n)
    (hstops : ∀ e, vouchedFor e n → e < flagEpoch + grace)
    (hk : 0 < k) :
    ∀ t, ¬ Flagged (counted vouchedFor flagEpoch grace) initFlagged k t n := sorry

/-- The informedness gate: a vouch counts only when it is post-grace AND the
    voucher has been INFORMED that the vouchee is flagged. -/
def countedInformed (vouchedFor informed : Nat → Node → Prop) (flagEpoch grace : Nat) : Nat → Node → Prop :=
  fun e n => vouchedFor e n ∧ flagEpoch + grace ≤ e ∧ informed e n

/-- Uninformed never flagged: a voucher that was never informed the vouchee is
    flagged (and was not initially compromised) is NEVER flagged, no matter
    how long it keeps vouching in good faith. -/
theorem uninformed_never_flagged
    (vouchedFor informed : Nat → Node → Prop) (initFlagged : Node → Prop)
    (k flagEpoch grace n : Nat)
    (hinit : ¬ initFlagged n)
    (huninformed : ∀ e, ¬ informed e n)
    (hk : 0 < k) :
    ∀ t, ¬ Flagged (countedInformed vouchedFor informed flagEpoch grace) initFlagged k t n := sorry

/-- Combined: a flag always has a real cause, and a real complicity window
    always produces a flag — over unbounded epochs, at unbounded N. -/
theorem cascade_sound_and_complete
    (complicitAt : Nat → Node → Prop) (initFlagged : Node → Prop) (k : Nat) :
    -- soundness: a flag always has a real cause
    (∀ t n, Flagged complicitAt initFlagged k t n →
        initFlagged n ∨ ∃ t', consec complicitAt k t' n)
    ∧
    -- completeness: a real complicity window always produces a flag
    (∀ t n, consec complicitAt k t n → Flagged complicitAt initFlagged k (t + k) n) := sorry

/-! ## Quantitative reach-cap Sybil bound

`C` vouchers each back at most `cap` admissions per window, so the total
admission budget is at most `C * cap` voucher-uses; each admitted subject
consumes at least `T` of them. `costs` lists the per-admission budget-costs
actually spent, so `costs.length` is the number of subjects admitted. The
bound `⌊C·cap/T⌋` never mentions how many Sybils were ATTEMPTED. -/

/-- Dependency-free sum over a `List Nat`. -/
def lsum : List Nat → Nat
  | []      => 0
  | x :: xs => x + lsum xs

/-- Double-counting step: if every admission costs at least `T` budget units,
    then `(#admissions) * T ≤ (total spent)`. -/
theorem len_mul_le_lsum (T : Nat) :
    ∀ l : List Nat, (∀ x ∈ l, T ≤ x) → l.length * T ≤ lsum l := sorry

/-- Sybil reach bound: with threshold `T > 0`, per-admission spend ≥ `T`, and
    total spend within the `C · cap` budget, the number of subjects admitted
    is at most `⌊ C · cap / T ⌋`. Nothing mentions the number of Sybils attempted. -/
theorem sybil_reach_bound
    (T C cap : Nat) (hT : 0 < T) (costs : List Nat)
    (hcost : ∀ c ∈ costs, T ≤ c) (hbudget : lsum costs ≤ C * cap) :
    costs.length ≤ C * cap / T := sorry

/-- Flat-in-K corollary: two schedules with the SAME budget (`C`, `cap`) obey
    the SAME admission ceiling, regardless of how many Sybils each attempted. -/
theorem flat_in_attempts
    (T C cap : Nat) (hT : 0 < T)
    (costs₁ costs₂ : List Nat)
    (h1 : ∀ c ∈ costs₁, T ≤ c) (hb1 : lsum costs₁ ≤ C * cap)
    (h2 : ∀ c ∈ costs₂, T ≤ c) (hb2 : lsum costs₂ ≤ C * cap) :
    costs₁.length ≤ C * cap / T ∧ costs₂.length ≤ C * cap / T := sorry

/-- Concrete instantiation: C = 3 compromised vouchers, cap = 1, T = 3 ⇒ at
    most ⌊3·1/3⌋ = 1 Sybil admitted, for any flood. -/
theorem sybil_bound_3_1_3
    (costs : List Nat) (hcost : ∀ c ∈ costs, 3 ≤ c) (hbudget : lsum costs ≤ 3 * 1) :
    costs.length ≤ 1 := sorry