`AuditItem`

definition

show as: view math explainer →

module: IndisputableMonolith.URCAdapters.Audit
domain: URCAdapters
line: 14 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.URCAdapters.Audit on GitHub at line 14.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  11scale-declared running quantities.
  12-/
  13
  14structure AuditItem where
  15  name              : String
  16  category          : String
  17  status            : String   -- "Proven" | "Scaffold" | "Planned"
  18  usesExternalInput : Bool
  19  value             : Option String := none
  20deriving Repr
  21
  22/-! Numeric helpers for rational approximations (pure, computable). -/
  23
  24namespace NumFmt
  25
  26def pow10 (d : Nat) : Nat := Nat.pow 10 d
  27
  28def padLeftZeros (s : String) (len : Nat) : String :=
  29  let deficit := if s.length ≥ len then 0 else len - s.length
  30  let rec mkZeros (n : Nat) (acc : String) : String :=
  31    match n with
  32    | 0 => acc
  33    | n+1 => mkZeros n ("0" ++ acc)
  34  mkZeros deficit s
  35
  36/-- Render a rational q = n / m to a fixed d-decimal string. -/
  37def ratToDecimal (n : Int) (m : Nat) (d : Nat) : String :=
  38  let sign := if n < 0 then "-" else ""
  39  let nAbs : Nat := Int.natAbs n
  40  if m = 0 then sign ++ "NaN" else
  41  let scale := pow10 d
  42  let scaled : Nat := (nAbs * scale) / m
  43  let ip : Nat := scaled / scale
  44  let fp : Nat := scaled % scale

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.