BalaA363411

Abstract

Integer quadratic products and Bala’s valuation conjectures.

Definition 1.1 (The quadratic integer product).

$$\forall n\in \mathbb{N},P\left(n\right)=\prod _{k\in \mathrm{Finset}.\mathrm{range}\left(n+1\right)}(⟨1,(k:\mathbb{Z})⟩:\mathrm{Zsqrtd}\left(-3\right))$$

Formalization. D5/S3/Arith/Congruence/BalaA363411.P (✓ std3).

Citation. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

OEIS A363411, NAME (revision 18, no page): “a(n) = the real part of Product_{k = 0..n} 1 + k*sqrt(-3).” The product includes k=0 and k=n. The pair in Zsqrtd (-3) denotes 1+k sqrt(-3).

Definition 1.2 (The real coordinate).

$$\forall n\in \mathbb{N},a\left(n\right)=\mathrm{Zsqrtd}.\mathrm{re}\left(P\left(n\right)\right)$$

Formalization. D5/S3/Arith/Congruence/BalaA363411.a (✓ std3).

Citation. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

OEIS A363411, NAME (revision 18, no page): “a(n) = the real part of Product_{k = 0..n} 1 + k*sqrt(-3).” Here a is the integer real coordinate.

Definition 1.3 (The imaginary coordinate).

$$\forall n\in \mathbb{N},b\left(n\right)=\mathrm{Zsqrtd}.\mathrm{im}\left(P\left(n\right)\right)$$

Formalization. D5/S3/Arith/Congruence/BalaA363411.b (✓ std3).

Citation. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

OEIS A363412, NAME (revision 19, no page): “a(n) = 1/sqrt(3) * the imaginary part of Product_{k = 0..n} 1 + k*sqrt(-3).” The source sequence is called b here; it is the sqrt(-3) coordinate.

Definition 1.4 (The five-adic conjecture).

$$\mathrm{claim}=\left(\forall n\in \mathbb{N},\mathrm{padicValInt}\left(5,a\left(n+2\right)\right)=\mathrm{if}5\mid n\mathrm{then}1\mathrm{else}0\right)$$

Formalization. D5/S3/Arith/Congruence/BalaA363411.claim (✓ std3).

Citation. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

OEIS A363411, FORMULA (revision 18, no page): “Conjecture: the 5-adic valuation v_5(a(n+2)) = A079998(n) (checked up to n = 5000).” OEIS A079998, NAME: “The characteristic function of the multiples of five.” All indices are natural numbers, including zero. The conditional has natural values 1 and 0.

Definition 1.5 (Coordinate recursion in a commutative ring).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)](\mathrm{seq}\left(R,0\right)=(1,0))\wedge (\forall n\in \mathbb{N},\mathrm{seq}\left(R,n+1\right)=((\mathrm{seq}\left(R,n\right)).1-3\cdot \left((n:R)+1\right)\cdot (\mathrm{seq}\left(R,n\right)).2,(\mathrm{seq}\left(R,n\right)).2+\left((n:R)+1\right)\cdot (\mathrm{seq}\left(R,n\right)).1))$$

Formalization. D5/S3/Arith/Congruence/BalaA363411.seq (✓ std3).

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

For any commutative ring R in any universe, seq starts at (1,0). Multiplication by 1+(n+1)sqrt(-3) gives the two displayed successor coordinates.

Theorem 1.6 (Real coordinates are one modulo three).

$$\forall I\in \mathrm{Type},\forall s\in \mathrm{Finset}\left(I\right),\forall f\in I\to \mathbb{Z},\exists u\in \mathbb{Z},\mathrm{Zsqrtd}.\mathrm{re}\left(\prod _{i\in s}(⟨1,f\left(i\right)⟩:\mathrm{Zsqrtd}\left(-3\right))\right)=1+3\cdot u$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/BalaA363411.real_one (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

For any finite family of integer coefficients, the real coordinate of the product is one modulo three. The ring homomorphism to ZMod 3 sends sqrt(-3) to zero and each factor to one.

Theorem 1.7 (The recursion equals the product coordinates).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall n\in \mathbb{N},\mathrm{seq}\left(R,n\right)=((a\left(n\right):R),(b\left(n\right):R))$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/BalaA363411.seq_cast (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

The integer coordinates map into every commutative ring. Induction compares the coordinate multiplication formula with the recursion.

Theorem 1.8 (A scalar block controls every later block).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall q\in \mathbb{N},\forall c\in R,((q:R)=0)\Rightarrow ((\mathrm{seq}\left(R,q\right)=(c,0))\Rightarrow (\forall n\in \mathbb{N},\mathrm{seq}\left(R,n+q\right)=(c\cdot (\mathrm{seq}\left(R,n\right)).1,c\cdot (\mathrm{seq}\left(R,n\right)).2)))$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/BalaA363411.seq_shift (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

If q vanishes in R and the qth pair is (c,0), shifting an index by q multiplies both coordinates by c. This holds for every natural index.

Theorem 1.9 (A unit block gives a period).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall q\in \mathbb{N},((q:R)=0)\Rightarrow ((\mathrm{seq}\left(R,q\right)=(1,0))\Rightarrow (\mathrm{Function}.\mathrm{Periodic}\left(\mathrm{seq}\left(R\right),q\right)))$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/BalaA363411.seq_period (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

A block equal to (1,0) yields period q when q vanishes in the coefficient ring. The scalar-block identity gives the equality at every index.

Theorem 1.10 (Reduction of a periodic sequence).

$$\forall R\in \mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall q\in \mathbb{N},(\mathrm{Function}.\mathrm{Periodic}\left(\mathrm{seq}\left(R\right),q\right))\Rightarrow (\forall n\in \mathbb{N},\mathrm{seq}\left(R,n\right)=\mathrm{seq}\left(R,n\mathrm{mod}q\right))$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/BalaA363411.seq_mod (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

A periodic coordinate sequence has the same value at n and at its natural remainder modulo q. The remainder is the Lean natural-number modulo operation.

Theorem 1.11 (Bala five-adic valuation formula).

$$\forall n\in \mathbb{N},\mathrm{padicValInt}\left(5,a\left(n+2\right)\right)=\mathrm{if}5\mid n\mathrm{then}1\mathrm{else}0$$

Proof. Machine-checked in Lean as D5/S3/Arith/Congruence/BalaA363411.result (✓ std3). ∎

Resolves. Problems/bala3634-valuations (proved) by D5/S3/Arith/Congruence/BalaA363411.result.

Source. Repository-derived.

Acknowledgement. P. Bala (2023). OEIS A363411 and A363412 — quadratic integer product coordinates. URL: https://oeis.org/A363411.

Commentary.

The product block at 25 is (7,0) modulo 25. Four successive blocks give period 100. Modulo 5 the real coordinate vanishes exactly at indices congruent to 2, while modulo 25 it never vanishes. These two facts give exactly one factor of 5 at n+2 when 5 divides n, and none otherwise.

References

• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.P
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.a
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.b
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.claim
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.real_one
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.result
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.seq
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.seq_cast
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.seq_mod
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.seq_period
• Truth anchor: D5/S3/Arith/Congruence/BalaA363411.seq_shift