MF-18: full complex limiting Green-function rank equality

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

George Stepaniants

For every complex matrix dimension n≥1 under the original positivity, unique stabilizing family, nonsingular right-limit, regular-pencil and simple-unit-root assumptions, the Hermitian imaginary-part rank equals half the unit-circle root count.

Claims

LEAN VERIFIED OP-00095 — Imaginary-part rank in a limiting Green-function matrix equation

Full resolution · statement matched the canonical formalisation

Files and sources

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

Verification PASSED

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

Warnings

These never block publication — unused hypotheses have routine false positives — but they are the best mechanical signal of a mis-transcribed statement, so they are shown rather than hidden.

unused_hypothesis — The proof never uses: hunique. This is often legitimate, but an unused hypothesis in a headline theorem is the commonest sign of a mis-transcribed statement.
NLA.MF18.canonical_full_complex_rank

Declarations audited

Declaration	Kind	Axioms	Unused hypotheses	Canonical
NLA.MF18.canonical_full_complex_rank	theorem · Prop	propext, Classical.choice, Quot.sound	hunique	matched
RegistryProblems.Problem_OP_00095	definition	propext, Classical.choice, Quot.sound	none	no canonical statement

NLA.MF18.canonical_full_complex_rank

∀ {n : Nat} [NeZero n] (C D R P : NLA.MF18.Mat n) (X : Real → NLA.MF18.Mat n) (X₀ : NLA.MF18.Mat n) (m : Nat), NLA.MF18.GreenAssumptions C D R P X X₀ → (∀ (η : Real), Real.instLT.lt 0 η → ∀ (Y : NLA.MF18.Mat n), NLA.MF18.IsStabilizingSolution C D R P η Y → Eq Y (X η)) → Eq (NLA.MF18.circleRootCount (NLA.MF18.unregularizedPolynomial C R)) (instHMul.hMul 2 m) → Eq (Matrix.rank (NLA.MF18.hermitianImaginaryPart X₀)) m

RegistryProblems.Problem_OP_00095

Prop

Build log

.lean:160:0: 'NLA.MF18.reflected_zero_and_disk_count' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3720/3735] Built NLA.MF18.SteinRankLower (19s)
warning: NLA/MF18/SteinRankLower.lean:28:4: Try `simp at hlam` instead of `simpa using hlam`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
info: NLA/MF18/SteinRankLower.lean:105:0: 'NLA.MF18.stein_rank_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3721/3735] Built NLA.MF18.StableKernel (18s)
warning: NLA/MF18/StableKernel.lean:67:4: Try this: intro μ w hw
warning: NLA/MF18/StableKernel.lean:45:2: Try this: intro hlam v hv
info: NLA/MF18/StableKernel.lean:90:0: 'NLA.MF18.stable_space_in_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3722/3735] Built NLA.MF18.UnitPencilKernel (18s)
warning: NLA/MF18/UnitPencilKernel.lean:23:4: Try `simp at hlam` instead of `simpa using hlam`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: NLA/MF18/UnitPencilKernel.lean:34:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: NLA/MF18/UnitPencilKernel.lean:45:0: 'NLA.MF18.unit_pencil_left_pairing_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3723/3735] Built NLA.MF18.HalfPlaneHomotopy (18s)
info: NLA/MF18/HalfPlaneHomotopy.lean:41:0: 'NLA.MF18.monic_half_plane_count_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3724/3735] Built NLA.MF18.ReciprocalCount (18s)
info: NLA/MF18/ReciprocalCount.lean:85:0: 'NLA.MF18.reciprocal_count_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3725/3735] Built NLA.MF18.SimpleEigenfunctional (18s)
info: NLA/MF18/SimpleEigenfunctional.lean:69:0: 'NLA.MF18.simple_eigenfunctional_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3726/3735] Built NLA.MF18.DiskHomotopy (19s)
info: NLA/MF18/DiskHomotopy.lean:53:0: 'NLA.MF18.monicCayley_coeffContinuousOn' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF18/DiskHomotopy.lean:54:0: 'NLA.MF18.bounded_degree_disk_count_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3727/3735] Built NLA.MF18.SimpleUnitPairing (19s)
warning: NLA/MF18/SimpleUnitPairing.lean:74:4: Try `simp at hlam` instead of `simpa using hlam`

Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
warning: NLA/MF18/SimpleUnitPairing.lean:81:27: this tactic is never executed

Note: This linter can be disabled with `set_option linter.unreachableTactic false`
warning: NLA/MF18/SimpleUnitPairing.lean:81:27: Unused tactic linter: `ring` does nothing

Note: This linter can be disabled with `set_option linter.unusedTactic false`
info: NLA/MF18/SimpleUnitPairing.lean:94:0: 'NLA.MF18.simple_unit_root_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3728/3735] Built NLA.MF18.RegularizedCount (11s)
info: NLA/MF18/RegularizedCount.lean:112:0: 'NLA.MF18.homotopy_coeffContinuousOn' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF18/RegularizedCount.lean:113:0: 'NLA.MF18.homotopy_zero_disk_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF18/RegularizedCount.lean:114:0: 'NLA.MF18.regularized_root_count' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3729/3735] Built NLA.MF18.ComplementaryStability (11s)
warning: NLA/MF18/ComplementaryStability.lean:61:23: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice

Note: This linter can be disabled with `set_option linter.unnecessarySeqFocus false`
info: NLA/MF18/ComplementaryStability.lean:65:0: 'NLA.MF18.complementary_stability' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3730/3735] Built NLA.MF18.LimitingEquation (11s)
info: NLA/MF18/LimitingEquation.lean:71:0: 'NLA.MF18.limiting_equation_and_spectra' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3731/3735] Built NLA.MF18.SelectedCount (10s)
info: NLA/MF18/SelectedCount.lean:78:0: 'NLA.MF18.selected_spectrum_count' depends on axioms: [propext, Classical.choice, Quot.sound]
⚠ [3732/3735] Built NLA.MF18.CanonicalRank (11s)
warning: NLA/MF18/CanonicalRank.lean:73:5: Variable name `hunique` 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] _hunique

Note: This linter can be disabled with `set_option linter.unusedVariables false`
info: NLA/MF18/CanonicalRank.lean:79:0: 'NLA.MF18.full_complex_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
info: NLA/MF18/CanonicalRank.lean:80:0: 'NLA.MF18.canonical_full_complex_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
ℹ [3733/3735] Built Solution (10s)
info: Solution.lean:18:0: 'NLA.MF18.certified_half' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:20:0: 'NLA.MF18.stability_semantics' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:22:0: 'NLA.MF18.pencil_evaluation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:24:0: 'NLA.MF18.pencil_degree_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:26:0: 'NLA.MF18.positive_average_and_sign' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:28:0: 'NLA.MF18.homotopy_boundary_nonvanishing' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:30:0: 'NLA.MF18.cayley_degree_and_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:32:0: 'NLA.MF18.cayley_boundary_transfer' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:34:0: 'NLA.MF18.monic_half_plane_count_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:36:0: 'NLA.MF18.bounded_degree_disk_count_homotopy' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:38:0: 'NLA.MF18.regularized_root_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:40:0: 'NLA.MF18.solution_factorization' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:42:0: 'NLA.MF18.complementary_stability' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:44:0: 'NLA.MF18.closed_disk_stability_limit' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:46:0: 'NLA.MF18.limiting_equation_and_spectra' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:48:0: 'NLA.MF18.reciprocal_count_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:50:0: 'NLA.MF18.selected_spectrum_count' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:52:0: 'NLA.MF18.stein_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:54:0: 'NLA.MF18.simple_unit_root_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:56:0: 'NLA.MF18.generalized_stein_pairing' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:58:0: 'NLA.MF18.stable_space_dimension' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:60:0: 'NLA.MF18.stable_space_in_kernel' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:62:0: 'NLA.MF18.stein_rank_lower_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:64:0: 'NLA.MF18.full_complex_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Solution.lean:66:0: 'NLA.MF18.canonical_full_complex_rank' depends on axioms: [propext, Classical.choice, Quot.sound]
✔ [3734/3735] Built RegistryRecord (11s)
Build completed successfully (3735 jobs).