def definition def or abbrev

`thetaMin`

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

formal statement (Lean)

  49def thetaMin (Amax : ℝ) : ℝ := Real.arcsin (Real.exp (-Amax))

proof body

Definition body.

  50
  51/-! ## Core limit and threshold lemmas (via classical results) -/
  52
  53open Filter
  54
  55/-- As θ → 0⁺, the kernel action `A_of_theta θ = -log(sin θ)` diverges to `+∞`. -/

used by (6)

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

infeasible_below_thetaMin in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
theta_min_range in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
theta_min_spec in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
R3 in IndisputableMonolith.Measurement.RecognitionAngle.BlindCone decl_use
angleOK in IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating decl_use
no_feasible_if_angle_below_threshold in IndisputableMonolith.Measurement.RecognitionAngle.TemporalGating decl_use

depends on (5)

Lean names referenced from this declaration's body.

kernel in IndisputableMonolith.Cosmology.BITKernelFamilies decl_use
via in IndisputableMonolith.Derivations.MassToLight decl_use
kernel in IndisputableMonolith.ILG.Kernel decl_use
A_of_theta in IndisputableMonolith.Measurement.RecognitionAngle.ActionSmallAngle decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use