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)
14structure AuditItem where
15 name : String
16 category : String
17 status : String -- "Proven" | "Scaffold" | "Planned"
18 usesExternalInput : Bool
19 value : Option String := none
proof body
Definition body.
20deriving Repr
21
22/-! Numeric helpers for rational approximations (pure, computable). -/
23
24namespace NumFmt
25
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
f_gap
in IndisputableMonolith.Constants.AlphaHigherOrder
decl_use
-
f_gap
in IndisputableMonolith.Constants.GapWeight
decl_use
-
status
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
status
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
via
in IndisputableMonolith.Derivations.MassToLight
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
status
in IndisputableMonolith.Measurement.RSNative.Alignment
decl_use
-
status
in IndisputableMonolith.Measurement.RSNative.Alignment
decl_use
-
f_gap
in IndisputableMonolith.Pipelines
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
value
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
boolToJson
in IndisputableMonolith.URCAdapters.Audit
decl_use
-
quote
in IndisputableMonolith.URCAdapters.Audit
decl_use