RA-03: a counterexample to the randomized LU squared-error bound
Recorded by the registry's curators from GitHub; the authors did not submit it here.
George Stepaniants
Proves the genuine finite randomized LU process and its normalized history law, derives the actual singular-value tail and expected squared Frobenius error at an exact matrix witness, and refutes the full original universal bound.
Claims
Files and sources
- Paper
- OpenProblemsInNLA @ e375a6f, RA-03/lean/ ↗
- Lean bundle
- submissions/bundles/openproblemsinnla-ra-03-lean.tar.gz
- Toolchain
- leanprover/lean4:v4.33.1
- Posted on GitHub
- 12 September 2026
Verification PASSED
- Attempt
- 1
- Toolchain
- leanprover/lean4:v4.33.1
- Auditor
- v1 · modal
- lake build
- succeeded
- Kernel replay
- succeeded
- Duration
- 0:01:39.450379
Declarations audited
| Declaration | Kind | Axioms | Unused hypotheses | Canonical |
|---|---|---|---|---|
| NLA.RA03.not_squaredErrorConjecture | theorem · Prop | propext, Classical.choice, Quot.sound | none | matched |
| RegistryProblems.Problem_OP_00116 | definition | propext, Classical.choice, Quot.sound | none | no canonical statement |
NLA.RA03.not_squaredErrorConjecture
Not NLA.RA03.SquaredErrorConjecture
RegistryProblems.Problem_OP_00116
Prop
Build log
RegistryProblems: built against the registry's copy at 38ca23a44fc2b159a0c944d5c9af39a80eb601c2 rather than the pinned 545a5d18ad3917d52192c41ce172ec4b41945751. Statements are checked by content, not revision. ✔ [3731/3735] Built NLA.RA03.Definitions (7.2s) ℹ [3732/3735] Built NLA.RA03.Proof (8.8s) info: NLA/RA03/Proof.lean:235:0: 'NLA.RA03.frobeniusSq_eq_norm_sq_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:237:0: 'NLA.RA03.process_isProbability_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:239:0: 'NLA.RA03.witness_singularValue_zero' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:241:0: 'NLA.RA03.witness_singularValue_one' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:243:0: 'NLA.RA03.witness_expectedError' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:245:0: 'NLA.RA03.strict_scalar_gap' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:247:0: 'NLA.RA03.counterexample_proved' depends on axioms: [propext, Classical.choice, Quot.sound] info: NLA/RA03/Proof.lean:249:0: 'NLA.RA03.not_squaredErrorConjecture_proved' depends on axioms: [propext, Classical.choice, Quot.sound] ℹ [3733/3735] Built Solution (4.2s) info: Solution.lean:43:0: 'NLA.RA03.frobeniusSq_eq_norm_sq' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:45:0: 'NLA.RA03.process_isProbability' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:47:0: 'NLA.RA03.counterexample' depends on axioms: [propext, Classical.choice, Quot.sound] info: Solution.lean:49:0: 'NLA.RA03.not_squaredErrorConjecture' depends on axioms: [propext, Classical.choice, Quot.sound] ✔ [3734/3735] Built RegistryRecord (4.2s) Build completed successfully (3735 jobs).