IE-16: finite complex-spectrum counterexample to the normal-GMRES subset bound

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

George Stepaniants

Complete negative resolution of the original IE-16 universal inequality from Sidney Holden’s exact nine-point, degree-four counterexample. All fifteen independently reviewed contracts passed actual non-root Linux Comparator, standard axiom checks and default-kernel replay.

Claims

LEAN VERIFIED OP-00080 — A sharp subset bound for worst-case normal GMRES

Disproof · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, IE-16/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-ie-16-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:02:43.514983

Declarations audited

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

NLA.IE16.not_IE16Conjecture

Not NLA.IE16.IE16Conjecture

RegistryProblems.Problem_OP_00080

Prop

Build log

RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision.
⚠ [3128/3140] Replayed RegistryProblems.OP_00080
warning: RegistryProblems/OP_00080.lean:52:14: Variable name `L` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _L

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3129/3140] Built NLA.IE16.Definitions (6.7s)
warning: NLA/IE16/Definitions.lean:32:14: Variable name `L` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _L

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3130/3140] Built NLA.IE16.Minimax (12s)
warning: NLA/IE16/Minimax.lean:29:5: Variable name `hz` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hz

Note: This linter can be disabled with `set_option linter.unusedVariables false`
⚠ [3131/3140] Built NLA.IE16.WeightedDraft (11s)
warning: NLA/IE16/WeightedDraft.lean:26:5: Variable name `hS` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hS

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/IE16/WeightedDraft.lean:27:5: Variable name `hweights` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hweights

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/IE16/WeightedDraft.lean:122:16: Variable name `hp` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hp

Note: This linter can be disabled with `set_option linter.unusedVariables false`
✔ [3132/3140] Built NLA.IE16.SubsetBoundsDraft (10s)
⚠ [3133/3140] Built NLA.IE16.Numeric (61s)
warning: NLA/IE16/Numeric.lean:75:12: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/IE16/Numeric.lean:102:41: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/IE16/Numeric.lean:181:4: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/IE16/Numeric.lean:181:4: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
warning: NLA/IE16/Numeric.lean:245:4: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/IE16/Numeric.lean:245:4: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [3134/3140] Built NLA.IE16.WeightedBridgeDraft (12s)
warning: NLA/IE16/WeightedBridgeDraft.lean:25:5: Variable name `hweights` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hweights

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/IE16/WeightedBridgeDraft.lean:123:16: Variable name `hp` is not explicitly referenced.

Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning:
  [apply] _hp

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/IE16/WeightedBridgeDraft.lean:199:42: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/IE16/WeightedBridgeDraft.lean:199:42: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
⚠ [3135/3140] Built NLA.IE16.SubsetGeometryDraft (14s)
warning: NLA/IE16/SubsetGeometryDraft.lean:26:57: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/IE16/SubsetGeometryDraft.lean:27:14: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
✔ [3136/3140] Built NLA.IE16.FullMinimumDraft (4.2s)
✔ [3137/3140] Built NLA.IE16.FinalContractsDraft (4.2s)
ℹ [3138/3140] Built Solution (4.3s)
info: Solution.lean:57:0: 'NLA.IE16.explicitL_card' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:59:0: 'NLA.IE16.explicitL_admissible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:61:0: 'NLA.IE16.witness_feasible' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:63:0: 'NLA.IE16.witness_objective' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:65:0: 'NLA.IE16.full_minimum_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:67:0: 'NLA.IE16.full_minimum_isLeast' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:69:0: 'NLA.IE16.full_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:71:0: 'NLA.IE16.every_five_point_subset_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:73:0: 'NLA.IE16.every_five_point_subset_minimum_isLeast' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:75:0: 'NLA.IE16.subset_max_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:77:0: 'NLA.IE16.subset_max_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:79:0: 'NLA.IE16.ratio_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:81:0: 'NLA.IE16.ratio_exceeds_candidate' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:83:0: 'NLA.IE16.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:85:0: 'NLA.IE16.not_IE16Conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3139/3140] Built RegistryRecord (4.0s)
Build completed successfully (3140 jobs).