12:52 AM
@Deadcode I think that A+2+1/A < 4*B is a sufficient condition, where A is the divisor and B is the quotient.
In practice the 1/A doesn't matter so much.
I based this on:
> This regex does division-by-a-variable in the innermost portion of the loop. The division algorithm is the same as in my other regexes (and similar to the multiplication algorithm): for A≤B, A*B=C if any only if C%A=0 and B is the largest number which satisfies B≤C and C%B=0 and (C-B-(A-1))%(B-1)=0, where C is the dividend, A is the divisor, and B is the quotient. (A similar algorithm can be used for the case that A≥B, and if it is not known how A compares to B, one extra divisibility test is all that is needed.)
One can rewrite the conditions as: C = 0 (mod B) and C = A (mod (B-1))
Suppose you find a B' satisfying these conditions, with C=n*B', and B' > B. Then you find that A ≥ x+B'-1.
But x+B' ≥ 2*√C, so A ≥ 2*√C-1. Then A²+2*A+1 ≥ 4*C, so A+2+1/A ≥ 4*B.
Therefore: as long as A²+2*A+1 < 4*C, any B' will be ≤B. And since B is always good, the maximum B' will be B
This was (roughly) my reasoning
The reason that A ≥ x+B'-1 is because x < A and C = A (mod (B'-1)). So x = A (mod (B'-1), so A-x is positive and divisible by (B'-1). So A-x ≥ B'-1

1:18 AM
@H.PWiz How did you get the A ≥ x+B'-1 part?

I tried to explain it right above your message

Oh, I thought it was a prerequisite for getting to the next step

I skipped a couple of steps when first writing

1:32 AM
@H.PWiz How did you get x = A (mod (B'-1)?

C = A (mod (B'-1)), C=x*B', and B' = 1 (mod (B'-1))

@H.PWiz how do you go from x*B' % (B'-1) = A and B' % (B'-1) = 1 to x % (B'-1) = A?

I'm saying that they're equivalent mod (B'-1). So you could add % (B'-1) to the right side of your equations. Essentially, because B' is equivalent to 1 mod (B'-1), x is equivalent to x*B', which is equivalent to A

2:00 AM
@H.PWiz Okay I understand all of it before the x+B' ≥ 2*√C part. How did you get that?

I didn't prove it. I just think it's true. It's probably some well-known theorem. Let me see
Ah, it's just the AM-GM inequality.

Oh right, I understand that intuitively.

2:13 AM
@H.PWiz Awesome, I got it. (You flipped the inequality at the end, but that's just the version that applies to skipping the other assertion instead.) Thank you very much!

Right the inequality flips because we really care about the times when B' is never bigger than B, (i.e the opposite of when there is a B' > B)

Oh right.

2:27 AM
@H.PWiz Oh, there's one more important part to prove
That B' < A
Well, it needs to be proved that x > 1, otherwise we can have B' = A
In order to prove that codegolf.stackexchange.com/questions/164911/… always works, I mean.
Oh yeah, and that B' > 1
Assuming of course that A > 1
and A < C

So, we know that the regex works when A²+2*A+1 < 4*C. What specific other cases do we need to consider? (in terms of A and C)

Well it's not at all guaranteed that A²+2*A+1 < 4*C. And it can give an incorrect quotient when that is not true. But the incorrect quotient doesn't matter because it won't be able to divide it by the divisor again...
because I found (empirically) that the incorrect quotient is always less than the divisor, but always greater than 1.
The regex detects a match if the division loop ends finding that the final quotient equals 1.
In terms of A and C: The regex matches if B=1. It's not always true that A²+2*A+1 < 4*C, and when it isn't, we can have B' as the result of an iteration of division. But if it's always true that 1 < B' < A then this will never result in a false positive.
Oh and furthermore, 1 < B' < A remains true even when we're not guaranteed that C = 0 (mod B). Because the division loop does not reassert this after each division. It's only guaranteed to be true on the first iteration.

2:49 AM
@Deadcode Do you mean (mod A)?

Oops, yeah.
A²+2*A+1 < 4*C itself doesn't actually help with this particular regex, but it is required for codegolf.stackexchange.com/questions/198427/…

In my work, I write A ≥ x+B'-1, so A > B' when x ≥ 2. Now when x = 1, B' = C, so we have A ≥ C. So when A=C, we get the bad quotient B' = C, otherwise the bad quotient B' is <A
Am I right in saying that when the regex sees A=C, it gives a quotient of C?

We never actually get the bad quotient B' = C because it starts looking for quotients at C-A-1
So we always get a good B=1 when A=C

Oh, I see.
@Deadcode Okay, so what's nice is that my "proof" doesn't really care if A divides C. So in this case the bad quotient will still be <A

Er, I mean at C-A
@H.PWiz Yeah, that's pretty cool.
That's what I thought, but wanted to confirm.
@H.PWiz Oops, when I said it needs to be proved x > 1, that was a mistake. It need to be proved that B' > 1 when A < C

3:07 AM
Hmm, I think this is true. (It's obviously true when A divides C)

Er, I mean that B' > 1 when A ≠ C

Okay, the regex in your consecutive-prime-power regex is (?=((x*)(?=\2\16*\$)x)(\15*\$)) This can only match 1 when A divides C. But, then it has the option of matching B which is normally bigger than 1
@H.PWiz It is confusing to think of it returning B'=1 since we are considering A%(B'-1). It seems that getting B' = 1 is a unary-regex trick

@Deadcode Oh neat, I can reply to myself. But I had to copy the permalink and paste the ID after a colon manually to do it. How did you do it?

The same way

@H.PWiz Right, because in regex, 0 = 0 (mod 0)
It's pretty convenient, isn't it?
Yeah, so we can never get B'=1, only B=1 and that's iff A=C. Because in regex, y=0 is the only y that satisfies y = 0 (mod 0). In this it's important that we're actually doing ` C-B-(A-1) = 0 (mod B-1)`

3 hours later…
6:25 AM
@H.PWiz Your Lynch-Bell inspired me to take another crack at Two Bit Numbers™️ and it worked! -4 bytes: codegolf.stackexchange.com/questions/211840/…