IV-03: full inverse-M interval vertex criterion

Recorded by the registry's curators from GitHub; the authors did not submit it here.

Sidney Holden

Complete all-dimensional inverse-M interval characterization by n-squared negative-sign vertices, implying the full original two-sign criterion without a regularity premise.

Claims

LEAN VERIFIED OP-00087 — Polynomial-size vertex test for inverse M-matrix intervals

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, IV-03/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-iv-03-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 16 September 2026

Verification PASSED

Attempt: 1
Toolchain: leanprover/lean4:v4.33.1
Auditor: v1 · modal
lake build: succeeded
Kernel replay: succeeded
Duration: 0:03:26.025378

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.IV03.twoSignCriterion	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched
RegistryProblems.Problem_OP_00087	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.IV03.twoSignCriterion

NLA.IV03.TwoSignCriterion

RegistryProblems.Problem_OP_00087

Prop

Build log

RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision.
✔ [8794/8808] Built NLA.IV03.Definitions (10s)
✔ [8795/8808] Built NLA.IV03.Proof (7.9s)
⚠ [8796/8808] Built NLA.IV03.Principal (16s)
warning: NLA/IV03/Principal.lean:31:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Principal.lean:32:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Principal.lean:33:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Principal.lean:111:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Principal.lean:112:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Principal.lean:113:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
⚠ [8797/8808] Built NLA.IV03.Vertices (17s)
warning: NLA/IV03/Vertices.lean:46:16: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
⚠ [8798/8808] Built NLA.IV03.Complementary (7.4s)
warning: NLA/IV03/Complementary.lean:28:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Complementary.lean:29:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Complementary.lean:30:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
⚠ [8799/8808] Built NLA.IV03.Adjugate (9.5s)
warning: NLA/IV03/Adjugate.lean:33:25: This simp argument is unused:
  Matrix.head_cons

Hint: Omit it from the simp argument list.
  [apply] simp only [Matrix.det_fin_two, Matrix.submatrix_apply, Matrix.cons_val_zero, Matrix.cons_val_one] at h₁ h₂ h₃

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
⚠ [8800/8808] Built NLA.IV03.Cofactor (7.2s)
warning: NLA/IV03/Cofactor.lean:29:2: Try this: 
  letI̵

The goal is a proposition, so `let` is preferred over `letI`.
The difference between `let` and `letI` is that `letI` inlines the value.
But this is not relevant for proofs because of proof irrelevance.

Note: This linter can be disabled with `set_option linter.style.haveILetI false`
warning: NLA/IV03/Cofactor.lean:24:67: This simp argument is unused:
  Pi.single_apply

Hint: Omit it from the simp argument list.
  [apply] simp [P', Q', Matrix.updateRow_apply, Matrix.fromBlocks]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IV03/Cofactor.lean:26:67: This simp argument is unused:
  Pi.single_apply

Hint: Omit it from the simp argument list.
  [apply] simp [P', Q', Matrix.updateRow_apply, Matrix.fromBlocks]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IV03/Cofactor.lean:28:57: This simp argument is unused:
  Pi.single_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Matrix.updateRow_apply, Matrix.fromBlocks]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
✔ [8801/8808] Built NLA.IV03.Monotonicity (6.7s)
✔ [8802/8808] Built NLA.IV03.IntervalStructure (6.4s)
✔ [8803/8808] Built NLA.IV03.SchurInterval (7.0s)
✔ [8804/8808] Built NLA.IV03.IntervalAdjugate (7.3s)
✔ [8805/8808] Built NLA.IV03.IntervalInduction (6.5s)
ℹ [8806/8808] Built Solution (7.1s)
info: Solution.lean:45:0: 'NLA.IV03.vertex_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:46:0: 'NLA.IV03.vertices_admissible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:47:0: 'NLA.IV03.nSquaredCriterion' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:48:0: 'NLA.IV03.twoSignCriterion' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [8807/8808] Built RegistryRecord (6.7s)
Build completed successfully (8808 jobs).