module module

`IndisputableMonolith.Verification.AnchorNonCircularityCert`

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 (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Physics.AnchorPolicy module_import
IndisputableMonolith.Physics.RGTransport module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (18)

structure SMBetaStructure L59
def canonicalSMBeta L68
theorem stationarity_structural L83
theorem beta_is_mass_independent L89
theorem lambda_from_phi L95
theorem muStar_positive L98
structure StationarityCert L104
def certified_stationarity_bounds L116
structure DispersionMinCert L123
def certified_dispersion_minimum L136
structure NonCircularityCert L147
def is_mass_independent L162
def is_parameter_free L170
def canonical_anchor_cert L176
theorem anchor_mass_independent L188
theorem anchor_parameter_free L194
theorem anchor_value L204
theorem anchor_scale_certified L217