Unconstrained inverse-affine characterization and globally positive realization of source rank
ProvedHirsch.inverse_affine_source_rank_reductionFor finite real point sets S contained in C, a target v and distinct source x in S, and a fixed linear h strictly positive on z-v at every other point of C, define upper inverse heights from (1+D(z-v))/h(z-v) on S without v. Prove that adding a scalar multiple of h to D preserves their source-relative distinct upper count and can make 1+D(z-v) positive on all of C. For every denominator positive on S, its distinct ratio values below the source count equal the upper inverse-height count plus one. Derive an unconstrained affine-height minimizer attained by a denominator positive on all of C and optimal even against denominators required positive only on S. Pair-comparison directions of normalized non-target points are annihilated by h. The data are finite sets, not samples standing in for unseen vertices. This is a source-rank characterization, not a uniform polynomial route bound. The numerator is fixed and strict; the source is different from the target.
import Mathlib open scoped BigOperators set_option autoImplicit false
theorem Hirsch.inverse_affine_source_rank_reduction (d : ℕ) (C S : Finset (Fin d → ℝ))
(h : (Fin d → ℝ) →ₗ[ℝ] ℝ) (v x : Fin d → ℝ)
(hSC : S ⊆ C) (hv : v ∈ S) (hx : x ∈ S) (hxv : x ≠ v)
(hh : ∀ z ∈ C, z ≠ v → 0<h (z-v)) :
let U := fun D : (Fin d → ℝ) →ₗ[ℝ] ℝ =>
@Finset.filter ℝ (fun a => (1+D (x-v))/h (x-v)<a)
(fun _ => Classical.propDecidable _)
((S.erase v).image (fun z => (1+D (z-v))/h (z-v)))
let R := fun D : (Fin d → ℝ) →ₗ[ℝ] ℝ =>
@Finset.filter ℝ (fun a => a<h (x-v)/(1+D (x-v)))
(fun _ => Classical.propDecidable _)
(S.image (fun z => h (z-v)/(1+D (z-v))))
(∀ D : (Fin d → ℝ) →ₗ[ℝ] ℝ, ∃ c : ℝ,
(∀ z ∈ C, 0<1+(D+c • h) (z-v)) ∧ (U (D+c • h)).card=(U D).card) ∧
(∀ D : (Fin d → ℝ) →ₗ[ℝ] ℝ, (∀ z ∈ S, 0<1+D (z-v)) →
(R D).card=(U D).card+1) ∧
(∀ z ∈ C, z ≠ v → ∀ w ∈ C, w ≠ v →
h ((h (z-v))⁻¹ • (z-v)-(h (w-v))⁻¹ • (w-v))=0) ∧
∃ D : (Fin d → ℝ) →ₗ[ℝ] ℝ,
(∀ z ∈ C, 0<1+D (z-v)) ∧ (R D).card=(U D).card+1 ∧
(∀ E : (Fin d → ℝ) →ₗ[ℝ] ℝ, (U D).card ≤ (U E).card) ∧
(∀ E : (Fin d → ℝ) →ₗ[ℝ] ℝ, (∀ z ∈ S, 0<1+E (z-v)) →
(R D).card ≤ (R E).card) := by sorry