structure OpenBox (n : ℕ) : Type

Definition 7.2 (Open box and volume): an open box in ℝ^n is specified by coordinate bounds a_i ≤ b_i, corresponding to the product set ∏ i, (a_i, b_i).

• lower : Fin n → ℝ
• upper : Fin n → ℝ
• lower_le_upper (i : Fin n) : self.lower i ≤ self.upper i

def OpenBox.toSet {n : ℕ} (B : OpenBox n) : Set (Fin n → ℝ)

The subset of ℝ^n represented by an open box.

Equations

• B.toSet = {x : Fin n → ℝ | ∀ (i : Fin n), x i ∈ Set.Ioo (B.lower i) (B.upper i)}

def OpenBox.volume {n : ℕ} (B : OpenBox n) : ℝ

The volume of an open box, defined as the product of side lengths.

Equations

• B.volume = ∏ i : Fin n, (B.upper i - B.lower i)

def IsCoveredByBoxes {n : ℕ} (Ω : Set (Fin n → ℝ)) {J : Type u_1} (B : J → OpenBox n) : Prop

Definition 7.3 (Covering by boxes): a family (B_j)_{j ∈ J} of boxes in ℝ^n covers Ω when Ω ⊆ ⋃ j, B_j.

Equations

• IsCoveredByBoxes Ω B = (Ω ⊆ ⋃ (j : J), (B j).toSet)

noncomputable def boxOuterMeasureCoverCost (d : ℕ) (Ω : Set (Fin d → ℝ)) : ENNReal

The raw cover-cost functional used to build boxOuterMeasure, normalized so that the empty set has cost 0.

Equations

• boxOuterMeasureCoverCost d Ω = if Ω = ∅ then 0 else sInf {r : ENNReal | ∃ (C : ℕ → OpenBox d), IsCoveredByBoxes Ω C ∧ r = ∑' (j : ℕ), ENNReal.ofReal (C j).volume}

theorem boxOuterMeasureCoverCost_empty (d : ℕ) : boxOuterMeasureCoverCost d ∅ = 0

The normalized cover-cost functional vanishes on the empty set.

theorem boxOuterMeasureCoverCost_eq_rawInf_of_nonempty {d : ℕ} {Ω : Set (Fin d → ℝ)} (hΩ : Ω.Nonempty) : boxOuterMeasureCoverCost d Ω = sInf {r : ENNReal | ∃ (C : ℕ → OpenBox d), IsCoveredByBoxes Ω C ∧ r = ∑' (j : ℕ), ENNReal.ofReal (C j).volume}

On nonempty sets, the normalized cover-cost agrees with the raw cover infimum.

noncomputable def boxOuterMeasure (d : ℕ) : MeasureTheory.OuterMeasure (Fin d → ℝ)

Definition 7.4 (Outer measure): for Ω ⊆ ℝ^d, boxOuterMeasure d Ω is the extended real infimum of ∑ j, vol(B_j) over all at-most-countable box covers (B_j) of Ω.

Equations

• boxOuterMeasure d = MeasureTheory.OuterMeasure.ofFunction (boxOuterMeasureCoverCost d) ⋯

theorem boxOuterMeasure_apply (d : ℕ) (Ω : Set (Fin d → ℝ)) : (boxOuterMeasure d) Ω = ⨅ (t : ℕ → Set (Fin d → ℝ)), ⨅ (_ : Ω ⊆ ⋃ (i : ℕ), t i), ∑' (n : ℕ), boxOuterMeasureCoverCost d (t n)

Defining infimum formula for boxOuterMeasure evaluated on a set Ω.

theorem helperForProposition_7_1_coverMonotone {d : ℕ} {Ω : Set (Fin d → ℝ)} (B : ℕ → OpenBox d) (hcover : IsCoveredByBoxes Ω B) : (boxOuterMeasure d) Ω ≤ (boxOuterMeasure d) (⋃ (j : ℕ), (B j).toSet)

Helper for Proposition 7.1: monotonicity of boxOuterMeasure under a box cover.

theorem helperForProposition_7_1_coverSubadditive {d : ℕ} (B : ℕ → OpenBox d) : (boxOuterMeasure d) (⋃ (j : ℕ), (B j).toSet) ≤ ∑' (j : ℕ), (boxOuterMeasure d) (B j).toSet

Helper for Proposition 7.1: countable subadditivity on a ℕ-indexed union of boxes.

theorem helperForProposition_7_1_openBoxVolume_eqMeasureVolume {d : ℕ} (B : OpenBox d) : MeasureTheory.volume B.toSet = ENNReal.ofReal B.volume

Helper for Proposition 7.1: identify OpenBox.volume with Lebesgue volume on B.toSet.

theorem helperForProposition_7_1_volume_le_boxOuterMeasureCoverCost {d : ℕ} (Ω : Set (Fin d → ℝ)) : MeasureTheory.volume Ω ≤ boxOuterMeasureCoverCost d Ω

The cover-cost dominates Lebesgue volume on all sets.

theorem helperForProposition_7_1_volume_le_boxOuterMeasure {d : ℕ} (Ω : Set (Fin d → ℝ)) : MeasureTheory.volume Ω ≤ (boxOuterMeasure d) Ω

Lebesgue volume is bounded above by boxOuterMeasure.

theorem helperForProposition_7_1_openBoxCoverVolumeLowerBound {d : ℕ} (B : OpenBox d) (C : ℕ → OpenBox d) (hcover : IsCoveredByBoxes B.toSet C) : ENNReal.ofReal B.volume ≤ ∑' (j : ℕ), ENNReal.ofReal (C j).volume

Helper for Proposition 7.1: any countable open-box cover of a box has total volume at least the covered box volume.

def helperForProposition_7_1_zeroVolumeOpenBox (d : ℕ) : OpenBox (d + 1)

Helper for Proposition 7.1: a canonical zero-volume open box in positive dimension.

Equations

• helperForProposition_7_1_zeroVolumeOpenBox d = { lower := fun (x : Fin (d + 1)) => 0, upper := fun (x : Fin (d + 1)) => 0, lower_le_upper := ⋯ }

theorem helperForProposition_7_1_zeroVolumeOpenBox_volume (d : ℕ) : (helperForProposition_7_1_zeroVolumeOpenBox d).volume = 0

Helper for Proposition 7.1: the canonical positive-dimensional zero box has volume 0.

theorem helperForProposition_7_1_openBoxOuterEqVolume (d : ℕ) (B : OpenBox (d + 1)) : (boxOuterMeasure (d + 1)) B.toSet = ENNReal.ofReal B.volume

Helper for Proposition 7.1: in positive dimension, each open box has outer measure equal to its box volume.

theorem helperForProposition_7_1_boxOuterMeasureCoverCost_zeroDim_eq_top_of_nonempty {Ω : Set (Fin 0 → ℝ)} (hΩ : Ω.Nonempty) : boxOuterMeasureCoverCost 0 Ω = ⊤

Any nonempty subset of ℝ^0 has infinite normalized cover-cost.

theorem helperForProposition_7_1_boxOuterMeasure_zero_univ_eq_top : (boxOuterMeasure 0) Set.univ = ⊤

Helper for Proposition 7.1: in dimension 0, the outer measure of univ is ⊤ for this box-cover model using ℕ-indexed covers.

theorem helperForProposition_7_1_tsumOuterEqTsumVolume_zeroDim (B : ℕ → OpenBox 0) : ∑' (j : ℕ), (boxOuterMeasure 0) (B j).toSet = ∑' (j : ℕ), ENNReal.ofReal (B j).volume

Helper for Proposition 7.1: the tsum identity ∑ m(B_j) = ∑ vol(B_j) in dimension 0.

theorem helperForProposition_7_1_tsumOuterEqTsumVolume {d : ℕ} (B : ℕ → OpenBox d) : ∑' (j : ℕ), (boxOuterMeasure d) (B j).toSet = ∑' (j : ℕ), ENNReal.ofReal (B j).volume

Helper for Proposition 7.1: rewrite the tsum of outer measures of covering boxes as the tsum of their volumes.

theorem helperForProposition_7_1_infimumBound {d : ℕ} (Ω : Set (Fin d → ℝ)) : (boxOuterMeasure d) Ω ≤ sInf {r : ENNReal | ∃ (C : ℕ → OpenBox d), IsCoveredByBoxes Ω C ∧ r = ∑' (j : ℕ), ENNReal.ofReal (C j).volume}

Helper for Proposition 7.1: boxOuterMeasure d Ω is bounded above by the defining infimum over countable box covers.

theorem proposition_7_1 (d : ℕ) (Ω : Set (Fin d → ℝ)) (B : ℕ → OpenBox d) : (IsCoveredByBoxes Ω B → (boxOuterMeasure d) Ω ≤ (boxOuterMeasure d) (⋃ (j : ℕ), (B j).toSet) ∧ (boxOuterMeasure d) (⋃ (j : ℕ), (B j).toSet) ≤ ∑' (j : ℕ), (boxOuterMeasure d) (B j).toSet ∧ ∑' (j : ℕ), (boxOuterMeasure d) (B j).toSet = ∑' (j : ℕ), ENNReal.ofReal (B j).volume) ∧ (boxOuterMeasure d) Ω ≤ sInf {r : ENNReal | ∃ (C : ℕ → OpenBox d), IsCoveredByBoxes Ω C ∧ r = ∑' (j : ℕ), ENNReal.ofReal (C j).volume}

Proposition 7.1: for a box cover of Ω indexed by ℕ (encoding an at most countable family), the associated outer measure satisfies m(Ω) ≤ m(⋃ j, B_j) ≤ ∑' j, m(B_j) = ∑' j, vol(B_j), and in particular m(Ω) is bounded by the infimum of all such covering sums.

theorem helperForLemma_7_1_rangeBounds {n : ℕ} (m : MeasureTheory.OuterMeasure (Fin n → ℝ)) (Ω : Set (Fin n → ℝ)) : 0 ≤ m Ω ∧ m Ω ≤ ⊤

Helper for Lemma 7.1: every outer-measure value lies between 0 and ⊤.

theorem helperForLemma_7_1_monotone {n : ℕ} (m : MeasureTheory.OuterMeasure (Fin n → ℝ)) {A B : Set (Fin n → ℝ)} (hAB : A ⊆ B) : m A ≤ m B

Helper for Lemma 7.1: outer measures are monotone under set inclusion.

theorem helperForLemma_7_1_finiteSubadditivity {n : ℕ} (m : MeasureTheory.OuterMeasure (Fin n → ℝ)) {J : Type u_1} (s : Finset J) (A : J → Set (Fin n → ℝ)) : m (⋃ j ∈ s, A j) ≤ ∑ j ∈ s, m (A j)

Helper for Lemma 7.1: finite subadditivity over a finite-indexed union.

theorem helperForLemma_7_1_countableSubadditivity {n : ℕ} (m : MeasureTheory.OuterMeasure (Fin n → ℝ)) {J : Type u_1} [Countable J] (A : J → Set (Fin n → ℝ)) : m (⋃ (j : J), A j) ≤ ∑' (j : J), m (A j)

Helper for Lemma 7.1: countable subadditivity over countable-indexed unions.

theorem helperForLemma_7_1_translationInvariant_passthrough {n : ℕ} (m : MeasureTheory.OuterMeasure (Fin n → ℝ)) : (∀ (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ), m ((fun (y : Fin n → ℝ) => x + y) '' Ω) = m Ω) → ∀ (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ), m ((fun (y : Fin n → ℝ) => x + y) '' Ω) = m Ω

Helper for Lemma 7.1: translation invariance implication is the identity map on that property.

theorem outerMeasure_properties (n : ℕ) (m : MeasureTheory.OuterMeasure (Fin n → ℝ)) : m ∅ = 0 ∧ (∀ (Ω : Set (Fin n → ℝ)), 0 ≤ m Ω ∧ m Ω ≤ ⊤) ∧ (∀ ⦃A B : Set (Fin n → ℝ)⦄, A ⊆ B → m A ≤ m B) ∧ (∀ {J : Type u_1} (s : Finset J) (A : J → Set (Fin n → ℝ)), m (⋃ j ∈ s, A j) ≤ ∑ j ∈ s, m (A j)) ∧ (∀ {J : Type u_2} [Countable J] (A : J → Set (Fin n → ℝ)), m (⋃ (j : J), A j) ≤ ∑' (j : J), m (A j)) ∧ ((∀ (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ), m ((fun (y : Fin n → ℝ) => x + y) '' Ω) = m Ω) → ∀ (Ω : Set (Fin n → ℝ)) (x : Fin n → ℝ), m ((fun (y : Fin n → ℝ) => x + y) '' Ω) = m Ω)

Lemma 7.1 (Properties of outer measure): for an outer measure m* on ℝ^n, (v) m*(∅)=0; (vi) for every Ω, 0 ≤ m*(Ω) ≤ +∞; (vii) monotonicity under inclusion; (viii) finite subadditivity over a finite family; (x) countable subadditivity over a countable family; and (xiii) if m* is translation invariant (m*(x + Ω) = m*(Ω)), then this translation-invariance property holds.

theorem helperForProposition_7_2_zeroDim_Icc_eq_univ (a b : Fin 0 → ℝ) : Set.Icc a b = Set.univ

Helper for Proposition 7.2: in dimension 0, every closed box is all of Set.univ.

theorem helperForProposition_7_2_zeroDim_Icc_measure_eq_top (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Icc a b) = ⊤

Helper for Proposition 7.2: in dimension 0, every closed box has box outer measure ⊤ in the current model.

theorem helperForProposition_7_2_zeroDim_rhs_eq_one (a b : Fin 0 → ℝ) : ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) = 1

Helper for Proposition 7.2: in dimension 0, the right-hand side product is 1.

theorem helperForProposition_7_2_zeroDim_canonical_payload : (∀ (i : Fin 0), i.elim0 ≤ i.elim0) ∧ (boxOuterMeasure 0) (Set.Icc Fin.elim0 Fin.elim0) = ⊤ ∧ ENNReal.ofReal (∏ i : Fin 0, (i.elim0 - i.elim0)) = 1

Helper for Proposition 7.2: the canonical zero-dimensional data a = b = Fin.elim0 has vacuous bounds, left side ⊤, and right side 1.

theorem helperForProposition_7_2_zeroDim_rhs_ne_top (a b : Fin 0 → ℝ) : ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ≠ ⊤

Helper for Proposition 7.2: in dimension 0, the right-hand-side product term is not ⊤.

theorem helperForProposition_7_2_zeroDim_vacuous_bounds (a b : Fin 0 → ℝ) (i : Fin 0) : a i ≤ b i

Helper for Proposition 7.2: in dimension 0, the coordinate-wise bounds hypothesis is vacuous.

theorem helperForProposition_7_2_zeroDim_top_ne_rhs (a b : Fin 0 → ℝ) : ⊤ ≠ ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: in dimension 0, ⊤ cannot equal the right-hand-side product term.

theorem helperForProposition_7_2_zeroDim_univ_measure_ne_one : (boxOuterMeasure 0) Set.univ ≠ 1

Helper for Proposition 7.2: in dimension 0, the outer measure of Set.univ is not 1 for the current model.

theorem helperForProposition_7_2_zeroDim_Icc_measure_ne_one (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Icc a b) ≠ 1

Helper for Proposition 7.2: in dimension 0, every closed box has outer measure different from 1 in the current model.

theorem helperForProposition_7_2_zeroDim_formula_false (a b : Fin 0 → ℝ) : (boxOuterMeasure 0) (Set.Icc a b) ≠ ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: the closed-box identity is false in dimension 0 for the current boxOuterMeasure model.

theorem helperForProposition_7_2_zeroDim_bounds_instance_false (a b : Fin 0 → ℝ) (_h : ∀ (i : Fin 0), a i ≤ b i) : (boxOuterMeasure 0) (Set.Icc a b) ≠ ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: even after adding the coordinate-wise bounds hypothesis, the dimension-0 closed-box identity remains false in the current model.

theorem helperForProposition_7_2_zeroDim_implication_shape_iff_false (a b : Fin 0 → ℝ) : (∀ (i : Fin 0), a i ≤ b i) → (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)) ↔ False

Helper for Proposition 7.2: in dimension 0, even the implication-shaped form (∀ i, a i ≤ b i) → m*(Icc a b) = ... is equivalent to False because the bounds premise is vacuous.

theorem helperForProposition_7_2_zeroDim_no_bounded_solution : ¬∃ (a : Fin 0 → ℝ) (b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) ∧ (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: in dimension 0, no bounded closed box can satisfy the claimed closed-box outer-measure identity in the current model.

theorem helperForProposition_7_2_zeroDim_instance_implies_false (a b : Fin 0 → ℝ) (_h : ∀ (i : Fin 0), a i ≤ b i) (hEq : (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : False

Helper for Proposition 7.2: any claimed closed-box formula instance in dimension 0 immediately yields False in the current model.

theorem helperForProposition_7_2_zeroDim_equality_implies_false (a b : Fin 0 → ℝ) (hEq : (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))) : False

Helper for Proposition 7.2: the dimension-0 closed-box equality is contradictory, even without using any bounds hypothesis.

theorem helperForProposition_7_2_zeroDim_counterexample : ∃ (a : Fin 0 → ℝ) (b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) ∧ (boxOuterMeasure 0) (Set.Icc a b) ≠ ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: there is an explicit n = 0 closed-box counterexample with vacuous coordinate-wise bounds.

theorem helperForProposition_7_2_exists_dimensionwise_counterexample : ∃ (n : ℕ) (a : Fin n → ℝ) (b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) ∧ (boxOuterMeasure n) (Set.Icc a b) ≠ ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Proposition 7.2: the universal closed-box identity has a concrete counterexample in the family of all dimensions (again witnessed at n = 0).

theorem helperForProposition_7_2_zeroDim_specialization_forces_top_eq_one (hEq : (boxOuterMeasure 0) (Set.Icc Fin.elim0 Fin.elim0) = ENNReal.ofReal (∏ i : Fin 0, (i.elim0 - i.elim0))) : ⊤ = 1

Helper for Proposition 7.2: the concrete n = 0 specialization of the target equality forces the impossible identity ⊤ = 1.

theorem helperForProposition_7_2_zeroDim_specialization_contradiction (hEq : (boxOuterMeasure 0) (Set.Icc Fin.elim0 Fin.elim0) = ENNReal.ofReal (∏ i : Fin 0, (i.elim0 - i.elim0))) : False

Helper for Proposition 7.2: the specific n = 0, a = b = Fin.elim0 specialization of the closed-box identity is contradictory in the current model.

theorem helperForProposition_7_2_zeroDim_family_false : ¬∀ (a b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) → (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: even when restricted to dimension 0, the closed-box formula cannot hold for all boxes in the current model.

theorem helperForProposition_7_2_zeroDim_family_explicitBounds_false : ¬∀ (a b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) → (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: in dimension 0, the family statement written with an explicit bounds argument (matching the target binder order) is also impossible.

theorem helperForProposition_7_2_universal_formula_false : ¬∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Proposition 7.2: the fully universal closed-box formula is inconsistent with the current zero-dimensional model.

theorem helperForProposition_7_2_universal_formula_implies_false (hAll : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: any universal proof object for the closed-box formula immediately yields a contradiction in the current model.

theorem helperForProposition_7_2_universalImplicationShape_isEmpty : IsEmpty (∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i)))

Helper for Proposition 7.2: the implication-shaped universal family has no inhabitant in the current model.

theorem helperForProposition_7_2_universalImplicationShape_iff_false : (∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) ↔ False

Helper for Proposition 7.2: equivalently, the implication-shaped universal family is logically False in the current model.

theorem helperForProposition_7_2_fixedDimension_family_forces_nonzero (n : ℕ) (hAtDim : ∀ (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : n ≠ 0

Helper for Proposition 7.2: if the closed-box formula holds for all boxes in a fixed dimension n, then necessarily n ≠ 0 in the current model.

theorem helperForProposition_7_2_targetShape_forces_zero_ne_zero (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : 0 ≠ 0

Helper for Proposition 7.2: any proof object of the target quantifier shape forces the impossible conclusion (0 : ℕ) ≠ 0 via the fixed-dimension obstruction at n = 0.

theorem helperForProposition_7_2_targetShape_zeroDim_specialization (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : (boxOuterMeasure 0) (Set.Icc Fin.elim0 Fin.elim0) = ENNReal.ofReal (∏ i : Fin 0, (i.elim0 - i.elim0))

Helper for Proposition 7.2: the exact quantifier shape of the target theorem still specializes to a contradiction in dimension 0.

theorem helperForProposition_7_2_targetShape_forces_top_eq_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : ⊤ = 1

Helper for Proposition 7.2: the target quantifier shape forces ⊤ = 1 by the dimension-0 specialization in the current model.

theorem helperForProposition_7_2_targetShape_forces_false_via_top_eq_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the target quantifier shape directly contradicts ENNReal.top_ne_one through the dimension-0 specialization.

theorem helperForProposition_7_2_targetShape_implies_false (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the exact quantifier shape of the target theorem still specializes to a contradiction in dimension 0.

theorem helperForProposition_7_2_targetShape_not_satisfiable : ¬∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Proposition 7.2: the target quantifier shape is not satisfiable in the current model because it implies the zero-dimensional contradiction.

theorem helperForProposition_7_2_targetShape_not_nonempty : ¬Nonempty (∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i)))

Helper for Proposition 7.2: the exact target quantifier shape has no inhabitant in the current model.

theorem helperForProposition_7_2_targetShape_isEmpty : IsEmpty (∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i)))

Helper for Proposition 7.2: equivalently, the target quantifier-shape type is empty in the current model.

theorem helperForProposition_7_2_targetShape_iff_false : (∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) ↔ False

Helper for Proposition 7.2: in the current model, the exact target quantifier shape is equivalent to False.

theorem helperForProposition_7_2_singleInstance_with_zero_dimension_contradiction {n : ℕ} {a b : Fin n → ℝ} (hn : n = 0) (hEq : (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: any single closed-box equality instance in a dimension identified with 0 is contradictory in the current model.

theorem helperForProposition_7_2_singleInstance_forces_positive_dimension {n : ℕ} {a b : Fin n → ℝ} (hEq : (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : ∃ (d : ℕ), n = d + 1

Helper for Proposition 7.2: any single closed-box equality instance in this model forces the ambient dimension to be positive.

theorem helperForProposition_7_2_singleInstance_forces_nonzero {n : ℕ} {a b : Fin n → ℝ} (hEq : (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : n ≠ 0

Helper for Proposition 7.2: any single closed-box equality instance in this model already forces the ambient dimension to be nonzero.

theorem helperForProposition_7_2_targetShape_forces_zero_eq_succ (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : ∃ (d : ℕ), 0 = d + 1

Helper for Proposition 7.2: the full target quantifier shape yields the impossible identity 0 = d + 1 for some natural d.

theorem helperForProposition_7_2_targetShape_forces_all_dimensions_nonzero (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) (n : ℕ) : n ≠ 0

Helper for Proposition 7.2: a proof object of the full target quantifier shape would force every natural number to be nonzero, by specializing at each dimension.

theorem helperForProposition_7_2_targetShape_forces_two_contradiction_routes (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : ⊤ = 1 ∧ 0 ≠ 0

Helper for Proposition 7.2: the target quantifier shape simultaneously forces two incompatible consequences (⊤ = 1 and 0 ≠ 0) under the current model.

theorem helperForProposition_7_2_targetShape_forces_zero_eq_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : 0 = 1

Helper for Proposition 7.2: the target quantifier shape is contradictory because 0 cannot be the successor of a natural number.

theorem helperForProposition_7_2_targetShape_forces_false_via_zero_eq_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the target quantifier shape implies False because it would force the absurd natural-number identity 0 = 1.

theorem helperForProposition_7_2_targetShape_forces_false_via_nat (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the target quantifier shape is contradictory because 0 cannot be the successor of a natural number.

theorem helperForProposition_7_2_targetShape_forces_all_dimensions_positive (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) (n : ℕ) : 0 < n

Helper for Proposition 7.2: any proof object of the full target quantifier shape forces every natural dimension to be strictly positive.

theorem helperForProposition_7_2_targetShape_forces_zero_lt_zero (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : 0 < 0

Helper for Proposition 7.2: the target quantifier shape forces the absurd strict inequality 0 < 0 by specialization at dimension 0.

theorem helperForProposition_7_2_targetShape_forces_false_via_lt_irrefl (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the target quantifier shape implies False because Nat.lt_irrefl 0 rules out the forced inequality 0 < 0.

theorem helperForProposition_7_2_targetShape_implies_zeroDim_family (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) (a b : Fin 0 → ℝ) (h : ∀ (i : Fin 0), a i ≤ b i) : (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i))

Helper for Proposition 7.2: a proof object of the exact target quantifier shape specializes to the explicit dimension-0 family statement with bounds as parameters.

theorem helperForProposition_7_2_targetShape_forces_false_via_zeroDim_family (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: reducing the exact target quantifier shape to the dimension-0 family immediately yields False in the current model.

theorem helperForProposition_7_2_zeroDim_canonical_equality_ne : (boxOuterMeasure 0) (Set.Icc Fin.elim0 Fin.elim0) ≠ ENNReal.ofReal (∏ i : Fin 0, (i.elim0 - i.elim0))

Helper for Proposition 7.2: the canonical dimension-0 closed-box equality is false in the current model.

theorem helperForProposition_7_2_targetShape_forces_false_via_canonical_zeroDim_ne (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: any inhabitant of the exact target quantifier shape contradicts the canonical dimension-0 inequality witness.

theorem helperForProposition_7_2_targetShape_forces_zeroDim_univ_measure_eq_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : (boxOuterMeasure 0) Set.univ = 1

Helper for Proposition 7.2: any inhabitant of the exact target quantifier shape forces boxOuterMeasure 0 Set.univ = 1 by specializing to a = b = Fin.elim0.

theorem helperForProposition_7_2_targetShape_forces_false_via_zeroDim_univ_eq_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the target quantifier shape implies False because its dimension-0 specialization forces boxOuterMeasure 0 Set.univ = 1, contradicting boxOuterMeasure 0 Set.univ = ⊤.

theorem helperForProposition_7_2_targetShape_forces_false_via_zeroDim_univ_ne_one (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: the target quantifier shape implies False because its dimension-0 specialization forces boxOuterMeasure 0 Set.univ = 1, contradicting the already established boxOuterMeasure 0 Set.univ ≠ 1.

theorem helperForProposition_7_2_zeroDim_family_isEmpty : IsEmpty (∀ (a b : Fin 0 → ℝ), (∀ (i : Fin 0), a i ≤ b i) → (boxOuterMeasure 0) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin 0, (b i - a i)))

Helper for Proposition 7.2: the full dimension-0 implication family is empty in the current model.

theorem helperForProposition_7_2_targetShape_forces_false_via_zeroDim_family_isEmpty (hTarget : ∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))) : False

Helper for Proposition 7.2: any inhabitant of the exact target quantifier shape yields an inhabitant of an empty dimension-0 family type, hence False.

theorem helperForProposition_7_2_targetShape_negated : ¬∀ (n : ℕ) (a b : Fin n → ℝ), (∀ (i : Fin n), a i ≤ b i) → (boxOuterMeasure n) (Set.Icc a b) = ENNReal.ofReal (∏ i : Fin n, (b i - a i))

Helper for Proposition 7.2: the full target quantifier shape is refuted in the current model, expressed directly as a negated proposition.

theorem helperForProposition_7_2_positiveDim_eq_succ {n : ℕ} (hn : 0 < n) : ∃ (d : ℕ), n = d + 1

Helper for Proposition 7.2: every positive natural number is a successor.

theorem helperForProposition_7_2_closedBox_volume_le_coverSum {d : ℕ} (a b : Fin (d + 1) → ℝ) (h : ∀ (i : Fin (d + 1)), a i ≤ b i) (C : ℕ → OpenBox (d + 1)) (hcover : IsCoveredByBoxes (Set.Icc a b) C) : ENNReal.ofReal (∏ i : Fin (d + 1), (b i - a i)) ≤ ∑' (j : ℕ), ENNReal.ofReal (C j).volume

Helper for Proposition 7.2: any countable open-box cover of a closed box has total covering volume at least the closed-box volume term.

theorem helperForProposition_7_2_closedBox_outer_ge_volume {d : ℕ} (a b : Fin (d + 1) → ℝ) (h : ∀ (i : Fin (d + 1)), a i ≤ b i) : ENNReal.ofReal (∏ i : Fin (d + 1), (b i - a i)) ≤ (boxOuterMeasure (d + 1)) (Set.Icc a b)

Helper for Proposition 7.2: the closed-box volume term is a lower bound for boxOuterMeasure in positive dimension.