module module

`IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle`

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

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Measurement.RecognitionAngle.BlindCone module_import
IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.ClassicalResults module_import

declarations in this module (9)

abbrev R3 L29
def dir L32
def angleAt L38
def A_of_theta L46
def thetaMin L49
theorem action_small_angle_diverges L56
theorem theta_min_spec L62
theorem theta_min_range L70
theorem infeasible_below_thetaMin L76