Primes are just counting, twin primes are just counting also.

Twin Primes are infinite:

Proof:

In the modular clock version of Sieve of Eratosthenes, that everyone keeps telling me is so trivial: the literal definition of prime is all of the clocks are non zero. That is the only condition that is required of it.

Therefore, the only condition for a twin prime is that Mod 2 and mod 3 are fixed at 0.
The relationship between primes does not change in any way , mod 5 mod 7 mod 11 mod 13 all continue to open because the series of primes are infinite.

It is always possible to find the next prime by simply counting, and if you hold mod 2 and mod 3 at zero, it is equivalent to finding the next twin prime address, it changes nothing about the relationship between primes.

Conclusion:
The decision is this prime? Is a geometric logical operation, and simply reduces to 1 or 0 in binary logic simply by looking at the clock... if it is 0, it is 0... simple as that.

But you can still keep counting past a 0 if you want to, and continue adding a new coprime to the cycle.

Deeper thoughts rather than formal conclusions: Choices are immutable and some choices are hard to understand when viewed backwards, but it is always possible to count forwards by keeping track of every angle.

Continuing to seek the best way to prove this in lean, I've never used lean before though so I'm still getting the ideas for it.