IndisputableMonolith.Ethics.Truth

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Ethics
   5
   6namespace Truth
   7  abbrev Claim := String
   8
   9  /-! Evidence ledger over claims with support/conflict relations. -/
  10  structure EvidenceLedger where
  11    universeClaims : List Claim
  12    supports : Claim → Claim → Bool
  13    conflicts : Claim → Claim → Bool
  14
  15  /-- Iterate a function `f` n times. -/
  16  def iterate {α} (f : α → α) : Nat → α → α
  17  | 0, x => x
  18  | Nat.succ n, x => iterate f n (f x)
  19
  20  /-- One closure step: add all ledger claims supported by any current claim. -/
  21  def step (E : EvidenceLedger) (current : List Claim) : List Claim :=
  22    let add := E.universeClaims.filter (fun b => current.any (fun a => E.supports a b))
  23    (current ++ add).eraseDups
  24
  25  /-- Supports-closure of a claim set within the ledger universe. -/
  26  def closure (E : EvidenceLedger) (S : List Claim) : List Claim :=
  27    iterate (step E) (E.universeClaims.length.succ) S
  28
  29  /-- Check for any conflict within the closure of a claim set. -/
  30  def hasConflict (E : EvidenceLedger) (S : List Claim) : Bool :=
  31    let C := closure E S
  32    let rec pairs : List Claim → Bool
  33    | [] => False
  34    | x :: xs => xs.any (fun y => E.conflicts x y || E.conflicts y x) || pairs xs
  35    pairs C
  36
  37  /-- Symmetric conflict count between request-closure and evidence-closure. -/
  38  def divergenceCount (E : EvidenceLedger) (S : List Claim) : Nat :=
  39    let Creq := closure E S
  40    let Cev := closure E E.universeClaims
  41    Creq.foldl (fun acc x =>
  42      Cev.foldl (fun acc2 y => acc2 + (if E.conflicts x y || E.conflicts y x then 1 else 0)) acc) 0
  43
  44end Truth
  45
  46end Ethics
  47end IndisputableMonolith
  48
  49