MF-12: realizing every nonnegative polynomial growth exponent

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

George Stepaniants

Complete formally checked proof for every nonnegative real polynomial growth exponent using a fixed positive-dimensional real matrix pair, all words at every positive length, genuine Euclidean operator norm and the actual nth-root limit one.

Claims

LEAN VERIFIED OP-00093 — Realizing arbitrary polynomial growth exponents by finite matrix families

Full resolution · statement matched the canonical formalisation

Files and sources

Paper: OpenProblemsInNLA @ e375a6f, MF-12/lean/ ↗
Lean bundle: submissions/bundles/openproblemsinnla-mf-12-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:02:42.071806

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
RegistryProblems.Problem_OP_00093	definition	propext, Classical.choice, Quot.sound	none	no canonical statement
RegistryRecord.resolution	theorem · Prop	propext, Classical.choice, Quot.sound	none	matched

RegistryProblems.Problem_OP_00093

Prop

RegistryRecord.resolution

RegistryProblems.Problem_OP_00093

Build log

 Classical.choice, Quot.sound]
ℹ [3110/3123] Built NLA.MF12.Tensor (7.8s)
info: NLA/MF12/Tensor.lean:102:0: 'NLA.MF12.tensor_norm_comparison' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF12/Tensor.lean:103:0: 'NLA.MF12.tensor_word_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3111/3123] Built NLA.MF12.JordanEntries (9.7s)
warning: NLA/MF12/JordanEntries.lean:81:91: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
warning: NLA/MF12/JordanEntries.lean:96:2: Try `simp at he` instead of `simpa using he`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: NLA/MF12/JordanEntries.lean:114:6: try 'simp' instead of 'simpa'

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: NLA/MF12/JordanEntries.lean:119:47: Variable name `hn` 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] _hn

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: NLA/MF12/JordanEntries.lean:125:0: 'NLA.MF12.jordan_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF12/JordanEntries.lean:126:0: 'NLA.MF12.integer_family_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3112/3123] Built NLA.MF12.Budgets (8.0s)
info: NLA/MF12/Budgets.lean:108:0: 'NLA.MF12.telescoping_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF12/Budgets.lean:109:0: 'NLA.MF12.compressed_product_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3113/3123] Built NLA.MF12.Gaps (9.0s)
info: NLA/MF12/Gaps.lean:116:0: 'NLA.MF12.gap_decomposition' depends on axioms: [propext, Quot.sound]
info: NLA/MF12/Gaps.lean:117:0: 'NLA.MF12.reset_product_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF12/Gaps.lean:118:0: 'NLA.MF12.lower_word_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3114/3123] Built NLA.MF12.JordanBounds (10s)
info: NLA/MF12/JordanBounds.lean:115:0: 'NLA.MF12.jordan_growth_estimates' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3115/3123] Built NLA.MF12.HolderBound (9.1s)
info: NLA/MF12/HolderBound.lean:104:0: 'NLA.MF12.compressed_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3116/3123] Built NLA.MF12.GapBounds (11s)
info: NLA/MF12/GapBounds.lean:71:0: 'NLA.MF12.logarithmic_gap_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3117/3123] Built NLA.MF12.Upper (6.8s)
warning: NLA/MF12/Upper.lean:27:28: Variable name `hb` 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] _hb

Note: This linter can be disabled with `set_option linter.unusedVariables false`
warning: NLA/MF12/Upper.lean:181:53: This simp argument is unused:
  List.sum_singleton

Hint: Omit it from the simp argument list.
  [apply] simp only [List.sum_cons, List.sum_append, List.length_cons, List.length_append,
    List.length_singleton] at hlength

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
warning: NLA/MF12/Upper.lean:182:50: This simp argument is unused:
  List.length_singleton

Hint: Omit it from the simp argument list.
  [apply] simp only [List.sum_cons, List.sum_append, List.sum_singleton, List.length_cons,
    List.length_append] at hlength

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
info: NLA/MF12/Upper.lean:204:0: 'NLA.MF12.fractional_all_word_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3118/3123] Built NLA.MF12.Lower (5.7s)
info: NLA/MF12/Lower.lean:173:0: 'NLA.MF12.fractional_lower_all_lengths' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF12/Lower.lean:174:0: 'NLA.MF12.fractional_growth_estimates' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3119/3123] Built NLA.MF12.Lifted (4.3s)
info: NLA/MF12/Lifted.lean:126:0: 'NLA.MF12.fractional_tensor_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3120/3123] Built NLA.MF12.Realization (4.1s)
info: NLA/MF12/Realization.lean:74:0: 'NLA.MF12.realizes_every_nonnegative_exponent' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3121/3123] Built Solution (3.0s)
info: Solution.lean:18:0: 'NLA.MF12.family_growth_is_maximum' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:20:0: 'NLA.MF12.pair_word_norms' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:22:0: 'NLA.MF12.entry_maximum_norm_comparison' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:24:0: 'NLA.MF12.tensor_norm_comparison' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:26:0: 'NLA.MF12.tensor_word_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:28:0: 'NLA.MF12.fractional_parameters' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:30:0: 'NLA.MF12.fractional_projection' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:32:0: 'NLA.MF12.jordan_two_power' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:34:0: 'NLA.MF12.compressed_powers' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:36:0: 'NLA.MF12.loss_gain_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:38:0: 'NLA.MF12.telescoping_budget' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:40:0: 'NLA.MF12.compressed_product_formula' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:42:0: 'NLA.MF12.compressed_product_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:44:0: 'NLA.MF12.fractional_powers_entry_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:46:0: 'NLA.MF12.gap_decomposition' depends on axioms: [propext, Quot.sound]
info: Solution.lean:48:0: 'NLA.MF12.reset_product_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:50:0: 'NLA.MF12.fractional_all_word_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:52:0: 'NLA.MF12.logarithmic_gap_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:54:0: 'NLA.MF12.bernoulli_loss' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:56:0: 'NLA.MF12.lower_word_exact' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:58:0: 'NLA.MF12.fractional_lower_all_lengths' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:60:0: 'NLA.MF12.fractional_growth_estimates' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:62:0: 'NLA.MF12.roots_of_polynomial_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:64:0: 'NLA.MF12.jordan_entries' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:66:0: 'NLA.MF12.jordan_growth_estimates' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:68:0: 'NLA.MF12.integer_family_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:70:0: 'NLA.MF12.fractional_tensor_growth' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:72:0: 'NLA.MF12.realizes_every_nonnegative_exponent' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3122/3123] Built RegistryRecord (3.0s)
Build completed successfully (3123 jobs).