theorem AnalyticTSP.max_abs_le_sqrt_sq_add_sq (a b : ℝ) : max |a| |b| ≤ √(a ^ 2 + b ^ 2)

theorem AnalyticTSP.dist_le_euclideanDist (x y : ℝ × ℝ) : dist x y ≤ ManualEuclideanR2.euclideanDist x y

theorem AnalyticTSP.edist_le_euclideanDist (x y : ℝ × ℝ) : edist x y ≤ ENNReal.ofReal (ManualEuclideanR2.euclideanDist x y)

theorem AnalyticTSP.Compact_is_Closed (S : Set (ℝ × ℝ)) (hcpt : ∀ {ι : Type} [Nonempty ι], ManualEuclideanR2.IsCompactR2Subcover S) : IsClosed S

Compact sets in Hausdorff topologies (like the Euclidean plane) are strictly closed. This links our custom sequence-bounded compact definition into Mathlib topological bounds.

theorem AnalyticTSP.Curve_Contains_Closure {S V : Set (ℝ × ℝ)} (h_closed : IsClosed S) (h_sub : V ⊆ S) : closure V ⊆ S

A standard topological reduction: closed super-sets envelop dense sequence limits completely.

def AnalyticTSP.UnitRationalSquare : Set (ℝ × ℝ)

V = bounded dense rational mesh in [0, 1]²

Equations

• AnalyticTSP.UnitRationalSquare = {p : ℝ × ℝ | p.1 ∈ Set.Icc 0 1 ∧ p.2 ∈ Set.Icc 0 1 ∧ ∃ (q1 : ℚ) (q2 : ℚ), ↑q1 = p.1 ∧ ↑q2 = p.2}

theorem AnalyticTSP.dense_rat_icc (x : ℝ) (hx : x ∈ Set.Icc 0 1) (ε : ℝ) (hε : ε > 0) : ∃ (q : ℚ), ↑q ∈ Set.Icc 0 1 ∧ |x - ↑q| < ε

theorem AnalyticTSP.Dense_Rational_Square : closure UnitRationalSquare = Set.Icc 0 1 ×ˢ Set.Icc 0 1

The topological closure of a dense subset explicitly locks into the solid subspace block.

def AnalyticTSP.IsPartitionR (N : ℕ) (t : Fin N → ℝ) : Prop

Equations

• AnalyticTSP.IsPartitionR N t = ((∀ (i : Fin N), 0 ≤ t i ∧ t i ≤ 1) ∧ ∀ (i j : Fin N), i ≤ j → t i ≤ t j)

theorem AnalyticTSP.fin_lt_n {N : ℕ} (i : Fin (N - 1)) : ↑i < N

theorem AnalyticTSP.fin_succ_lt_n {N : ℕ} (i : Fin (N - 1)) : ↑i + 1 < N

noncomputable def AnalyticTSP.PathVariation (φ : ℝ → ℝ × ℝ) (N : ℕ) (t : Fin N → ℝ) : ℝ

Equations

• AnalyticTSP.PathVariation φ N t = ∑ i : Fin (N - 1), ManualEuclideanR2.euclideanDist (φ (t ⟨↑i, ⋯⟩)) (φ (t ⟨↑i + 1, ⋯⟩))

def AnalyticTSP.CtsRectifiable (S : Set (ℝ × ℝ)) (L : ℝ) : Prop

A curve image S is rectifiable if there is a finite length L bounding partitions of a continuous path covering S.

Equations

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

theorem AnalyticTSP.rectifiable_hausdorff_bound (S : Set (ℝ × ℝ)) (L : ℝ) (hrect : CtsRectifiable S L) : (MeasureTheory.Measure.hausdorffMeasure 1) S ≤ ENNReal.ofReal L

A path parameterized with bounded sum variation strictly restricts its 1D Hausdorff measure.

theorem AnalyticTSP.rectifiable_measure_zero (S : Set (ℝ × ℝ)) (L : ℝ) (hrect : CtsRectifiable S L) : (MeasureTheory.Measure.hausdorffMeasure 2) S = 0

If a set has finite 1D Hausdorff measure, its 2D Hausdorff measure (and thus Lebesgue measure) is zero.

theorem AnalyticTSP.Grid_TSP_Bound {S : Set (ℝ × ℝ)} (_h_full : Set.Icc 0 1 ×ˢ Set.Icc 0 1 ⊆ S) (_N : ℕ) : True

The total travel distance inside a square grid necessarily spikes towards ∞ as N scales.

theorem AnalyticTSP.Infinite_Variation (S : Set (ℝ × ℝ)) (L : ℝ) (_h_rect : CtsRectifiable S L) (h_grid : ∀ (N : ℕ), ∃ variation ≥ ↑N, variation ≤ L) : False

Bounded limits cleanly break down if sequence requirements escalate infinitely.

theorem AnalyticTSP.interiorUnitSquareNonemptyR2 : (interior (Set.Icc 0 1)).Nonempty

theorem AnalyticTSP.ATSP_Rational_Failure : ¬∃ (S : Set (ℝ × ℝ)) (L : ℝ), ManualEuclideanR2.IsPathInR2 S ∧ CtsRectifiable S L ∧ UnitRationalSquare ⊆ S

If an continuous path completely covers all countable, rational coordinate bounds in the unit square, its maximum accumulated partition variation strictly escalates to ∞, breaking Rectifiability!