formatConstant

formal source

  15open IndisputableMonolith.CPM.ConstantsAudit
  16
  17/-- Format a verified constant for display. -/
  18def formatConstant (name source : String) (exact : Bool) : String :=
  19  let exactStr := if exact then "exact" else "approximate"
  20  s!"  • {name} ({exactStr})\n    Source: {source}"
  21
  22/-- Print the audit report header. -/
  23def printHeader : IO Unit := do
  24  IO.println "╔══════════════════════════════════════════════════════════════╗"
  25  IO.println "║           CPM Constants Audit Report                         ║"
  26  IO.println "║           Recognition Physics Institute                      ║"
  27  IO.println "╚══════════════════════════════════════════════════════════════╝"
  28  IO.println ""
  29
  30/-- Print verified constants section. -/
  31def printConstants : IO Unit := do
  32  IO.println "┌─────────────────────────────────────────────────────────────┐"
  33  IO.println "│ Verified Constants                                          │"
  34  IO.println "└─────────────────────────────────────────────────────────────┘"
  35  IO.println ""
  36  IO.println "  CPM Core Constants:"
  37  IO.println "  • K_net (cone) = 1"
  38  IO.println "    Source: Intrinsic cone projection"
  39  IO.println ""
  40  IO.println "  • K_net (eight-tick) = (9/7)² = 81/49"
  41  IO.println "    Source: ε=1/8 covering, refined analysis"
  42  IO.println ""
  43  IO.println "  • C_proj = 2"
  44  IO.println "    Source: Hermitian rank-one bound, J''(1)=1"
  45  IO.println ""
  46  IO.println "  • C_eng = 1"
  47  IO.println "    Source: Standard energy normalization"
  48  IO.println ""