Multiplicative-Exclusion Residue Class

Abstract

The candidate-inclusive multiplicative-exclusion sequence is uniquely defined and equals 1, 3, then the arithmetic progression 3n-5.

OEIS A026488, contributed by Clark Kimberling and corrected on 2019-10-12, states this formula as a conjecture. Sean A. Irvine reported verification through n=1300. The repository proof below is symbolic and unbounded.

The rule is stated with the atom’s integer subtraction a(i)a(j) − a(k); Theorem literal_exclusion_iff_additive records the subtraction-free form used in the proofs. At prospective index n, a’(r) is x when r=n and is the prior sequence value a(r) otherwise. Thus k=n, including the self-witness 2+2=2*2, is retained literally.

Definition 1.1 (Literal witness set).

$S = {3} \cup {3 t + 1 ∣ t \in N} .$

Formalization. D5/S1/Recurrence/MultiplicativeExclusionResidueClass.S (✓ std3).

Source. Repository-derived.

Commentary.

This is the atom’s witness set verbatim: the exceptional element 3 together with every natural number of the form 3t+1.

Theorem 1.2 (Literal witness set equals the residue description).

$\forall x \in N, x \in S ⟺ (x = 3 \lor x mod 3 = 1) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.mem_S_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

Division with remainder identifies the progression 3t+1 with residue one modulo three, while preserving the exceptional element 3.

Definition 1.3 (Literal candidate-inclusive least-value rule).

$\forall a : N \to N, n, x, r \in N, (a^{[n := x]})_{r} = if (r = n, x, a_{r}), SatisfiesLiteralRule (a) ⟺ (a_{0} = 0 \land a_{1} = 1 \land \forall n \in N, (2 \leq n) \Rightarrow (0 < a_{n} \land a_{n - 1} < a_{n} \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n) \Rightarrow (a_{n} : Z) \neq = ((a^{[n := a_{n}]})_{i} : Z) \cdot ((a^{[n := a_{n}]})_{j} : Z) - ((a^{[n := a_{n}]})_{k} : Z)) \land (\forall x \in N, (0 < x \land a_{n - 1} < x \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n) \Rightarrow (x : Z) \neq = ((a^{[n := x]})_{i} : Z) \cdot ((a^{[n := x]})_{j} : Z) - ((a^{[n := x]})_{k} : Z)) \Rightarrow a_{n} \leq x)) .$

Formalization. D5/S1/Recurrence/MultiplicativeExclusionResidueClass.SatisfiesLiteralRule (✓ std3).

Source. Repository-derived.

Commentary.

The sequence is totalized by a(0)=0 and starts at a(1)=1. For every n at least two, a(n) is the least positive x above a(n-1) for which every ordered index triple 1<=i<=j<=k<=n passes the displayed inequality.

Theorem 1.4 (Integer subtraction is equivalent to the additive exclusion test).

$\forall x, a, b, c \in N, ((x : Z) \neq = (a : Z) \cdot (b : Z) - (c : Z)) ⟺ (x + c \neq = a \cdot b) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.literal_exclusion_iff_additive (✓ std3). ∎

Source. Repository-derived.

Commentary.

For natural x,a,b,c, the left inequality is interpreted in the integers. Moving c across the equality yields exactly the natural-number form used by the internal exclusion predicate.

Theorem 1.5 (The literal and additive sequence rules are identical).

$\forall a : N \to N, SatisfiesLiteralRule (a) ⟺ (a_{0} = 0 \land a_{1} = 1 \land \forall n \in N, (2 \leq n) \Rightarrow (0 < a_{n} \land a_{n - 1} < a_{n} \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n) \Rightarrow a_{n} + (a^{[n := a_{n}]})_{k} \neq = (a^{[n := a_{n}]})_{i} \cdot (a^{[n := a_{n}]})_{j}) \land (\forall x \in N, (0 < x \land a_{n - 1} < x \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n) \Rightarrow x + (a^{[n := x]})_{k} \neq = (a^{[n := x]})_{i} \cdot (a^{[n := x]})_{j}) \Rightarrow a_{n} \leq x)) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.satisfiesLiteralRule_iff_additive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The identity is applied pointwise to every prospective candidate. This public bridge leaves the covered theorems stated for the literal rule while the proof uses addition in the natural numbers.

Theorem 1.6 (The protected residue class cannot be excluded).

$\forall x, u, v, w \in N, (4 \leq x \land (x \in S) \land (u \in S) \land (v \in S) \land (w \in S) \land u \leq v \land v \leq w) \Rightarrow x + w \neq = u \cdot v .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.residue_protection (✓ std3). ∎

Source. Repository-derived.

Commentary.

If x>=4 and x,u,v,w lie in the literal set S with u<=v<=w, then x+w differs from uv. The exceptional element 3 is discharged by the order bound; all remaining cases are protected modulo three.

Theorem 1.7 (Five ordered witness families cover the complement).

$\forall y \in N, (7 \leq y) \Rightarrow (\neg (y \in S)) \Rightarrow \exists u, v, w \in N, ((u \in S) \land (v \in S) \land (w \in S) \land u \leq v \land v \leq w \land w < y \land y + w = u \cdot v) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.witness_of_not_memS (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every y>=7 outside S has ordered u<=v<=w in S, with w<y and y+w=uv.

For t>=1 the proof uses exactly the preregistered families: 9t+3t+4=4(3t+1), (9t+3)+(3t+1)=4(3t+1), (9t+6)+(3t+10)=4(3t+4), (6t+2)+(3t+1)=3(3t+1), and (6t+5)+(3t+7)=3(3t+4).

Definition 1.8 (Well-founded Nat.find realization).

$se q u e n ce : N \to N, se q u e n c e_{0} = 0, se q u e n c e_{1} = 1, \forall n \in N, h_{n} : N \to N := (r \mapsto if (r < n + 2, se q u e n c e_{r}, 0)), se q u e n c e_{n + 2} = if (h e x : \exists x \in N, 0 < x \land (h_{n})_{n + 2 - 1} < x \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n + 2) \Rightarrow x + ((h_{n})^{[n + 2 := x]})_{k} \neq = ((h_{n})^{[n + 2 := x]})_{i} \cdot ((h_{n})^{[n + 2 := x]})_{j}, Nat.find (h e x), 0) .$

Formalization. D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence (✓ std3).

Source. Repository-derived.

Commentary.

At n+2, h_n is the recursively available prefix, zero outside that prefix. The definition applies Nat.find to the set of literal admissible values when it is inhabited and otherwise returns zero. Strong induction proves the fallback unreachable; the recursive call is on r<n+2.

Theorem 1.9 (The recursive sequence satisfies the literal rule).

$SatisfiesLiteralRule (se q u e n ce) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_satisfies_literal_rule (✓ std3). ∎

Source. Repository-derived.

Commentary.

Residue protection makes every target term admissible. The prefix witnesses 2+2=22, 5+4=33, and 6+3=3*3, followed by the five general families, exclude every intervening value and prove leastness.

Theorem 1.10 (The initial term is one).

$se q u e n c e_{1} = 1.$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the initial value required by the OEIS name line.

Theorem 1.11 (The second term is three).

$se q u e n c e_{2} = 3.$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_two (✓ std3). ∎

Source. Repository-derived.

Commentary.

The value two is excluded by the prospective self-witness at i=j=k=n=2, while three is admissible.

Theorem 1.12 (Every later term is the least literal admissible value).

$\forall n \in N, (2 \leq n) \Rightarrow (0 < se q u e n c e_{n} \land se q u e n c e_{n - 1} < se q u e n c e_{n} \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n) \Rightarrow (se q u e n c e_{n} : Z) \neq = ((se q u e n c e^{[n := se q u e n c e_{n}]})_{i} : Z) \cdot ((se q u e n c e^{[n := se q u e n c e_{n}]})_{j} : Z) - ((se q u e n c e^{[n := se q u e n c e_{n}]})_{k} : Z)) \land (\forall x \in N, (0 < x \land se q u e n c e_{n - 1} < x \land \forall i, j, k \in N, (1 \leq i \land i \leq j \land j \leq k \land k \leq n) \Rightarrow (x : Z) \neq = ((se q u e n c e^{[n := x]})_{i} : Z) \cdot ((se q u e n c e^{[n := x]})_{j} : Z) - ((se q u e n c e^{[n := x]})_{k} : Z)) \Rightarrow se q u e n c e_{n} \leq x) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_recurrence (✓ std3). ∎

Source. Repository-derived.

Commentary.

This exposes the recurrence clause of SatisfiesLiteralRule directly for the constructed sequence, including the prospective substitution at n.

Theorem 1.13 (The literal-rule sequence exists uniquely).

$\exists! a : N \to N, SatisfiesLiteralRule (a) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.literal_rule_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

Agreement on all earlier positive indices preserves the exclusion predicate. Strong induction then identifies the least values at every index.

Theorem 1.14 (OEIS A026488 has the exact formula 1, 3, then 3n-5).

$(se q u e n c e_{2} = 3) \land (\forall n \in N, (3 \leq n) \Rightarrow se q u e n c e_{n} = 3 \cdot n - 5) .$

Proof. Machine-checked in Lean as D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_formula (✓ std3). ∎

Source. Repository-derived.

Commentary.

This single theorem carries both numerical clauses of candidate theorem 4.115: a(2)=3 and a(n)=3n-5 for every one-based n>=3. The guarded natural subtraction in 3n-5 is therefore nontruncating.

References

Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.S
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.SatisfiesLiteralRule
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.literal_exclusion_iff_additive
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.literal_rule_unique
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.mem_S_iff
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.residue_protection
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.satisfiesLiteralRule_iff_additive
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_formula
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_one
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_recurrence
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_satisfies_literal_rule
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.sequence_two
Truth anchor: D5/S1/Recurrence/MultiplicativeExclusionResidueClass.witness_of_not_memS

Keyboard shortcuts

trureturing Blueprint

Multiplicative-Exclusion Residue Class

Abstract

References