`bandLower_ratio`

proved

show as: view math explainer →

module: IndisputableMonolith.Unification.RecognitionBandGeometry
domain: Unification
line: 71 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Unification.RecognitionBandGeometry on GitHub at line 71.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  68  linarith [bandBoundaries_sum_to_one]
  69
  70/-- At the lower boundary, `ρ/(1-ρ) = 1/φ`. -/
  71theorem bandLower_ratio : rhoBandLower / (1 - rhoBandLower) = phi⁻¹ := by
  72  rw [one_sub_rhoBandLower_eq_rhoBandUpper]
  73  unfold rhoBandLower rhoBandUpper
  74  field_simp [phi_ne_zero]
  75
  76/-- At the upper boundary, `ρ/(1-ρ) = φ`. -/
  77theorem bandUpper_ratio : rhoBandUpper / (1 - rhoBandUpper) = phi := by
  78  rw [one_sub_rhoBandUpper_eq_rhoBandLower]
  79  unfold rhoBandLower rhoBandUpper
  80  field_simp [phi_ne_zero]
  81
  82theorem bandBoundaries_product : rhoBandLower * rhoBandUpper = phi⁻¹ ^ 3 := by
  83  unfold rhoBandLower rhoBandUpper
  84  ring
  85
  86end
  87end RecognitionBandGeometry
  88end Unification
  89end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.