Wang's Conjecture 5.3

Wang, arXiv:2509.18724v1, Conjecture 5.3, asks whether every finite commutative semigroup S and field K satisfying either the splitting condition or the characteristic-p / p-power-exponent condition obey

$$d(S,K)=\max_{a\in S}{\epsilon_a D_{\bar a}(S/\mathcal H) +d(\Gamma(H_a),K)}.$$

Here epsilon is zero exactly when the positive cyclic subsemigroup is a group with its own identity. The algebra is the ordinary semigroup algebra, the scalar quantifier is universal over individually nonzero scalars, D is the relative irreducible-length constant at the canonical quotient image, and Gamma consists of the actual stabilizer translation maps.

| Source clause | Lean counterpart | | --- | --- | | every finite commutative semigroup | S : Type, AddCommSemigroup S, Finite S in claim | | arbitrary field and both alternatives | Field K, Admissible S K | | ordinary basis and convolution | upstream AddMonoidAlgebra K S and its single | | positive cyclic semigroup and idempotent | positiveMultiple, cyclic, IsCyclicIdempotent, cyclicIdempotent | | period, exponent, splitting | period, semigroupExponent, Splitting | | group property in epsilon | CyclicIsGroup, epsilon | | every independently nonzero coefficient | GoodSequence quantifies all nonzero scalar functions of position | | supremum, including unboundedness | algebraicD : ENat, supremum over every finite list | | actual principal ideals and congruence quotient | Below, Green, greenCon and its upstream canonical quotient | | relative Davenport constant and empty subsequences | SequenceSum, IrreducibleAt, relativeD | | actual stabilizer translations, equality of maps | HClass, Gamma, composition addition | | maximum of the exact summands | rightSide, an ENat supremum over the finite carrier | | whole universal equality and its negation | claim : Prop, result : Not claim |

The source's infinite-length notation is interpreted as unbounded admissible finite lengths, without inventing an infinite product. For a general nonunital semigroup algebra only positive products are used; a bottom length zero does not affect the supremum. The empty sequence sums to an identity only if the semigroup already has one. The model lies in a monoid over Q, where the usual nonzero empty product is available. No zero-ring claim is needed for the field-valued conjecture.

The formula joins the two classes highlighted by the paper, Clifford and Archimedean semigroups. A finite product semigroup tests whether their local quotient and stabilizer information still predicts nonvanishing in the ordinary semigroup algebra.

Irreducibility of a quotient sequence does not force the corresponding algebraic factors to have a nonzero product for all nonzero scalars. In the witness, the quotient retains distinct labels while products of two transient factors lose the distinctions needed to prevent cancellation.

Use all six labels (b,n) in {0,1} x {0,1,2}, with maximum and addition truncated at two. Q meets splitting branch (i), since all cyclic periods and the exponent are one. Cyclic-idempotent existence for every finite semigroup is obtained from the upstream compact-semigroup theorem with the discrete topology; uniqueness follows from positive multiples.

A transient singleton has a coefficient that is always one. The all-ones assignment kills every product of length at least two, without a finite search cutoff. Hence d(S,Q)=1. Principal ideals distinguish the six labels. The quotient sequence [(0,1),(1,0)] is irreducible at (1,1) and gives relative D at least two. The cyclic semigroup of (1,1) has no identity, so epsilon is one. Therefore the source right side is at least two, which contradicts equality. No exact-right-side computation is claimed.

The claim uses the full finite-semigroup domain. Substituting one admissible monoid into that universal claim is a logical counterexample to it; it is not a conjecture restricted to monoids or to a bounded sequence length.

A contracted basis, coefficient choice shared by repeated positions, a monoid restriction in the universal claim, an identity-adjoined Gamma, incorrect cyclic periods, or a global Davenport constant substituted for the relative one invalidates this refutation. Every such distinction is kept in the source definitions. The numerical inequalities must follow from the actual algebra and quotient, not from supplied number placeholders.

Issue 23871 is the pre-probe Tier 1 named-problem admission basis. The externally named final result uses admission_basis: open-problem-resolution. Its proof contains the finite semigroup certificate, arbitrary-length algebraic annihilation, quotient irreducibility, and the separation of constants. Private helpers serve that live proof. The only public theorem is the designated literal result : Not claim, exempt from the four-slot audit. Definitions and instances introduce no additional public theorem audit.

The Library note gives source locators, source hashes, semantic conventions, the mathematical derivation, and the bounded literature status. Existing contracted-algebra refutations do not implement this question. The ordinary algebra and congruence infrastructure are reused from pinned Mathlib; no third-party code is transplanted. No independent mathematical novelty, minimality, Conjecture 3.26 settlement, freeze, CI, or publication follows from the local certificate alone.

Tier 1: Conjecture 5.3 is a published, named universal assertion. One admissible finite counterexample refutes the entire equality, counting as one question. The exact kernel theorem is the literal negation of the full finite-semigroup claim. Independent source/form approval, freezing, required CI and publication are separate obligations.

The bounded literature screen does not establish worldwide absence of an earlier settlement or independent novelty. The finite-length ENat convention does not assert an infinite product in an algebra without a topology. No statement is made about a general zero coefficient ring, minimal counterexamples, the exact proposed maximum, or Conjecture 3.26.