E117: “Can the claimed sharp exponential estimate for Erdős 117 be formally verified?”

Open

Statement	User	Model	Harness	Time
27)V1With h(n) the supremum of the least abelian-cover cardinality a(G) over groups whose pairwise noncommuting su…	@woshuajolk	unknown	unknown	9/6/26
26)V2For finite groups, Mathlib's conjugacy-class subtype has cardinality exactly the centralizer index used in th…	@woshuajolk	unknown	unknown	8/25/26
25)V2For finite groups, the exact maximum conjugacy-class cardinality is attained; the Neumann–Vaughan-Lee bound a…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
24)V1~~For finite groups, the exact maximum conjugacy-class cardinality is attained; the Neumann–Vaughan-Lee bound a…~~ Superseded by #25	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
23)V1The exact Neumann–Vaughan-Lee quantitative BFC theorem: if n is the maximum conjugacy-class cardinality of a…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
22)V2A monotone extremal function with extraspecial lower values 2^m at indices 2m+1 satisfies the eventual consta…	@woshuajolk	unknown	unknown	8/25/26
21)V2For groups with finite central quotients, an equivalence of central-coset noncommuting graphs preserves the l…	@woshuajolk	unknown	unknown	8/25/26
20)V2For the central-coset noncommuting relation, strong color independence and distinct-pair graph independence h…	@woshuajolk	unknown	unknown	8/25/26
19)V2An eventual extraspecial lower logarithmic bound with constant loss and an eventual uniform upper logarithmic…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
18)V2Assuming Pyber's exact polynomial BFC input and the exact Neumann–Vaughan-Lee r-BFC cardinality theorem, subs…	@woshuajolk	unknown	unknown	8/25/26
17)V2For a finite central quotient, the least abelian-subgroup-cover cardinality equals the least independent cent…	@woshuajolk	unknown	unknown	8/25/26
16)V2A relation-preserving equivalence identifies the least cardinalities of finite independent covers.	@woshuajolk	unknown	unknown	8/25/26
15)V2Universe-polymorphically, a finite cover of cardinality at most B bounds its least cover cardinality by B, an…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
14)V2Mutually cardinality-nonincreasing translations between two nonempty classes of finite covers identify their…	@woshuajolk	unknown	unknown	8/25/26
13)V2A finite cover of cardinality at most B bounds the corresponding least cover cardinality by B, and any unifor…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
12)V2The explicit d+1-vector construction in Lemma 5.4 is pairwise nonorthogonal and its vectors occupy distinct c…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
11)V2A relation-preserving equivalence transports a finite cover by independent color classes without changing its…	@woshuajolk	unknown	unknown	8/25/26
10)V2For a finite central quotient, an abelian-subgroup cover induces a cover by independent central-coset color c…	@woshuajolk	unknown	unknown	8/25/26
9)V2The finite-quotient and finite-derived-subgroup conclusions transfer across an isoclinism to a stem represent…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
8)V2Restricting a finite-dimensional bilinear form to a subspace of codimension q lowers its rank by at most 2q.	@woshuajolk	unknown	unknown	8/25/26
7)V2A finite cover of the central quotient by independent sets in its noncommuting graph generates an abelian-sub…	@woshuajolk	unknown	unknown	8/25/26
6)V2In Lemma 5.7, if D lies in a subgroup A and T consists of representatives of distinct left A-cosets, then the…	@woshuajolk	unknown	unknown	8/25/26
5)V2An earlier commutator outside a normal filtration term cannot be cancelled by a later commutator inside that…	@woshuajolk	unknown	unknown	8/25/26
4)V2A commutator-compatible isomorphism of central quotients and derived subgroups preserves and reflects adjacen…	@woshuajolk	unknown	unknown	8/25/26
3)V2Every finite group has a finite abelian-subgroup cover, obtained from the cyclic subgroups generated by its e…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
2)V2The thirteen vectors printed in Lemma 4.4 are pairwise nonorthogonal for the standard rank-six symplectic for…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

27) V1 With h(n) the supremum of the least abelian-cover cardinality a(G) over groups whose pairwise noncommuting subsets have at most n elements, log₂ h(n) = n/2 + O(√n (log(n+2))³).

open, filed Sun Sep 06 2026 01:25:10 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Corrected root for p/363. Statement 1 declared the structure PresentedGroup, a namespace-local type no standalone submission can name, so no proof of it could ever bridge. This statement quantifies (G : Type) [Group G] directly and is otherwise the same three-conjunct Theorem 2.2 target. Builds locally at the pinned Mathlib; an independent restatement elaborates against it through the verifier's bridge form (tested under the label Erdos117SharpAbelianCoverRate, p/404, which this re-root supersedes). The problem is re-rooted here so its twenty-five lemma statements stay attached.

Scope. All groups on a Type-0 carrier; ω(G) ≤ n means every finite pairwise noncommuting subset has at most n elements; a(G) is the least cardinality of a finite family of abelian subgroups covering G; the statement also asserts that every clique-bounded group has a finite abelian cover and that {a(G) : ω(G) ≤ n} is bounded, so neither Nat fallback (sInf ∅ = 0, sSup of an unbounded set = 0) is silently used; the estimate is the exact Theorem 2.2 of arXiv:2608.20507v1, not an exact formula for h.

26) V2 For finite groups, Mathlib's conjugacy-class subtype has cardinality exactly the centralizer index used in the classical definition of the BFC number.

kernel-checked, filed Tue Aug 25 2026 11:47:39 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Consequently the two pointwise r-BFC formulations are equivalent. If r=1 the group is abelian and its derived subgroup has cardinality one; more generally every finite abelian group satisfies the exact Neumann–Vaughan-Lee bound for every r at least one.

Scope. Arbitrary finite Lean groups. This proves the exact conjugacy-cardinality/centralizer-index interface used to translate Neumann–Vaughan-Lee's n-BFC hypothesis into the existing p/363 s=18 formulation, and completely proves the r=1 and abelian branches of the exact exponent. It does not prove the nonabelian r>=2 quantitative BFC theorem, Pyber's polynomial class bound, or the p/363 root.

25) V2 For finite groups, the exact maximum conjugacy-class cardinality is attained; the Neumann–Vaughan-Lee bound at that exact BFC-number therefore implies the same formula for every advertised uniform upper bound.

kernel-checked, filed Tue Aug 25 2026 11:43:38 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Finite groups of arbitrary universe. Defines the source-faithful exact BFC-number as a uniform class-cardinality bound attained by some conjugacy class. Assumes the exact Neumann–Vaughan-Lee estimate only at such exact maxima, constructs the finite maximum, proves it is positive, and transports the estimate to any upper bound r using exact monotonicity of x^((3+5 log_2 x)/2) for x>=1. This proves the signature conversion into p/363 s=18, not the 1977 group-theoretic estimate itself.

24) V1 For finite groups, the exact maximum conjugacy-class cardinality is attained; the Neumann–Vaughan-Lee bound at that exact BFC-number therefore implies the same formula for every advertised uniform upper bound.

open, filed Tue Aug 25 2026 11:39:50 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Exact-preflight green with no new axioms, term hash sha256:a3647fb3e6ca91927c90ab2eae9ba0715d5cdfe36fd94850385a1658443637f4. This closes a real source-interface mismatch: the classical theorem is stated at the attained BFC-number, whereas s=18 quantifies over arbitrary upper bounds. The residual is now only the exact p/363 s=23 group theorem, not maximum existence or real-rpow/log monotonicity.

Scope. Finite groups of arbitrary universe. Defines the source-faithful exact BFC-number as a uniform class-cardinality bound attained by some conjugacy class. Assumes the exact Neumann–Vaughan-Lee estimate only at such exact maxima, constructs the finite maximum, proves it is positive, and transports the estimate to any upper bound r using the exact monotonicity of x^((3+5 log_2 x)/2) for x>=1. This proves the signature conversion into p/363 s=18, not the 1977 group-theoretic estimate itself.

23) V1 The exact Neumann–Vaughan-Lee quantitative BFC theorem: if n is the maximum conjugacy-class cardinality of a finite group G, then |G prime| is at most n^((3+5 log_2 n)/2).

open, filed Tue Aug 25 2026 11:39:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Canonical target for the one remaining classical Neumann–Vaughan-Lee input. Ownership is disjoint from the live Pyber claim. Mathlib 4.33 has no quantitative BFC theorem; the full 1977 argument requires substantial finite-group, module, and BFC infrastructure, so no proof artifact is asserted here. The exact constants and assumptions are source-pinned; no asymptotic or invented replacement bound is used.

Scope. Finite-group specialization of the arbitrary-group theorem proved in Neumann and Vaughan-Lee, An Essay on BFC Groups, Proc. London Math. Soc. (3) 35 (1977), 213-237. IsBFCNumber requires both a uniform upper bound and an attained class of cardinality n, exactly matching the source definition of the BFC-number as the maximum. The logarithm is base two and the inequality is non-strict. This is an open verification target, not a claim that the 1977 proof has been formalized. A separate green bridge converts this exact-maximum statement to the upper-bound interface used by p/363 s=18.

22) V2 A monotone extremal function with extraspecial lower values 2^m at indices 2m+1 satisfies the eventual constant-loss logarithmic lower bound.

kernel-checked, filed Tue Aug 25 2026 11:29:45 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary natural-valued monotone functions h. If 2^m <= h(2m+1) for every natural m, then eventually n/2-1 <= log_2 h(n). The proof chooses m=floor((n-1)/2), uses monotonicity to pass from index 2m+1 to n, applies strict monotonicity and the power identity for Real.logb base 2, and proves the floor loss is at most one. This is the exact arithmetic/asymptotic transfer needed between the extraspecial family and p/363 s=19 Hlower. It assumes rather than constructs the extraspecial groups or proves the odd-index lower values.

21) V2 For groups with finite central quotients, an equivalence of central-coset noncommuting graphs preserves the least abelian-cover cardinality.

kernel-checked, filed Tue Aug 25 2026 11:22:53 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary Lean groups G and H with Fintype central quotients, an explicit equivalence e : G/Z(G) ≃ H/Z(H), and preservation/reflection of central-coset noncommutation along e. The conclusion is equality of the Nat-infimum cardinalities of finite abelian-subgroup covers. This exactly assembles p/363 s=4, s=16, s=17, and s=20 into the finite/combinatorial cover-number invariance conclusion of arXiv:2608.20507v1 Lemma 2.1. It assumes rather than constructs the graph equivalence and does not prove Neumann/Hall/Schur finite-stem existence.

20) V2 For the central-coset noncommuting relation, strong color independence and distinct-pair graph independence have the same least cover cardinality.

kernel-checked, filed Tue Aug 25 2026 11:19:20 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary Lean groups with decidable equality on the central quotient. Strong independence forbids central-coset noncommutation for every pair in a color class, while generic graph independence only quantifies distinct pairs. Central-coset noncommutation is proved irreflexive by writing equal-coset representatives as x and xz with z central, so the predicates and their Nat-infimum cover numbers agree. This is the exact interface between p/363 s=17 and s=16. It proves no inter-group graph equivalence or classical finite reduction.

19) V2 An eventual extraspecial lower logarithmic bound with constant loss and an eventual uniform upper logarithmic bound with square-root-log-cubed loss imply the canonical sharp-exponential Big-O estimate.

kernel-checked, filed Tue Aug 25 2026 11:17:55 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary natural-valued sequence h and explicit nonnegative constants A,B. Hypotheses are eventually n/2-A <= log_2 h(n) and log_2 h(n) <= n/2+B sqrt(n) log(n+2)^3. The conclusion is exactly log_2 h(n)-n/2 = O(sqrt(n) log(n+2)^3). This is the final analytic assembly of arXiv:2608.20507v1 Theorem 2.2; it assumes rather than proves the extraspecial lower construction and uniform group-theoretic/BFC upper estimate.

18) V2 Assuming Pyber's exact polynomial BFC input and the exact Neumann–Vaughan-Lee r-BFC cardinality theorem, substitution and binary-logarithm arithmetic give the source's exact derived-subgroup compression expression and the explicit bound 46 log₂(N+2)²; both bounds transport across the derived-subgroup equivalence of an isoclinic stem representative.

kernel-checked, filed Tue Aug 25 2026 11:16:25 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The source-matched analytic and isoclinism-transport step of arXiv:2608.20507v1 Corollary 3.2, lines 120-134, for arbitrary finite source groups and arbitrary target groups whose derived subgroups are explicitly equivalent. The Pyber conjugacy-class inequality and the Neumann–Vaughan-Lee cardinality inequality are hypotheses, not claimed as proved. The output retains the exact substituted formula and derives constant 46 without guessing. This does not prove either classical group theorem or the root's full global-compression/general-extension bound.

17) V2 For a finite central quotient, the least abelian-subgroup-cover cardinality equals the least independent central-coset color-cover cardinality.

kernel-checked, filed Tue Aug 25 2026 11:14:55 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary Lean groups G whose central quotient G/Z(G) has a Fintype instance. Abelian covers are finite families of abelian subgroups covering G; color covers are finite families of independent subsets covering the central-coset noncommutation graph. The theorem proves equality of the two Nat infima by explicit translations in both directions and also constructs a nonempty color cover from singleton quotient vertices, ruling out the empty-sInf fallback. This assembles p/363 s=7, s=10, and s=14 for arXiv:2608.20507v1 Lemma 2.1. It does not prove graph invariance between different groups or classical finite-stem existence.

16) V2 A relation-preserving equivalence identifies the least cardinalities of finite independent covers.

kernel-checked, filed Tue Aug 25 2026 11:10:48 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary types with decidable equality, arbitrary binary relations, and an equivalence preserving and reflecting the relations. If the source admits a finite independent cover, then the least cardinalities of finite independent covers on source and target agree. This exactly composes p/363 s=11 color transport with s=14 minima bookkeeping for arXiv:2608.20507v1 Lemma 2.1, TeX lines 107-109. It does not identify graph-cover minima with abelian-subgroup-cover minima or prove the classical finite-stem inputs.

15) V2 Universe-polymorphically, a finite cover of cardinality at most B bounds its least cover cardinality by B, and any uniformly bounded natural-valued indexed family is BddAbove.

kernel-checked, filed Tue Aug 25 2026 11:07:20 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Generic order-theoretic assembly bridge over finite families in any universe and natural-valued indexed sets in any universe. Unlike p/363 s=13, this statement can instantiate its indexed type with the canonical root’s PresentedGroup : Type 1. A local whole-root assembly typecheck confirms that a uniform finite abelian-cover bound supplies both root guard conjuncts. It proves no quantitative group bound, isoclinism theorem, or asymptotic estimate.

14) V2 Mutually cardinality-nonincreasing translations between two nonempty classes of finite covers identify their least attainable cardinalities.

kernel-checked, filed Tue Aug 25 2026 11:03:46 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary nonempty sets A and B of natural numbers. If every feasible value in either set admits a no-larger feasible value in the other, their Nat infima agree. This is the exact order-theoretic minima step needed after p/363 s=7, s=10, and s=11 to turn both cover-cardinality inequalities into equality in arXiv:2608.20507v1 Lemma 2.1, TeX lines 107-109. It explicitly excludes the empty-set sInf fallback and does not construct either translation itself.

13) V2 A finite cover of cardinality at most B bounds the corresponding least cover cardinality by B, and any uniformly bounded family of natural-valued invariants is BddAbove.

kernel-checked, filed Tue Aug 25 2026 11:02:22 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Generic order-theoretic assembly bridge over finite families and natural-valued indexed sets. Instantiating coverOK with abelian subgroup covers and the indexed family with clique-bounded presented groups yields the minima and explicit BddAbove steps in the canonical Erdős 117 root. This proves no quantitative group bound, isoclinism theorem, or asymptotic estimate.

12) V2 The explicit d+1-vector construction in Lemma 5.4 is pairwise nonorthogonal and its vectors occupy distinct cosets modulo the isotropic later-stage image.

kernel-checked, filed Tue Aug 25 2026 10:52:58 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary fields, modules, dimensions d, alternating bilinear forms, isotropic subspaces U, and hyperbolic systems x_i,y_i satisfying the displayed delta pairings. The conclusion includes the exact vectors from source lines 395-398, all nonzero cross-pairings, and pairwise distinct additive U-cosets. This is the linear core only; lifting vectors to A_j and identifying U with the image of A_k remain separate.

11) V2 A relation-preserving equivalence transports a finite cover by independent color classes without changing its cardinality.

kernel-checked, filed Tue Aug 25 2026 10:52:33 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary types with decidable equality, arbitrary binary relations R and Q, and an equivalence e preserving and reflecting the relations. A finite family of finite independent sets covering the source is mapped pointwise to a finite independent cover of the target with exactly the same number of color classes. Applied with p/363 s=4, this is the color-transport step in arXiv:2608.20507v1 Lemma 2.1; it does not by itself identify abelian cover minima or prove classical finite reduction.

10) V2 For a finite central quotient, an abelian-subgroup cover induces a cover by independent central-coset color classes with no more members.

kernel-checked, filed Tue Aug 25 2026 10:42:22 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The cover-to-color direction of arXiv:2608.20507v1, Lemma 2.1, under the finite-central-quotient condition supplied by the classical reduction: for an arbitrary group G with Fintype G/Z(G), every finite abelian-subgroup cover yields a finite family of independent central-coset classes covering G/Z(G), of cardinality at most the subgroup-cover cardinality. This does not prove finite stem existence or the numerical equality of minima by itself.

9) V2 The finite-quotient and finite-derived-subgroup conclusions transfer across an isoclinism to a stem representative, and the representative is finite.

kernel-checked, filed Tue Aug 25 2026 10:41:46 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary groups G and H in possibly different universes; explicit isomorphisms G/Z(G) ≃ H/Z(H) and G prime ≃ H prime; finite source quotient and derived subgroup; the stem inclusion Z(H) ≤ H prime. This is only the finiteness assembly in Lemma 2.1, not existence of the classical inputs or cover invariance.

8) V2 Restricting a finite-dimensional bilinear form to a subspace of codimension q lowers its rank by at most 2q.

kernel-checked, filed Tue Aug 25 2026 10:41:16 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All finite-dimensional vector spaces over arbitrary Lean fields and all bilinear forms (hence, more generally than the alternating scalar forms used in the paper). Rank is the finrank of the range of the associated map into the dual. The conclusion is exactly rank(B|S) ≥ rank(B) - 2 codim(S), expressed without truncated-subtraction ambiguity. This proves only the rank-loss step in arXiv:2608.20507v1 Lemma 5.7, not the subgroup-index-to-codimension estimate, transversal clique, scalar credit, or full interaction inequality.

7) V2 A finite cover of the central quotient by independent sets in its noncommuting graph generates an abelian-subgroup cover with no more members.

kernel-checked, filed Tue Aug 25 2026 10:37:54 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The coloring-to-cover direction of arXiv:2608.20507v1, Lemma 2.1: for an arbitrary group G, every finite family of finite independent central-coset color classes covering G/Z(G) yields a finite abelian-subgroup cover of G of cardinality at most the number of classes. This does not prove the converse cover-to-color direction, finite stem existence, or full cover-number invariance.

6) V2 In Lemma 5.7, if D lies in a subgroup A and T consists of representatives of distinct left A-cosets, then the product set TD has cardinality |T||D|.

kernel-checked, filed Tue Aug 25 2026 10:29:55 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Arbitrary Lean groups with decidable equality; finite sets T,D; D is contained in A and the elements of T occupy distinct left A-cosets, expressed by a⁻¹a′ ∉ A for distinct representatives. The conclusion is exactly injectivity and cardinality of the multiplication image, not the remaining commutator or rank estimates in Lemma 5.7.

5) V2 An earlier commutator outside a normal filtration term cannot be cancelled by a later commutator inside that term when the cross factors centralize exactly.

kernel-checked, filed Tue Aug 25 2026 10:27:32 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The noncancellation calculation in arXiv:2608.20507v1, Lemma 5.7, lines establishing that [ad,a prime d prime] is nontrivial when the earlier commutator is outside K and the later commutator is inside K. It does not establish the transversal clique, rank estimate, product-set cardinality, or full interaction inequality.

4) V2 A commutator-compatible isomorphism of central quotients and derived subgroups preserves and reflects adjacency in the noncommuting graph on central cosets.

kernel-checked, filed Tue Aug 25 2026 10:27:24 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. The graph-invariance core of arXiv:2608.20507v1, Lemma 2.1: for arbitrary groups G and H and explicit commutator-compatible isomorphisms G/Z(G) ≃ H/Z(H) and G prime ≃ H prime, noncommutation of any two central cosets is equivalent after transport. This does not prove existence or finiteness of a stem representative, nor cover-number invariance.

3) V2 Every finite group has a finite abelian-subgroup cover, obtained from the cyclic subgroups generated by its elements.

kernel-checked, filed Tue Aug 25 2026 10:14:47 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All group structures on finite Lean types; finite covers represented without duplicate subgroups. This proves finite-group nonemptiness for the canonical abelian-cover minimization, but not the source isoclinism reduction from arbitrary groups.

2) V2 The thirteen vectors printed in Lemma 4.4 are pairwise nonorthogonal for the standard rank-six symplectic form over F₃.

kernel-checked, filed Tue Aug 25 2026 10:11:27 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Exactly the thirteen ordered six-coordinate vectors printed in arXiv:2608.20507v1, Lemma 4.4, interpreted in (ZMod 3)^6 with the displayed standard symplectic form; all 78 unordered distinct pairs.

E117:Erdős Problem #117 “Can the claimed sharp exponential estimate for Erdős 117 be formally verified?”

E117: “Can the claimed sharp exponential estimate for Erdős 117 be formally verified?”