LeanPool.Erdos132ConvexK3.Assembly

theorem LeanPool.Erdos132ConvexK3.full_two_rung_shared_tip_degree_le_six {degree : ℕ} {F_s A B C : ℝ} (hSplit : F_s = A ∨ F_s = B ∨ F_s ≤ C) (hAImpossible : F_s = A → False) (hB : F_s = B → degree ≤ 6) (hLow : F_s ≤ C → degree ≤ 1) :

degree ≤ 6

Logical closure of the shared-tip F_s=A/B/≤C split after the reflection and metric/sign sublemmas have discharged their branches.

source

def LeanPool.Erdos132ConvexK3.WordClosureRealization {n : ℕ} (route : WordClosureRoute) (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) :

Prop

The four shared geometric realization predicates, indexed by closure route.

Equations

LeanPool.Erdos132ConvexK3.WordClosureRealization LeanPool.Erdos132ConvexK3.WordClosureRoute.terminalCage P d₁ d₂ d₃ = Nonempty (LeanPool.Erdos132ConvexK3.Row1B32WordRealization P d₁ d₂ d₃)
LeanPool.Erdos132ConvexK3.WordClosureRealization LeanPool.Erdos132ConvexK3.WordClosureRoute.antiSaturation P d₁ d₂ d₃ = Nonempty (LeanPool.Erdos132ConvexK3.OnePenultimateWordGeometry P d₁ d₂ d₃)
LeanPool.Erdos132ConvexK3.WordClosureRealization LeanPool.Erdos132ConvexK3.WordClosureRoute.fullTwoRung P d₁ d₂ d₃ = Nonempty (LeanPool.Erdos132ConvexK3.FullTwoRungGeometry P d₁ d₂ d₃)
LeanPool.Erdos132ConvexK3.WordClosureRealization LeanPool.Erdos132ConvexK3.WordClosureRoute.fourEdgeCage P d₁ d₂ d₃ = Nonempty (LeanPool.Erdos132ConvexK3.Row4DDWordRealization P d₁ d₂ d₃)

Instances For

source

def LeanPool.Erdos132ConvexK3.WordRealization {n : ℕ} (word : ExceptionalCoverWord) (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) :

Prop

A word is realized when the geometric predicate selected by its route is inhabited.

Equations

LeanPool.Erdos132ConvexK3.WordRealization word P d₁ d₂ d₃ = LeanPool.Erdos132ConvexK3.WordClosureRealization word.route P d₁ d₂ d₃

Instances For

source

theorem LeanPool.Erdos132ConvexK3.realization_degree_bound {n : ℕ} {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (route : WordClosureRoute) (hRealizes : WordClosureRealization route P d₁ d₂ d₃) :

∃ (v : Fin n), vertexDegree P d₁ d₂ d₃ v ≤ route.degreeBound

One transport theorem closes each of the four shared realization routes.

source

def LeanPool.Erdos132ConvexK3.RealizesGeom {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) (word : ExceptionalCoverWord) :

Prop

A tag is realized when its routed shared geometric predicate is inhabited.

Equations

LeanPool.Erdos132ConvexK3.RealizesGeom P d₁ d₂ d₃ word = LeanPool.Erdos132ConvexK3.WordRealization word P d₁ d₂ d₃

Instances For

source

structure LeanPool.Erdos132ConvexK3.DraftWordClosureInterface {n : ℕ} (degree : Fin n → ℕ) (Realizes : ExceptionalCoverWord → Prop) :

Prop

Route-indexed local closure interface. Realizes w supplies the local geometric data for the corresponding exceptional word.

fullTwoRung (w : ExceptionalCoverWord) : w.route = WordClosureRoute.fullTwoRung → Realizes w → ∃ (v : Fin n), degree v ≤ 6
antiSaturation (w : ExceptionalCoverWord) : w.route = WordClosureRoute.antiSaturation → Realizes w → ∃ (v : Fin n), degree v ≤ 5
terminalCage (w : ExceptionalCoverWord) : w.route = WordClosureRoute.terminalCage → Realizes w → ∃ (v : Fin n), degree v ≤ 6
fourEdgeCage (w : ExceptionalCoverWord) : w.route = WordClosureRoute.fourEdgeCage → Realizes w → ∃ (v : Fin n), degree v ≤ 6

Instances For

source

theorem LeanPool.Erdos132ConvexK3.concrete_word_closures {n : ℕ} (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) :

DraftWordClosureInterface (vertexDegree P d₁ d₂ d₃) (RealizesGeom P d₁ d₂ d₃)

All thirteen tags close unconditionally through the four shared geometric realization predicates.

source

def LeanPool.Erdos132ConvexK3.HasThirteenWordReduction {n : ℕ} (degree : Fin n → ℕ) (Realizes : ExceptionalCoverWord → Prop) :

Prop

Direct short-arc closure or one of the thirteen exceptional words.

Equations

LeanPool.Erdos132ConvexK3.HasThirteenWordReduction degree Realizes = ((∃ (v : Fin n), degree v ≤ 6) ∨ ∃ (w : LeanPool.Erdos132ConvexK3.ExceptionalCoverWord), Realizes w)

Instances For

source

theorem LeanPool.Erdos132ConvexK3.thirteen_word_assembly {n : ℕ} {degree : Fin n → ℕ} {Realizes : ExceptionalCoverWord → Prop} (hReduction : HasThirteenWordReduction degree Realizes) (hClosures : DraftWordClosureInterface degree Realizes) :

∃ (v : Fin n), degree v ≤ 6

Exact thirteen-word logical assembly. Every constructor is routed by ExceptionalCoverWord.route, with anti-saturation's stronger bound weakened from five to six only at the final interface.

source

def LeanPool.Erdos132ConvexK3.HasConvexK3DraftReduction {n : ℕ} [_nonzero : NeZero n] (P : Fin n → Point ℝ) (d₁ d₂ d₃ : ℝ) :

Prop

The proof-producing reduction package still required for an arbitrary convex configuration.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LeanPool.Erdos132ConvexK3.convex_top_three_min_degree_le_six_of_draft_reduction {n : ℕ} [_nonzero : NeZero n] {P : Fin n → Point ℝ} {d₁ d₂ d₃ : ℝ} (hReduction : HasConvexK3DraftReduction P d₁ d₂ d₃) :

∃ (v : Fin n), vertexDegree P d₁ d₂ d₃ v ≤ 6

A global reduction package and its thirteen kernel routes produce a vertex of degree at most six.

source

def LeanPool.Erdos132ConvexK3.ConvexTopThreeDegreeSixStatement :

Prop

The k = 3 degree-six statement suggested by the paper's p. 542 "perhaps degree at most 2k" question.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def LeanPool.Erdos132ConvexK3.ConvexTopThreeDraftReductionComplete :

Prop

Bridge from the two public geometric hypotheses to the complete draft reduction package.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem LeanPool.Erdos132ConvexK3.convex_top_three_degree_six_of_reduction_complete (hComplete : ConvexTopThreeDraftReductionComplete) :

ConvexTopThreeDegreeSixStatement

The named global bridge implies the convex degree-six statement.

source

theorem LeanPool.Erdos132ConvexK3.convex_k3_degree_six_of_reduction (hComplete : ConvexTopThreeDraftReductionComplete) :

ConvexTopThreeDegreeSixStatement

Abstract entry point from a complete reduction bridge to the convex degree-six statement.

Documentation

LeanPool.Erdos132ConvexK3.Assembly

Thirteen-word assembly #