IndisputableMonolith.Verification.Rendered

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Verification
   5namespace Rendered
   6
   7/-- Rendered summary of a dimensionless claim. -/
   8structure RenderedClaim where
   9  id        : String
  10  statement : String
  11  proved    : Bool
  12deriving Repr
  13
  14/-- Rendered gate specification (inputs and symbolic output). -/
  15structure GateSpec where
  16  id      : String
  17  inputs  : List String
  18  output  : String
  19deriving Repr
  20
  21/-- Zero-knobs proof bundle export: list of registered dimensionless theorems. -/
  22@[simp] def zeroKnobsExports : List String :=
  23  [ "K_gate", "cone_bound", "eight_tick_min", "period_exactly_8"
  24  , "dec_dd_eq_zero", "dec_bianchi", "display_speed_identity"
  25  , "gap_delta_time_identity", "recognition_lower_bound_sat" ]
  26
  27/-- Example rendered claims (placeholders; details live in core Verification). -/
  28@[simp] def dimlessClaimsRendered : List RenderedClaim :=
  29  [ { id := "K_gate",           statement := "(tau_rec/τ0) = (lambda_kin/ℓ0)", proved := true }
  30  , { id := "eight_tick_min",  statement := "8 ≤ minimal period",             proved := true }
  31  , { id := "period_exactly_8", statement := "∃ cover with period = 8",         proved := true } ]
  32
  33/-- Example rendered gates (symbolic). -/
  34@[simp] def gatesRendered : List GateSpec :=
  35  [ { id := "KGate"
  36    , inputs := ["u(ℓ0)", "u(λ_rec)", "k", "(optional) ρ", "K_B"]
  37    , output := "Z = |K_A - K_B| / (k · sqrt(u_ell0^2 + u_lrec^2)); passAt = (Z ≤ 1)" } ]
  38
  39end Rendered
  40end Verification
  41end IndisputableMonolith
  42