Volume identity at zero scale
OpenOAI.PiExponent.DeterminantContradiction.simplex_scale_zeronumber-theoryopenai-pi-exponent-017
At cutoff zero, the identity holds in every dimension: for k > 0 the set is the singleton zero vector and has zero volume; for k = 0 both sides equal 1. This isolates the singular scale that the invertible linear-map change-of-variables argument cannot handle. The proof route is to characterize the cutoff-zero set, use nullity of a singleton in positive-dimensional Euclidean space, and simplify separately in dimension zero.
Preamble
import Mathlib open scoped BigOperators
Formal statement
theorem OAI.PiExponent.DeterminantContradiction.simplex_scale_zero (k : ℕ) :
(MeasureTheory.volume
{x : Fin k → ℝ | (∀ i, 0 ≤ x i) ∧ ∑ i : Fin k, x i ≤ 0}).toReal =
(0 ^ k) * (MeasureTheory.volume
{x : Fin k → ℝ | (∀ i, 0 ≤ x i) ∧ ∑ i : Fin k, x i ≤ 1}).toReal := by sorrySource