← Mathematical handbook

Proposition 3(vii): TP2 and RR2 of the tent density

The necessity arguments use positive-length intervals, so isolated values on strip boundaries cannot repair a failed minor inequality.

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_ae_tp2_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (Verification.HasAEOrderedMinors 1 fun (u v : ↑unitInterval) => tentDensity b hb ![u, v]) ↔ b = 0 ∨ b = 1

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_ae_rr2_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (Verification.HasAEOrderedMinors (-1) fun (u v : ↑unitInterval) => tentDensity b hb ![u, v]) ↔ b = 0 ∨ b = -1

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_tp2_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : ProbabilityTheory.IsMTP2 (tentDensity b hb) ↔ b = 0 ∨ b = 1

theorem Papers.OrendayLaresRockel2026XiBeta.tentDensity_rr2_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (Verification.IsRR2 fun (u v : ↑unitInterval) => tentDensity b hb ![u, v]) ↔ b = 0 ∨ b = -1

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_density_version_ae_minors_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Measurable f) (hn : ∀ (x : Fin 2 → ↑unitInterval), 0 ≤ f x) (he : (leftBoundary b hb).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (f x)) (s : ℝ) : (Verification.HasAEOrderedMinors s fun (u v : ↑unitInterval) => f ![u, v]) ↔ Verification.HasAEOrderedMinors s fun (u v : ↑unitInterval) => tentDensity b hb ![u, v]

The classification is unchanged for any measurable nonnegative density version.

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_hasMTP2Density_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : (leftBoundary b hb).HasMTP2Density ↔ b = 0 ∨ b = 1

theorem Papers.OrendayLaresRockel2026XiBeta.leftBoundary_hasRR2Density_iff (b : ℝ) (hb : b ∈ Set.Icc (-1) 1) : Verification.HasRR2Density (leftBoundary b hb) ↔ b = 0 ∨ b = -1