module module

`IndisputableMonolith.Verification.Exclusivity.PredictionMap`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (14)

structure DimensionlessObservables L34
def rsObservables L40
def withinBounds L46
theorem rs_within_bounds L52
structure Predictor L57
def rsPredictionMap L62
theorem bridge_B5_prediction_map_exists L68
def componentwiseClose L75
def withinMicroWindow L81
def microWidth L85
theorem close_to_same_reference L89
theorem rs_within_micro_window L104
theorem prediction_map_unique L115
theorem prediction_map_matches_bounds L131