printProbability

formal source

  74  IO.println ""
  75
  76/-- Print probability bounds section. -/
  77def printProbability : IO Unit := do
  78  IO.println "┌─────────────────────────────────────────────────────────────┐"
  79  IO.println "│ Probability Bounds                                          │"
  80  IO.println "└─────────────────────────────────────────────────────────────┘"
  81  IO.println ""
  82  IO.println "  Coincidence probability for CPM constants matching RS:"
  83  IO.println "  • Number of independent constants: 4"
  84  IO.println "  • Precision of each match: 3 decimal places"
  85  IO.println "  • Upper bound: 10^(-12)"
  86  IO.println ""
  87  IO.println "  ✓ coincidence_negligible: probability < 10^(-10)"
  88  IO.println ""
  89
  90/-- Print example witness section (standalone CPM). -/
  91def printExamples : IO Unit := do
  92  IO.println "┌─────────────────────────────────────────────────────────────┐"
  93  IO.println "│ Example Witness                                             │"
  94  IO.println "└─────────────────────────────────────────────────────────────┘"
  95  IO.println ""
  96  IO.println "  The CPM standalone certificate includes a toy-model witness."
  97  IO.println "  This confirms the A/B/C assumptions are consistent and usable."
  98  IO.println ""
  99
 100/-- Print audit summary. -/
 101def printSummary : IO Unit := do
 102  IO.println "┌─────────────────────────────────────────────────────────────┐"
 103  IO.println "│ Audit Summary                                               │"
 104  IO.println "└─────────────────────────────────────────────────────────────┘"
 105  IO.println ""
 106  IO.println "  Total verified constants: 9"
 107  IO.println "  Consistency checks passed: 4"