BranchingVAS.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

14 declarations, 1 contain sorry, 0 declared as axioms

Decidability of reachability for branching vector addition systems

A branching vector addition system (BVAS) of dimension d is given by a finite list of axioms, a finite list of unary rules, and a finite list of binary rules, each of which is a vector in ℤ^d. A configuration is a vector in ℕ^d, which here is represented as a vector v ∈ ℤ^d subject to 0 ≤ v. The set of reachable configurations is defined inductively:

every axiom that is a valid configuration (i.e. lies in ℕ^d) is reachable;
if v is a reachable configuration, r is a unary rule and v + r ∈ ℕ^d, then v + r is reachable;
if v₁, v₂ are both reachable configurations, r is a binary rule and v₁ + v₂ + r ∈ ℕ^d, then v₁ + v₂ + r is reachable.

Modelling axioms as vectors in ℤ^d and only counting the non-negative ones as reachable yields the same set of reachable configurations as the usual definition in which axioms are required to lie in ℕ^d.

Branching vector addition systems are distinguished from ordinary vector addition systems (VAS) by allowing binary rules. VAS reachability is known to be decidable.

References:

The covering and boundedness problems for branching vector addition systems (Stéphane Demri, Marcin Jurdziński, Oded Lachish, Ranko Lazić, FSTTCS 2009) Gives a similar definition of BVAS, and compares it to related equivalent definitions.
On the Reachability Problem for Two-Dimensional Branching VASS by Clotilde Bizière, Thibault Hilaire, Jérôme Leroux, Grégoire Sutre, MFCS 2025, which settles the two-dimensional case and states that "the decidability status of the reachability problem for BVASS remains open in higher dimensions".
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants by Jérôme Leroux (2010), for the decidability of reachability for ordinary VAS.
Solving the Reachability Problem for Branching Vector Addition Systems via Semilinear Inductive Invariants by Clotilde Bizière, Jérôme Leroux, Grégoire Sutre (2026), a recent preprint claiming a positive resolution to the conjecture: reachability for branching vector addition systems is decidable.

Imports (1)

FormalConjecturesUtil

structure BranchingVAS.Bvas A branching vector addition system of dimension d line 65 source
Source documentation
A branching vector addition system of dimension d.

no axioms what this means
Statement uses: Nat
```
structure Bvas (d : ℕ) where
…
```

inductive BranchingVAS.Bvas.Reachable The reachable configurations of a branching vector addition system line 71 source

Source documentation

The reachable configurations of a branching vector addition system.

standard axioms: propext what this means

Statement uses: Nat, BranchingVAS.Bvas, Fin, Int

inductive Bvas.Reachable {d : ℕ} (b : Bvas d) : (Fin d → ℤ) → Prop
  | base {v : Fin d → ℤ} (hmem : v ∈ b.axioms) (hcfg : 0 ≤ v) : b.Reachable v
  | unary {v r w : Fin d → ℤ} (hv : b.Reachable v) (hr : r ∈ b.unaryRules)
      (hcfg : 0 ≤ w) (hw : w = v + r) : b.Reachable w
  | binary {v₁ v₂ r w : Fin d → ℤ} (hv₁ : b.Reachable v₁) (hv₂ : b.Reachable v₂)
      (hr : r ∈ b.binaryRules) (hcfg : 0 ≤ w) (hw : w = v₁ + v₂ + r) : b.Reachable w

/--
The vector in `ℤ^d` whose `i`-th coordinate is the `i`-th entry of the list `l`, or `0` if `l`
has fewer than `i + 1` entries. Used to encode the inputs of the reachability problem.
-/

Mentions: BranchingVAS.Bvas

def BranchingVAS.vecOfList The vector in ℤ^d whose i-th coordinate is the i-th entry of the list l, or 0 if l has fewer than i + 1 entries line 82 source
Source documentation
The vector in ℤ^d whose i-th coordinate is the i-th entry of the list l, or 0 if l has fewer than i + 1 entries. Used to encode the inputs of the reachability problem.

standard axioms: propext what this means
Statement uses: Nat, List, Int, Fin
Proof uses: List.getD, OfNat.ofNat
2 instances, coercions and auxiliary constants left out.
```
def vecOfList (d : ℕ) (l : List ℤ) : Fin d → ℤ := fun i => l.getD i 0
…
```
theorem BranchingVAS.vecOfList_ofFn line 85 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, Fin, Int, Eq, BranchingVAS.vecOfList, List.ofFn
Proof uses: funext, of_eq_true, Eq.trans, True, congrFun', congrArg, List.getD, OfNat.ofNat, Option.getD, GetElem?.getElem?, List, LT.lt, List.length, Option.some, List.getD_eq_getElem?_getD, Option, GetElem.getElem, List.length_ofFn, getElem?_pos, List.getElem_ofFn and 1 more
7 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem BranchingVAS.ofFn_vecOfList line 90 source
standard axioms: Quot.sound, propext what this means
Statement uses: Nat, List, Int, Eq, List.ofFn, BranchingVAS.vecOfList, List.map, List.getD, OfNat.ofNat, List.range
Proof uses: Eq.mpr, Fin, List.finRange, id, congrArg, List.ofFn_eq_map, Eq.symm, List.map_coe_finRange_eq_range, Function.comp, List.map_map, Eq.refl
3 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem BranchingVAS.primrec_ofFn_vecOfList line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Primrec₂, Nat, List, Int, List.ofFn, BranchingVAS.vecOfList
Proof uses: Primrec.of_eq, Prod, List.map, List.getD, Prod.snd, OfNat.ofNat, List.range, Prod.fst, Primrec.list_map, Primrec.comp, Primrec.list_range, Primrec.fst, Primrec₂.comp₂, Primrec.list_getD, Primrec.comp₂, Primrec.snd, Primrec₂.left, Primrec₂.right, Eq, Eq.symm and 1 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance BranchingVAS.(instance at line 106) line 106 source
Source documentation
An input of the reachability problem, that is, a dimension d, a branching vector addition system of dimension d and a target vector in ℤ^d, is encoded by d together with the lists of entries of the axioms, of the rules and of the target.
```
instance : Primcodable (Σ d : ℕ, Bvas d × (Fin d → ℤ)) :=
…
```
Mentions: BranchingVAS.Bvas
theorem BranchingVAS.reachability_decidable The reachability problem for branching vector addition systems is decidable sorry line 143 source
Source documentation
The reachability problem for branching vector addition systems is decidable.
That is, the predicate taking a dimension d, a branching vector addition system b of dimension d and a target vector t ∈ ℤ^d, and returning whether t is reachable in b, is a computable predicate. Note that the dimension is part of the input: a single algorithm must work for all dimensions.
As of August 2026, the solution is quite recently announced and is not yet peer-reviewed.

depends on sorry what this means
Statement uses: ComputablePred, Sigma, Nat, Prod, BranchingVAS.Bvas, Fin, Int, BranchingVAS.Bvas.Reachable, Sigma.fst, Prod.fst, Sigma.snd, Prod.snd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem reachability_decidable :
    ComputablePred fun p : Σ d : ℕ, Bvas d × (Fin d → ℤ) => p.2.1.Reachable p.2.2 := by
…
```
Mentions: BranchingVAS.Bvas
theorem BranchingVAS.reachable_of_mem_axioms Every axiom that is non-negative is reachable line 149 source
Source documentation
Every axiom that is non-negative is reachable.

standard axioms: propext what this means
Statement uses: Nat, BranchingVAS.Bvas, Fin, Int, Membership.mem, List, BranchingVAS.Bvas.axioms, LE.le, OfNat.ofNat, BranchingVAS.Bvas.Reachable
Proof uses: BranchingVAS.Bvas.Reachable.base
16 instances, coercions and auxiliary constants left out.
```
theorem reachable_of_mem_axioms {d : ℕ} (b : Bvas d) {v : Fin d → ℤ}
    (hmem : v ∈ b.axioms) (hcfg : 0 ≤ v) : b.Reachable v :=
…
```
Mentions: BranchingVAS.Bvas
theorem BranchingVAS.reachable_imp_pos Reachable vectors are always non-negative line 155 source
Source documentation
Reachable vectors are always non-negative.

standard axioms: propext what this means
Statement uses: Nat, Fin, Int, BranchingVAS.Bvas, BranchingVAS.Bvas.Reachable, LE.le, OfNat.ofNat
Proof uses: Eq, HEq, Membership.mem, List, BranchingVAS.Bvas.axioms, BranchingVAS.Bvas.Reachable.base, BranchingVAS.Bvas.unaryRules, HAdd.hAdd, BranchingVAS.Bvas.Reachable.unary, BranchingVAS.Bvas.binaryRules, BranchingVAS.Bvas.Reachable.binary, Eq.refl, HEq.refl
20 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem reachable_imp_pos {d : ℕ} (v : Fin d → ℤ) (b : Bvas d) :
    b.Reachable v → 0 ≤ v := by
…
```
Mentions: BranchingVAS.Bvas
def BranchingVAS.exampleBvas A small BVAS of dimension 3 used for a test below line 160 source
Source documentation
A small BVAS of dimension 3 used for a test below.

standard axioms: propext what this means
Statement uses: BranchingVAS.Bvas, OfNat.ofNat, Nat
Proof uses: BranchingVAS.Bvas.mk, List.cons, Fin, Int, Matrix.vecCons, Matrix.vecEmpty, List.nil, Neg.neg
4 instances, coercions and auxiliary constants left out.
```
def exampleBvas : Bvas 3 := {
…
```
Mentions: BranchingVAS.Bvas
def BranchingVAS.exampleBvas2 A small (indeed, degenerate, since it contains no binary rules) BVAS of dimension 2 used for a test below line 170 source
Source documentation
A small (indeed, degenerate, since it contains no binary rules) BVAS of dimension 2 used for a test below.

standard axioms: propext what this means
Statement uses: BranchingVAS.Bvas, OfNat.ofNat, Nat
Proof uses: BranchingVAS.Bvas.mk, List.cons, Fin, Int, Matrix.vecCons, Matrix.vecEmpty, List.nil, Neg.neg
4 instances, coercions and auxiliary constants left out.
```
def exampleBvas2 : Bvas 2 := {
…
```
Mentions: BranchingVAS.Bvas
theorem BranchingVAS.reachable_example The vector [0, 0, 12] is reachable in the first example BVAS line 180 source
Source documentation
The vector [0, 0, 12] is reachable in the first example BVAS.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: BranchingVAS.Bvas.Reachable, OfNat.ofNat, Nat, BranchingVAS.exampleBvas, Matrix.vecCons, Int, Matrix.vecEmpty
Proof uses: BranchingVAS.Bvas.Reachable.base, of_decide_eq_true, Membership.mem, Fin, List, BranchingVAS.Bvas.axioms, id, Eq, Bool, Decidable.decide, Bool.true, Eq.refl, List.Mem, List.finRange, HEq, Finset, Fintype.elems, Fintype.complete, LE.le, List.cons and 19 more
54 instances, coercions and auxiliary constants left out.

Tactic trace: 26 steps
Open to load the checked before-and-after goal states.
```
theorem reachable_example : exampleBvas.Reachable ![0,0,12] :=
…
```
theorem BranchingVAS.not_reachable_example The vector [0, 0] is not reachable in the second example BVAS line 202 source
Source documentation
The vector [0, 0] is not reachable in the second example BVAS.

standard axioms: propext what this means
Statement uses: Not, BranchingVAS.Bvas.Reachable, OfNat.ofNat, Nat, BranchingVAS.exampleBvas2, Matrix.vecCons, Int, Matrix.vecEmpty
Proof uses: False.elim, False, Eq.mp, Eq, HAdd.hAdd, Fin, Eq.trans, congrFun', congrArg, Matrix.cons_val_fin_one, Nat.succ, add_zero
17 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem not_reachable_example : ¬ exampleBvas2.Reachable ![0,0] := by
…
```