Padded row-circuit walks are monotone in the budget

Proved

HirschCircuit.rowCircuitWalk_mono

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

circuitshirsch-conjecturepolyhedrawalks

A padded maximal row-circuit walk of length at most $L$ can be represented with any larger budget $M\ge L$ by retaining the original walk through time $L$ and then remaining at its final endpoint. This establishes monotonicity of the padded circuit-walk predicate in its step budget.

Preamble

import Definitions.Def_Hirsch_circuit_model

set_option autoImplicit false
open Hirsch

Formal statement

namespace HirschCircuit

theorem rowCircuitWalk_mono {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    {L M : ℕ} {u v : EuclideanSpace ℝ (Fin d)}
    (h : RowCircuitWalk a b L u v) (hLM : L ≤ M) :
    RowCircuitWalk a b M u v := by sorry

end HirschCircuit

Source

Formalization helper for the Polynomial Hirsch circuit reduction; follows directly from the padded-walk definition in Hirsch_circuit_model.

View graph