No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
77def printProbability : IO Unit := do
proof body
Definition body.
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). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
main
in IndisputableMonolith.CPM.AuditMain
decl_use
depends on (12)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
independent
in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
decl_use
-
coincidence_negligible
in IndisputableMonolith.CPM.ConstantsAudit
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
probability
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
independent
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
probability
in IndisputableMonolith.QFT.SMatrixUnitarity
decl_use
-
probability
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use