Scalar-height gluing synchronizes strictly monotone factor paths additively

Open

Hirsch.scalar_height_fiber_monotone_path_bound

by jjosh · Sep 8, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-geometrypolytopes

If each factor has a genuine edge path of L_i strictly decreasing in its affine height, with aligned endpoint heights, then the common-height fiber has an endpoint edge walk of at most 1 + sum_i (L_i - 1) steps. This is the class-wide obstruction proved mathematically in prove2me-work PR #11. For the Q28 six-edge monotone apex path it implies every independently scalar-glued/projectively skewed k-copy construction has apex distance at most 5k+1. This is an Open Lean formalization target, not a conjecture inferred from finite experiments.

Preamble

import Definitions.Def_Hirsch_scalar_fiber_model
set_option autoImplicit false
open scoped RealInnerProductSpace BigOperators

Formal statement

theorem Hirsch.scalar_height_fiber_monotone_path_bound :
    ∀ (k d : ℕ)
      (P : Fin k → Set (EuclideanSpace ℝ (Fin d)))
      (h : Fin k → EuclideanSpace ℝ (Fin d) →ᵃ[ℝ] ℝ)
      (L : Fin k → ℕ)
      (u v : Fin k → EuclideanSpace ℝ (Fin d)),
      (∀ i, Convex ℝ (P i)) →
      (∀ i, Hirsch.StrictHeightEdgeWalk (P i) (h i) (L i) (u i) (v i)) →
      (∀ i j, h i (u i) = h j (u j)) →
      (∀ i j, h i (v i) = h j (v j)) →
      Hirsch.EndpointWalkLE (Hirsch.ScalarHeightFiber P h)
        (1 + ∑ i, (L i - 1)) u v := by sorry

Source

Original mathematical argument developed in jjoshua2/prove2me-work PR #11 (2026-09-08); no literature-priority claim.

View graph