module module

`IndisputableMonolith.Verification.Exclusivity.Observables`

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.Constants.ExternalAnchors module_import

declarations in this module (19)

structure DimensionlessObservables L58
def alpha_inv_derived L84
def electron_muon_derived L90
def proton_electron_derived L96
def dimensionless_G_derived L102
def rsObservables L108
structure EmpiricalBounds L126
def empiricalBounds L141
def withinBounds L154
theorem rs_within_bounds L173
structure PredictionFunction L186
def DerivesObservablesStrong L199
structure DerivesObservablesWitness L204
def unitPrediction L214
def rsDerivesObservables L219
theorem rs_derives_observables_strong L224
def badPrediction L230
theorem bad_prediction_fails L240
theorem bad_framework_fails_strong L253