Geometric orientation fans. Every cone uses the same support triple at both endpoints. All inputs are propositions about real points, not Boolean checker results.
A lower support estimate witnessed by three contained points.
Equations
- ConwaySoifer.Simplified.SupportBound Q e = ∃ p₀ ∈ Q.carrier, ∃ p₁ ∈ Q.carrier, ∃ p₂ ∈ Q.carrier, ConwaySoifer.len e ≤ ConwaySoifer.supportNum e p₀ p₁ p₂
Instances For
Critically, one triple witnesses both ends of this cone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ConwaySoifer.Simplified.SupportBound.smul
{Q : EquilateralTriangle}
{e : Point}
(h : SupportBound Q e)
{a : ℝ}
(ha : 0 ≤ a)
:
SupportBound Q (a • e)
theorem
ConwaySoifer.Simplified.ConeBound.bound
{Q : EquilateralTriangle}
{u v l : Point}
(h : ConeBound Q u v)
(huv : 0 < cross u v)
(hul : 0 ≤ cross u l)
(hlv : 0 ≤ cross l v)
:
SupportBound Q l
A chain ending on the last boundary of a 120-degree orientation arc.
Equations
- ConwaySoifer.Simplified.SupportFan Q x✝ [] = (x✝ = ConwaySoifer.rot ConwaySoifer.eastDir ∧ ConwaySoifer.Simplified.SupportBound Q x✝)
- ConwaySoifer.Simplified.SupportFan Q x✝ (v :: vs) = (0 < ConwaySoifer.cross x✝ v ∧ ConwaySoifer.Simplified.ConeBound Q x✝ v ∧ ConwaySoifer.Simplified.SupportFan Q v vs)
Instances For
theorem
ConwaySoifer.Simplified.SupportFan.bound
{Q : EquilateralTriangle}
{l : Point}
(hl0 : l ≠ 0)
(hl1 : 0 ≤ cross eastDir l)
(hl2 : 0 ≤ cross l (rot eastDir))
(vs : List Point)
(u : Point)
:
SupportFan Q u vs → 0 ≤ cross u l → SupportBound Q l
theorem
ConwaySoifer.Simplified.one_le_side_of_fan
{Q : EquilateralTriangle}
(hq : 0 < Q.side)
{vs : List Point}
(hf : SupportFan Q eastDir vs)
:
theorem
ConwaySoifer.Simplified.support_of_sq
{u p₀ p₁ p₂ : Point}
(hN : 0 ≤ supportNum u p₀ p₁ p₂)
(hD : normSq u ≤ supportNum u p₀ p₁ p₂ ^ 2)
:
Polynomial inequalities imply a geometric support estimate without square roots.