General_Operation_from_Binary_Operation

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Let $\left({S, \oplus}\right)$ be a magma. Then there a unique sequence $\left \langle {\oplus_k} \right \rangle_{k \mathop \ge 1}$ such that $(1): \quad \forall n \in \N_{>0}: \oplus_n$ is an $n$-ary operation on $S$ such that $(2): \quad \forall \left({a_1, \ldots, a_k}\right) \in S^k: \oplus_k \left({a_1, \ldots, a_k}\right) = \begin{cases} a: & k = 1 \\ \oplus_n \left({a_1, \ldots, a_n}\right) \oplus a_{n+1}: & k = n + 1 \end{cases}$ In particular, $\oplus_2$ is the same as the given binary operation $\oplus$. The $n$th term $\oplus_n$ of the sequence $\left \langle {\oplus} \right \rangle$ is called the '''$n$-ary operation defined by $\oplus$'''.

Why this node was retired

The posted statement is

theorem General_Operation_from_Binary_Operation {S : Type _} [Mul S] [Semigroup S] (a b c : S) : a * b * c = a * (b * c) := by sorry

The target replaces recursive finite-arity construction by associativity and supplies unrelated Mul and Semigroup structures.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Source-level repair: for any op:S→S→S there exists a unique family E_n:(Fin(n+1)→S)→S with E_0(x)=x_0 and E_{n+1}(x)=op(E_n(x restricted to first n+1 entries),x_{n+1}). No associativity or inhabitance is needed. If merely repairing the short associativity lemma, remove [Mul S] and keep one [Semigroup S], but that does not restore the source theorem.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.