IS-02: counterexample to the spectral-uniqueness locus condition

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

George Stepaniants

Complete exact order-four counterexample to the original spectral-uniqueness locus condition, independently reviewed and verified by the actual non-root Linux sandbox, Comparator, permitted-axiom audit and default kernel.

Claims

LEAN VERIFIED OP-00085 — Where a symmetric stochastic matrix can be spectrally unique

Disproof · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, IS-02/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-is-02-lean.tar.gz
Toolchain: leanprover/lean4:v4.33.1
Posted on GitHub: 13 September 2026

Verification PASSED

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

Declarations audited

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

NLA.IS02.not_targetNecessaryCondition

Not NLA.IS02.targetNecessaryCondition

RegistryProblems.Problem_OP_00085

Prop

Build log

RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision.
✔ [2639/2643] Built NLA.IS02.Definitions (6.3s)
⚠ [2640/2643] Built NLA.IS02.Proof (26s)
warning: NLA/IS02/Proof.lean:67:2: Unused tactic linter: `norm_num` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: NLA/IS02/Proof.lean:322:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:322:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:324:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:324:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:326:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:326:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:328:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:328:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:400:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:402:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:402:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:404:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:404:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:406:10: This simp argument is unused:
  Equiv.Perm.mul_apply

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.swap_apply_def]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:482:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:556:32: This simp argument is unused:
  Equiv.swap_apply_def

Hint: Omit it from the simp argument list.
  [apply] simp [Equiv.Perm.mul_apply]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:1308:24: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/IS02/Proof.lean:1322:58: This simp argument is unused:
  Matrix.cons_val_one

Hint: Omit it from the simp argument list.
  [apply] simp [counterexample, flatMatrix, Matrix.cons_val_zero, Matrix.cons_val_two, Matrix.cons_val_three] at e0 e2

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:1322:100: This simp argument is unused:
  Matrix.cons_val_three

Hint: Omit it from the simp argument list.
  [apply] simp [counterexample, flatMatrix, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two] at e0 e2

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:1345:58: This simp argument is unused:
  Matrix.cons_val_one

Hint: Omit it from the simp argument list.
  [apply] simp [counterexample, flatMatrix, Matrix.cons_val_zero, Matrix.cons_val_two, Matrix.cons_val_three] at e02

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/IS02/Proof.lean:1345:100: This simp argument is unused:
  Matrix.cons_val_three

Hint: Omit it from the simp argument list.
  [apply] simp [counterexample, flatMatrix, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two] at e02

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
ℹ [2641/2643] Built Solution (4.0s)
info: Solution.lean:57:0: 'NLA.IS02.counterexample_symmetric_nonnegative_stochastic' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:59:0: 'NLA.IS02.counterexample_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:61:0: 'NLA.IS02.counterexample_positive_trace' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:63:0: 'NLA.IS02.counterexample_spectrum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:65:0: 'NLA.IS02.sameSpectrum_iff_realEigenvalueMultiset_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:67:0: 'NLA.IS02.counterexample_spectral_uniqueness' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:69:0: 'NLA.IS02.counterexample_outside_locus' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:71:0: 'NLA.IS02.counterexample_claim' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:73:0: 'NLA.IS02.not_targetNecessaryCondition' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [2642/2643] Built RegistryRecord (3.9s)
Build completed successfully (2643 jobs).