Blueprint

🗺️ Map of Inversion height two in the free field of the free group: strict hierarchies and a non-membership criterion

🏷️ Associative rings · division rings 16K40 16S85 16S10 16S34 16E60
47 results ✅ 0 formalized in Lean ◐ 18 with a part in Lean 💻 22 checked by a program written proof only (a result can carry several tags)

Dependencies in the written proof: an arrow A → B means that this proof of B uses A. Every result rests on its written proof; the tags record what was checked besides, and each statement's “Evidence & scope” block says how far. The colour of a box is its strongest tag, in the order above; the tags in the box give the rest. Boxes with a thick border are the main results; click a box to read the statement.

cluster_0 Introduction cluster_1 Rings and notation cluster_2 The criterion cluster_3 Two evaluations cluster_4 The binomial hierarchy (Theorem B(i)) cluster_5 The size chain (Theorem B(ii)) cluster_6 The Dubrovin–Gräter–Hanke series (Theorem C) cluster_7 Remarks and open problems thm:A Theorem A the non-membership criterion: one atomic factor against the allowed denominators thm:B Theorem B the binomial hierarchy and the size chain are strict inside E₂ thm:C Theorem C every k[π] is a stopping step of the Dubrovin–Gräter–Hanke series lem:2.1 Lemma 2.1 atom criterion for monic pencils lem:5.7 Lemma 5.7 H_{n,p} and Q_r are atoms ◐ in Lean: only the eight conditions of (2) for Q₃ and Q₄ · 💻 program lem:2.1->lem:5.7 prop:5.8 Proposition 5.8 n axes: s_n⁻¹ ∉ 𝒰₁ 💻 program lem:2.1->prop:5.8 lem:6.2 Lemma 6.2 coranks on the quaternion curve; F̂_d is an atom ◐ in Lean: only the linear algebra of (c) · 💻 program lem:2.1->lem:6.2 lem:7.8 Lemma 7.8 F_ψ is an atom with six parts k+1 ◐ in Lean: only the integer data of the certificate of (a) · 💻 program lem:2.1->lem:7.8 rem:7.12 Remark 7.12 dependencies of Theorem 7.1 lem:2.1->rem:7.12 rem:8.4 Remark 8.4 strictness of the size chain over any fully atomic semifir lem:2.1->rem:8.4 lem:2.2 Lemma 2.2 the first strata of the series lem:3.1 Lemma 3.1 matrix localization: the atomic factors of H come from Σ rem:5.9 Remark 5.9 s_n⁻¹ ∉ Γ′_{n−2} lem:2.2->rem:5.9 lem:7.5 Lemma 7.5 the ring reached at k[π] 💻 program lem:2.2->lem:7.5 cor:7.10 Corollary 7.10 the size chain is strict inside 𝒰_r for every r ≥ 1 (witness q_d⁻¹); optimality; ⋃ 𝒟_k = 𝒰₂ ◐ in Lean: only the identities and the two evaluation points of (a); the identity used in (c) · 💻 program lem:2.2->cor:7.10 lem:2.2->rem:7.12 thm:3.4 Theorem 3.4 the criterion (Theorem A) ◐ in Lean: only with the conclusion of Lemma 3.1 as a hypothesis lem:7.9 Lemma 7.9 f_k is an atom; its one factor G_k not associated with y ◐ in Lean: only the two evaluation points of (c) (u and u² evaluate alike there) · 💻 program lem:3.1->lem:7.9 lem:3.1->rem:7.12 rem:8.1 Remark 8.1 characteristic p: the witness fails lem:3.1->rem:8.1 lem:3.1->rem:8.4 rem:8.5 Remark 8.5 independent adjunctions in [𝒰_∞, B₂] 💻 program lem:3.1->rem:8.5 rem:8.6 Remark 8.6 intermediate rings and classes of atoms lem:3.1->rem:8.6 lem:3.2 Lemma 3.2 the Smith counts ν_j do not grow on factors 💻 program def:3.3 Definition 3.3 monotone invariant lem:3.2->def:3.3 lem:3.5 Lemma 3.5 𝒰_r as U_Σ: one border per element ◐ in Lean: only the chain inverse · 💻 program lem:4.4 Lemma 4.4 the chain bound on the allowed borders lem:3.2->lem:4.4 lem:5.6 Lemma 5.6 the target profile of Q_r lem:3.2->lem:5.6 lem:3.6 Lemma 3.6 Γ′₂ as U_Σ: one lift per matrix def:3.3->rem:8.5 thm:5.1 Theorem 5.1 s⁻¹ lies in 𝒰₂ but not in 𝒰₁ ◐ in Lean: only the Woodbury reduction of §5.1 · 💻 program thm:3.4->thm:5.1 thm:5.2 Theorem 5.2 𝒰_{r−1} ⊊ 𝒰_r for every r (witness φ_r⁻¹) thm:3.4->thm:5.2 cor:5.3 Corollary 5.3 g_r⁻¹ ∈ 𝒰_{2r} ∖ 𝒰_r thm:3.4->cor:5.3 thm:3.4->rem:5.9 thm:6.1 Theorem 6.1 the size chain: ρ_d ∈ A_d ∩ E₂ but not in W_{d−1} ◐ in Lean: only the cycle inverse (6.1)–(6.2) · 💻 program thm:3.4->thm:6.1 thm:7.2 Theorem 7.2 ψ⁻¹ ∈ 𝒰₂ ∖ Γ′₂; 𝒰_∞ and Γ₂ are incomparable thm:3.4->thm:7.2 thm:7.3 Theorem 7.3 f_k⁻¹ ∉ Γ′_{k−2} for every k ≥ 4 thm:3.4->thm:7.3 thm:3.4->cor:7.10 rem:7.11 Remark 7.11 matrix size against number of binomial inverses ◐ in Lean: only the compression of (iii) thm:3.4->rem:7.11 thm:3.4->rem:7.12 thm:3.4->rem:8.1 rem:8.2 Remark 8.2 the two-parameter plane 𝒰_r ∩ Γ′_b ◐ in Lean: only the compressions of φ_r (identities) · 💻 program thm:3.4->rem:8.2 rem:8.3 Remark 8.3 later strata thm:3.4->rem:8.3 thm:3.4->rem:8.4 lem:3.5->thm:5.1 lem:3.5->cor:5.3 lem:3.5->thm:6.1 lem:3.5->rem:8.2 lem:4.1 Lemma 4.1 the exact arc: U_i² = tε·I ◐ in Lean: only trace, determinant and square (not the Smith parts) · 💻 program lem:3.6->rem:5.9 lem:3.6->thm:7.2 lem:3.6->thm:7.3 lem:4.2 Lemma 4.2 the scalar evaluation γ_k lem:4.1->lem:4.2 lem:4.3 Lemma 4.3 binomials on the arc: invertible, or parts (1,k) ◐ in Lean: only the trace of products of the N_j (core of (3)) · 💻 program lem:4.1->lem:4.3 lem:4.1->prop:5.8 lem:4.1->lem:7.8 lem:4.1->lem:7.9 lem:4.5 Lemma 4.5 no binomial degenerates on the quaternion curve ◐ in Lean: only the finite part (residues modulo 5) · 💻 program lem:4.2->thm:5.1 lem:4.2->cor:5.3 lem:4.2->rem:8.1 lem:4.3->lem:4.4 lem:4.3->prop:5.8 lem:4.3->rem:5.9 lem:7.7 Lemma 7.7 the bound 2a on the allowed lifts 💻 program lem:4.3->lem:7.7 lem:4.3->rem:7.12 lem:4.3->rem:8.1 lem:4.4->thm:5.1 lem:4.4->thm:5.2 lem:4.4->cor:5.3 rem:5.4 Remark 5.4 exact computations on the parabolic arc 💻 program lem:4.4->rem:5.4 lem:4.4->prop:5.8 lem:4.4->rem:5.9 lem:4.4->thm:7.2 lem:4.4->rem:7.12 lem:4.4->rem:8.1 lem:4.4->rem:8.2 lem:4.5->thm:6.1 lem:4.5->lem:6.2 lem:4.5->rem:8.1 thm:5.1->thm:5.2 thm:5.1->prop:5.8 thm:7.1 Theorem 7.1 every k[π] is a stopping step (Theorem C) 💻 program thm:5.1->thm:7.1 thm:5.1->thm:7.2 thm:5.1->cor:7.10 thm:5.1->rem:7.12 thm:5.1->rem:8.1 thm:5.1->rem:8.2 lem:5.5 Lemma 5.5 Q_r is associated with I ⊕ (−φ_r) 💻 program thm:5.2->rem:8.2 cor:5.3->rem:8.2 lem:5.5->thm:5.2 lem:5.6->thm:5.2 lem:5.6->rem:8.1 lem:5.6->rem:8.2 lem:5.7->thm:5.2 lem:5.7->cor:5.3 lem:5.7->prop:5.8 lem:5.7->rem:7.11 lem:5.7->rem:8.1 lem:5.7->rem:8.2 prop:5.8->rem:5.9 rem:6.4 Remark 6.4 the symmetric curve fails ◐ in Lean: only the commutator identity thm:6.1->thm:7.2 thm:6.1->rem:8.2 thm:6.1->rem:8.4 lem:6.2->thm:6.1 lem:6.2->rem:8.1 lem:6.2->rem:8.4 lem:6.2->rem:8.5 rem:6.3 Remark 6.3 a candidate second witness (not proved) ◐ in Lean: only the identities I + X_i + θX_{i+1} = N_i, N_i² = 0 lem:7.4 Lemma 7.4 compression at level k: f⁻¹ ∈ Γ′_{k−2} ◐ in Lean: only the inverse identities (fullness assumed) · 💻 program thm:7.1->rem:8.3 thm:7.2->thm:7.1 thm:7.2->rem:7.12 thm:7.3->thm:7.1 lem:7.6 Lemma 7.6 D′ ⊆ Γ₂ ◐ in Lean: only the inverse identities (fullness assumed) · 💻 program thm:7.3->cor:7.10 thm:7.3->rem:7.12 thm:7.3->rem:8.2 lem:7.4->lem:7.5 lem:7.4->lem:7.6 lem:7.4->cor:7.10 lem:7.4->rem:7.11 lem:7.4->rem:7.12 lem:7.4->rem:8.3 lem:7.5->thm:7.1 lem:7.5->cor:7.10 lem:7.5->rem:7.12 lem:7.6->thm:7.2 lem:7.7->thm:7.2 lem:7.7->thm:7.3 lem:7.7->rem:7.12 lem:7.8->thm:7.2 lem:7.8->lem:7.9 lem:7.8->rem:8.1 lem:7.9->thm:7.3 lem:7.9->cor:7.10 lem:7.9->rem:7.11 lem:7.9->rem:8.1 cor:7.10->rem:7.11 cor:7.10->rem:8.1 cor:7.10->rem:8.2 rem:7.11->rem:8.2

What the paper contributes

The free field D of A = ℂ[F3] is built in stages: E1 inverts the nonzero elements of A, E2 those of E1, and so on. The stages never stabilise (Reutenauer; Herbera–Sánchez). The paper works inside the single stage E2, where one restricts which elements are inverted.

  • A non-membership criterion (Theorem A = Theorem 3.4). If H−1 has its entries in the ring UΣ generated by the inverses of a family Σ of full matrices, each atomic factor of H is stably associated with an atomic factor of some Q ∈ Σ (Lemma 3.1). To refute that, it suffices that one atomic factor of H be more singular than every Q at some evaluation, measured by an invariant that does not grow on factors: Smith counts along an arc, the corank on a curve of integral quaternions, the corank at a character. The allowed denominators may themselves be singular there.
  • Two hierarchies inside E2, strict at every step (Theorem B). The rings 𝒰r generated by inverses of sums of products of at most r inverse binomials: 𝒰r−1 ⊊ 𝒰r, with witness (u−2+v−2+w−2)−1 for r = 2; their union is a proper subring of E2. The matrix-size chain Ad−1 ∩ E2 ⊊ Ad ∩ E2 for every d ≥ 2. The two hierarchies are independent, and the size chain is already strict inside 𝒰2 (Corollary 7.10).
  • Infinitely many stopping steps of the Dubrovin–Gräter–Hanke series inside E2 (Theorem C): for every k ≥ 3 the stratum of sums of k elements of Dπ, with explicit witnesses fk. That there are infinitely many stopping steps follows from Herbera–Sánchez, but no infinite family had been located within a fixed stage. The rings reached at these steps form a strict chain whose union is 𝒰2.

Main tools: Cohn's theory of firs, atoms and stable association, and of rational closures; Smith normal forms over ℂ[[t]] along an exact arc of 2×2 matrices; the free group generated by 1+2i, 1+2j, 1+2k; a grading argument that gives an atom for every k.

🚀 Start here: Theorem A: the non-membership criterion: one atomic factor against the allowed denominators.

Main results:

  • Theorem A: the non-membership criterion: one atomic factor against the allowed denominators
  • Theorem B: the binomial hierarchy and the size chain are strict inside E₂
  • Theorem C: every k[π] is a stopping step of the Dubrovin–Gräter–Hanke series

🧭 Fields: where the paper lives and what it connects

Tools taken from other branches

  • Theory of firs (Cohn) → complete factorization into atoms, stable association, torsion modules and rational closures — Lemma 2.1, Lemma 3.1, Theorem 3.4
  • Linear algebra over power series → Smith normal forms over ℂ[[t]] along an exact arc of 2×2 matrices — Lemma 3.2, Lemma 4.1, Lemma 4.4, Lemma 7.7
  • Arithmetic of quaternions → the free group generated by 1+2i, 1+2j, 1+2k (Lubotzky–Phillips–Sarnak), residues modulo 5 — Lemma 4.5, Theorem 6.1
  • Ordered groups → a grading argument and a bi-invariant order on the free group, to obtain an atom for every k — Lemma 7.9, Theorem 7.3
  • Formal verification → Lean 4 + Mathlib: the finite identities and certificates of the appendix — Lemma 4.1, Lemma 5.7, Lemma 7.8, Corollary 7.10, 8.2

What the results serve

  • Inversion height and complexity of rational expressions ← strict hierarchies of subrings inside one stage of the rational closure; stopping steps of the Dubrovin–Gräter–Hanke series — Theorem B, Theorem C
  • L²-invariants of groups ← the stages studied here are those of the division ring that carries the L²-invariants of F₃; the paper says nothing new about the Atiyah conjecture
  • Universal localization ← Malcolmson's chain A_b inside E₂, and already inside 𝒰₁ (Corollary 7.10(a)) — Theorem 6.1, Corollary 7.10