RA-02: no polynomial trace-error factor after exactly the target rank of pivots

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

George Stepaniants

Complete negative answer to the original RPCholesky polynomial trace-factor question. For every real C>0 and p>=0, a complex positive-definite matrix of order r+1 strictly violates the proposed bound after exactly r pivots. All normalized process and genuine ordered eigenvalue-tail semantics are proved.

Claims

LEAN VERIFIED OP-00115 — Polynomial trace-error factor after exactly the target rank of pivots

Disproof · statement matched the canonical formalisation

Files and sources

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

Verification PASSED

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

Declarations audited

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

NLA.RA02.no_polynomial_trace_factor

Not NLA.RA02.PolynomialTraceFactor

RegistryProblems.Problem_OP_00115

Prop

Build log

info: NLA/RA02/HistoryIdentity.lean:38:0: 'NLA.RA02.distinct_history_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3710/3718] Built NLA.RA02.FutureEstimates (11s)
warning: NLA/RA02/FutureEstimates.lean:63:62: 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/RA02/FutureEstimates.lean:127:68: 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/RA02/FutureEstimates.lean:158:30: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/RA02/FutureEstimates.lean:158:30: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: NLA/RA02/FutureEstimates.lean:162:0: 'NLA.RA02.future_diagonal_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/FutureEstimates.lean:164:0: 'NLA.RA02.future_weighted_ratio_sum_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/FutureEstimates.lean:166:0: 'NLA.RA02.trace_budget_scalar_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3711/3718] Built NLA.RA02.RetainedTrace (5.0s)
info: NLA/RA02/RetainedTrace.lean:104:0: 'NLA.RA02.state_false_insert_trace_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/RetainedTrace.lean:106:0: 'NLA.RA02.retained_trace_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3712/3718] Built NLA.RA02.RetainedContribution (4.8s)
warning: NLA/RA02/RetainedContribution.lean:54:38: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/RA02/RetainedContribution.lean:54:38: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: NLA/RA02/RetainedContribution.lean:59:0: 'NLA.RA02.retained_prefix_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/RetainedContribution.lean:61:0: 'NLA.RA02.retained_contribution_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3713/3718] Built NLA.RA02.ExpectationLower (4.4s)
info: NLA/RA02/ExpectationLower.lean:43:0: 'NLA.RA02.expectation_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3714/3718] Built NLA.RA02.ExponentialComparison (4.6s)
warning: NLA/RA02/ExponentialComparison.lean:22:44: Variable name `hr` 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] _hr

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/RA02/ExponentialComparison.lean:41:65: 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/RA02/ExponentialComparison.lean:60:28: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/RA02/ExponentialComparison.lean:60:28: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: NLA/RA02/ExponentialComparison.lean:66:0: 'NLA.RA02.binomial_exponential_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/ExponentialComparison.lean:68:0: 'NLA.RA02.exponential_tail_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/ExponentialComparison.lean:70:0: 'NLA.RA02.exponential_dominates_real_power' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3715/3718] Built NLA.RA02.FinalCounterexample (4.5s)
info: NLA/RA02/FinalCounterexample.lean:37:0: 'NLA.RA02.universal_counterexamples' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/RA02/FinalCounterexample.lean:39:0: 'NLA.RA02.no_polynomial_trace_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3716/3718] Built Solution (4.4s)
info: Solution.lean:8:0: 'NLA.RA02.exp_one_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:10:0: 'NLA.RA02.scalar_parameters' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:12:0: 'NLA.RA02.pivot_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:14:0: 'NLA.RA02.finite_path_law' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:16:0: 'NLA.RA02.zero_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:18:0: 'NLA.RA02.expected_trace_recursion' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:20:0: 'NLA.RA02.ordered_spectrum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:22:0: 'NLA.RA02.least_eigenvalue_rayleigh' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:24:0: 'NLA.RA02.spectral_tail_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:26:0: 'NLA.RA02.arrowhead_quadratic' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:28:0: 'NLA.RA02.arrowhead_positive_definite' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:30:0: 'NLA.RA02.rayleigh_probe_values' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:32:0: 'NLA.RA02.arrowhead_tail' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:34:0: 'NLA.RA02.residual_state_positivity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:36:0: 'NLA.RA02.residual_state_updates' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:38:0: 'NLA.RA02.distinct_history_state' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:40:0: 'NLA.RA02.distinct_history_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:42:0: 'NLA.RA02.retained_history_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:44:0: 'NLA.RA02.retained_prefix_description' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:46:0: 'NLA.RA02.retained_trace_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:48:0: 'NLA.RA02.retained_contribution_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:50:0: 'NLA.RA02.expectation_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:52:0: 'NLA.RA02.binomial_exponential_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:54:0: 'NLA.RA02.exponential_tail_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:56:0: 'NLA.RA02.exponential_dominates_real_power' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:58:0: 'NLA.RA02.universal_counterexamples' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:60:0: 'NLA.RA02.no_polynomial_trace_factor' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3717/3718] Built RegistryRecord (4.2s)
Build completed successfully (3718 jobs).