Support of a two-point coordinate box

Abstract

An actual two-corner budget slab has positive support, strictly above the base at zero shape.

All logarithms are natural. The support theorem uses three coordinates with widths log(2), log(3), log(7). All budgets, heights and shape coordinates are arbitrary finite real numbers. The notation xi denotes the source shape; its minimum is zero exactly when some coordinate is zero, since every coordinate is nonnegative. The variance sum below is unaveraged.

Definition 1.1 (Distance to an actual pair).

$\forall S \in Set (α), \forall c \in α, \forall d \in α, pairDistance (S, c, d) = min (infDist (c, S), infDist (d, S))$

Formalization. D5/S3/ArithSums/TwoPointSlabSupport.pairDistance (✓ std3).

Source. Repository-derived.

Commentary.

Here alpha is any pseudometric space and S is any subset. Each infDist is the usual point-to-set infimum distance. For a nonempty compact S the minimum has the attained-distance meaning proved below.

Definition 1.2 (One actual endpoint in every coordinate).

$\forall c \in (ι \to α), \forall d \in (ι \to α), \forall x \in (ι \to α), (IsCorner (c, d, x)) ⟺ (\forall i \in ι, x_{i} \in {c_{i}, d_{i}})$

Formalization. D5/S3/ArithSums/TwoPointSlabSupport.IsCorner (✓ std3).

Source. Repository-derived.

Commentary.

The index type and coordinate type are arbitrary. Endpoint coincidence is allowed in this definition. Fractional coordinate mixtures are not corners.

Definition 1.3 (Two different included budget values).

$\forall c \in (ι \to R), \forall d \in (ι \to R), \forall M_{0} \in R, \forall M_{1} \in R, (WideSlab (c, d, M_{0}, M_{1})) ⟺ ((M_{0} < M_{1}) \land (\exists x \in (ι \to R), \exists y \in (ι \to R), (IsCorner (c, d, x)) \land (IsCorner (c, d, y)) \land (i \sum (x_{i}) \in [M_{0}, M_{1}]) \land (i \sum (y_{i}) \in [M_{0}, M_{1}]) \land (i \sum (x_{i}) \neq = i \sum (y_{i}))))$

Formalization. D5/S3/ArithSums/TwoPointSlabSupport.WideSlab (✓ std3).

Source. Repository-derived.

Commentary.

The index type iota is finite. A budget is the sum of all coordinates. Both slab endpoints are included. Two corner labels with the same budget do not meet this hypothesis: the actual budget values must differ.

Definition 1.4 (The exact ordered widths).

$h = (lo g 2, lo g 3, lo g 7)$

Formalization. D5/S3/ArithSums/TwoPointSlabSupport.logWidths (✓ std3).

Source. Repository-derived.

Commentary.

The vector h is indexed by Fin(3), in this displayed order. In particular, a=log(2)>0, and a is no larger than either other width.

Theorem 1.5 (The minimum is the genuine set distance).

$\forall S \in Set (α), \forall c \in α, \forall d \in α, ((IsCompact (S)) \land (S \neq = \emptyset)) ⟹ ((0 \leq pairDistance (S, c, d)) \land (\exists y \in S, \exists z \in {c, d}, pairDistance (S, c, d) = dist (y, z)) \land (\forall y \in S, \forall z \in {c, d}, pairDistance (S, c, d) \leq dist (y, z)))$

Proof. Machine-checked in Lean as D5/S3/ArithSums/TwoPointSlabSupport.pair_distance_spec (✓ std3). ∎

Source. Repository-derived.

Commentary.

In any pseudometric space, compactness and nonemptiness give a closest point of S to each endpoint. Choose the endpoint with the smaller infimum. The result is attained by an actual pair and bounds the distance of every actual pair from below. These properties identify the set-to-set minimum; a merely supplied nonnegative lower bound would not have this meaning.

Theorem 1.6 (The complete three-coordinate support theorem).

$\forall T \in R, \forall M_{0} \in R, \forall M_{1} \in R, \forall xi \in (Fin (3) \to R), let a = lo g 2, h = (lo g 2, lo g 3, lo g 7); let c_{i} = T + xi_{i}, d_{i} = c_{i} + h_{i}, A = 3 \cdot T + i \sum (xi_{i}); let I = [\frac{M _{0}}{3}, \frac{M _{1}}{3}], μ = \frac{M _{1}}{3}, δ_{i} = pairDistance (I, c_{i}, d_{i}); let V_{0} = i \sum (δ_{i}^{2}), ρ = \frac{V _{0}}{6}, L = μ - ρ, H = μ + 2 \cdot ρ; let o = ((e : (Fin (3) \to {0, 1})) \mapsto i \sum (e_{i} \cdot h_{i})); (a \leq T) \land (\forall i \in Fin (3), 0 \leq xi_{i}) \land (\exists i \in Fin (3), xi_{i} = 0) \land (WideSlab (c, d, M_{0}, M_{1})) ⟹ [(\forall x \in (Fin (3) \to R), (IsCorner (c, d, x)) ⟺ (\exists e \in (Fin (3) \to {0, 1}), x = (i \mapsto c_{i} + e_{i} \cdot h_{i}))) \land (\forall e \in (Fin (3) \to {0, 1}), i \sum (c_{i} + e_{i} \cdot h_{i}) = A + o (e)) \land (\forall i \in Fin (3), (0 \leq δ_{i}) \land (\exists y \in I, \exists z \in {c_{i}, d_{i}}, δ_{i} = dist (y, z)) \land (\forall y \in I, \forall z \in {c_{i}, d_{i}}, δ_{i} \leq dist (y, z))) \land (\forall x \in (Fin (3) \to R), ((IsCorner (c, d, x)) \land (i \sum (x_{i}) \in [M_{0}, M_{1}])) ⟹ (let m = \frac{\sum _{i} ( x _{i} )}{3}; (m \in I) \land (\forall i \in Fin (3), 0 \leq x_{i} - T) \land (V_{0} \leq i \sum ((x_{i} - m)^{2}) = i \sum ((x_{i} - T)^{2}) - 3 \cdot (m - T)^{2} \leq 6 \cdot (m - T)^{2}) \land (0 \leq ρ \leq m - T \leq μ - T))) \land H \geq L \geq T > 0 \land IsLeast (range (o), 0) \land IsLeast ({r ∣ (r \in range (o)) \land (0 < r)}, a) \land ((xi = 0) ⟹ (let u = M_{0} - 3 \cdot T; let v = M_{1} - 3 \cdot T; (a \leq v) \land (u < v) \land ((u \leq 0) ⟹ ((\forall i \in Fin (3), δ_{i} = 0) \land (ρ = 0) \land (L = T + \frac{v}{3}) \land (T < L))) \land ((0 < u) ⟹ ((\forall i \in Fin (3), δ_{i} \leq \frac{u}{3}) \land (ρ \leq \frac{u}{3 \cdot 2}) \land (L \geq T + \frac{v - \frac{u}{2}}{3} > T))) \land (0 < L - T \leq H - T)))]$

Proof. Machine-checked in Lean as D5/S3/ArithSums/TwoPointSlabSupport.wide_slab_support_237 (✓ std3). ∎

Source. Repository-derived.

Commentary.

In the displayed statement, all unqualified coordinate sums and coordinate quantifiers range over Fin(3). Bool choices are identified with bits zero and one. Thus e_i h_i means h_i for true and zero for false. The symbol o is the offset function, and its range consists of the actual corner offsets. IsLeast asserts membership as well as a lower bound: zero and a are both attained. The bracketed conclusions are a conjunction under the displayed hypotheses. Every included corner is quantified, not only the two witnessing the slab.

For an included corner, its mean lies in the scaled closed budget interval. The attained-distance comparison gives delta_i <= |x_i-m|. Squaring and summing proves the first variance inequality. With w_i=x_i-T>=0, the identity sum(w_i)=3(m-T) and the nonnegative cross terms in its square give sum(w_i^2)<=(sum(w_i))^2. Subtracting 3(m-T)^2 gives the factor six. The generic finite-index square-sum argument specializes to three coordinates.

Every nonzero bit offset includes at least one positive width, and each width is at least a. The all-false choice attains zero; choosing only the first coordinate attains a. In zero shape, two different included budget values therefore force v>=a. The strict slab order gives u<v.

If u<=0, the base T lies in the mean interval and every coordinate distance vanishes. If u>0, the left interval endpoint bounds every distance by u/3. Summing the three squared bounds yields rho<=u/(3 sqrt(2)). Since sqrt(2)>1 and v>u>0, the displayed intermediate lower bound is strictly greater than T. In either branch the offsets lambda=L-T and eta=H-T satisfy 0<lambda<=eta; lambda is an offset, not a dual price.

Negative lower budgets, arbitrary upper slack, corners at either closed endpoint, zero w coordinates and zero variance are included. No integer exponent, coordinate-width comparison c_i>=h_i, cutoff, small-shape or physical premise is imposed. The result supplies positive arguments for later arithmetic analytic estimates; it makes no quantum or RH assertion.

References

Truth anchor: D5/S3/ArithSums/TwoPointSlabSupport.IsCorner
Truth anchor: D5/S3/ArithSums/TwoPointSlabSupport.WideSlab
Truth anchor: D5/S3/ArithSums/TwoPointSlabSupport.logWidths
Truth anchor: D5/S3/ArithSums/TwoPointSlabSupport.pairDistance
Truth anchor: D5/S3/ArithSums/TwoPointSlabSupport.pair_distance_spec
Truth anchor: D5/S3/ArithSums/TwoPointSlabSupport.wide_slab_support_237

Keyboard shortcuts

trureturing — Discovering truth

Support of a two-point coordinate box

Abstract

References