Rejecting-order exponent for the family P_ε

Statements for the finite parts of paper Proposition 5.13 (prop:family): the passing construction below 1 + ½ ε^{-1/3}, the fan rejection at ⌊τ_-(ε)⌋ + 1, and incompatibility. Proofs are deferred.

Scope: the asymptotic liminf/limsup statement of Proposition 5.13 is not formalized, nor is the finiteness of t_min (which the paper quotes from the asymptotic completeness of the Navascués–Wolfe hierarchy). Only the explicit finite bounds are stated.

noncomputable def TriangleInflation.sigmaEps (ε : ℝ) : ℝ

σ = ½ ε^{2/3}, so that P_ε = Q(ε, 1 - σ) (paper Proposition 5.13).

Equations

• TriangleInflation.sigmaEps ε = ε ^ (2 / 3) / 2

noncomputable def TriangleInflation.mEps (ε : ℝ) : ℝ

m = ε + (1-ε)σ, the common one-variable zero marginal of P_ε.

Equations

• TriangleInflation.mEps ε = ε + (1 - ε) * TriangleInflation.sigmaEps ε

noncomputable def TriangleInflation.zEps (ε : ℝ) : ℝ

z = ε + (1-ε)σ³, the all-zero atom of P_ε.

Equations

• TriangleInflation.zEps ε = ε + (1 - ε) * TriangleInflation.sigmaEps ε ^ 3

noncomputable def TriangleInflation.tauMinus (ε : ℝ) : ℝ

τ_- = (z + m²/2 - √((z + m²/2)² - 2m³))/m², the smaller root of the quadratic v_t = t z - m - C(t,2) m² of paper Proposition 5.13.

Equations

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

Private auxiliaries

The estimates of paper Proposition 5.13 are written in terms of u = ε^{1/3}, for which σ = u²/2; splitting them off keeps each elaboration small.

The statements of Proposition 5.13

theorem TriangleInflation.Peps_eq (ε : ℝ) : Peps ε = Q ε (1 - sigmaEps ε)

P_ε is Q(ε, 1 - σ).

theorem TriangleInflation.mEps_eq_marg {ε : ℝ} : margA (Peps ε) = mEps ε ∧ margB (Peps ε) = mEps ε ∧ margC (Peps ε) = mEps ε

m is the common one-variable zero marginal of P_ε.

theorem TriangleInflation.zEps_eq_atom {ε : ℝ} : atom000 (Peps ε) = zEps ε

z is the all-zero atom of P_ε.

theorem TriangleInflation.Peps_aiFeasible {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / 8) (t : ℕ) (ht : 1 ≤ t) (hle : ↑t ≤ 1 + ε ^ (-1 / 3) / 2) : AIFeasible t (Peps ε)

Paper Proposition 5.13 (prop:family), lower bound, part (a): if 0 < ε < 1/8 and t ≤ 1 + ½ ε^{-1/3} then P_ε is feasible at order t. This is Theorem 5.1 applied with r = 1 - σ, using (1-ε)^{t-1} ≥ 1 - (t-1)ε ≥ 1 - σ.

theorem TriangleInflation.Peps_nwFeasible {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / 8) (t : ℕ) (ht : 1 ≤ t) (hle : ↑t ≤ 1 + ε ^ (-1 / 3) / 2) : NWFeasible t (Peps ε)

The Navascués–Wolfe form of the same lower bound.

theorem TriangleInflation.Peps_not_nwFeasible {ε : ℝ} (h0 : 0 < ε) (h1 : ε ≤ 1 / 64) : ¬NWFeasible (⌊tauMinus ε⌋₊ + 1) (Peps ε)

Paper Proposition 5.13 (prop:family), upper bound, part (b): if ε ≤ 1/64 then the first fan inequality rejects P_ε at order ⌊τ_-(ε)⌋ + 1.

theorem TriangleInflation.mEps_cube_lt_zEps_sq {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / 8) : mEps ε ^ 3 < zEps ε ^ 2

The numerical Finner obstruction for the family P_ε.

theorem TriangleInflation.Peps_not_compatible {ε : ℝ} (h0 : 0 < ε) (h1 : ε < 1 / 8) : ¬TriangleCompatible (Peps ε)

Paper Proposition 5.13 (prop:family), part (c): P_ε violates the Finner inequality, since m³ < ε² ≤ z² when ε < 1/8; hence P_ε ∉ C_tri.

theorem TriangleInflation.Peps_tminNW_bounds {ε : ℝ} (h0 : 0 < ε) (h1 : ε ≤ 1 / 64) : ⌊1 + ε ^ (-1 / 3) / 2⌋₊ + 1 ≤ tminNW (Peps ε) ∧ tminNW (Peps ε) ≤ ⌊tauMinus ε⌋₊ + 1

Paper Proposition 5.13 (prop:family), the finite sandwich on the first rejecting order of the Navascués–Wolfe hierarchy.

theorem TriangleInflation.Peps_tminAI_bounds {ε : ℝ} (h0 : 0 < ε) (h1 : ε ≤ 1 / 64) : ⌊1 + ε ^ (-1 / 3) / 2⌋₊ + 1 ≤ tminAI (Peps ε) ∧ tminAI (Peps ε) ≤ ⌊tauMinus ε⌋₊ + 1

The same sandwich for the ancestral-independence hierarchy.