From functional rigidity to a facet

Abstract

Rigidity of vanishing functionals on saturating generators gives affine codimension one.

Theorem 1.1 (The exposed face has affine codimension one).

$$\forall E\in Type,[\mathrm{AddCommGroup}\left(E\right)][\mathrm{Module}\left(\mathbb{R},E\right)][\mathrm{FiniteDimensional}\left(\mathbb{R},E\right)]\forall s\in \mathrm{Set}\left(E\right),\forall I\in \mathrm{LinearMap}\left(\mathbb{R},E,\mathbb{R}\right),\forall n\in \mathrm{LinearMap}\left(\mathbb{R},E,\mathbb{R}\right),\forall b\in \mathbb{R},\forall o\in E,\forall t\in E,((\forall z\in E,(z\in s)\Rightarrow (b\le I\left(z\right)))\wedge ((\forall z\in E,(z\in s)\Rightarrow (n\left(z\right)=1))\wedge ((o\in s)\wedge ((I\left(o\right)=b)\wedge ((t\in s)\wedge ((I\left(t\right)\ne b)\wedge (\forall ell\in \mathrm{LinearMap}\left(\mathbb{R},E,\mathbb{R}\right),(\forall z\in E,(z\in s)\Rightarrow ((I\left(z\right)=b)\Rightarrow (\mathrm{ell}\left(z\right)=0)))\Rightarrow (\exists lam\in \mathbb{R},\forall z\in E,(z\in s)\Rightarrow (\mathrm{ell}\left(z\right)=lam\cdot (I\left(z\right)-b))))))))))\Rightarrow (\mathrm{Module}.\mathrm{finrank}\left(\mathbb{R},\mathrm{vectorSpan}\left(\mathbb{R},\{p:E\mid (p\in \mathrm{convexHull}\left(\mathbb{R},s\right))\wedge (I\left(p\right)=b)\}\right)\right)+1=\mathrm{Module}.\mathrm{finrank}\left(\mathbb{R},\mathrm{vectorSpan}\left(\mathbb{R},\mathrm{convexHull}\left(\mathbb{R},s\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/QuantumBounds/FacetRigidityBridge.rigidity_facet_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let s be any set in a finite-dimensional real module. The linear functional I is bounded below by b on s, and n normalises all its generators to one. The generator o attains the bound and t does not. If every linear functional vanishing on the saturating generators restricts to a scalar multiple of I−b on s, the exposed face of the convex hull has affine dimension one less than the hull. The notation vectorSpan is Mathlib’s direction space of the affine span, so finrank here is affine dimension. A convex combination reaches the bound only through active saturating generators. The annihilator of the face direction space is the annihilator of the hull direction space plus the line through I; t shows that this line adds exactly one dimension.

References

• Truth anchor: D5/S3/QuantumBounds/FacetRigidityBridge.rigidity_facet_bridge