theorem proved term proof

`r_in_detectable_range`

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

formal statement (Lean)

  67theorem r_in_detectable_range :
  68    tensor_to_scalar 60 > 0 ∧ tensor_to_scalar 50 > 0 := by

proof body

Term-mode proof.

  69  unfold tensor_to_scalar
  70  constructor <;> (apply div_pos (mul_pos (by norm_num : (0:ℝ) < 12) alpha_attractor_pos)
  71                    (by positivity))
  72
  73/-! ## Log-Periodic Modulation -/
  74
  75/-- The optimal recognition ratio: X_opt = φ/π.
  76    This is the ratio at which recognition cost and geometric constraint
  77    are in balance. -/

depends on (11)

Lean names referenced from this declaration's body.

tensor_to_scalar in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
alpha_attractor_pos in IndisputableMonolith.Gravity.Inflation decl_use
tensor_to_scalar in IndisputableMonolith.Gravity.Inflation decl_use
X_opt in IndisputableMonolith.Gravity.Inflation decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use