@H.PWiz There are at least two things left to prove about division. 1) That C≡B (mod A-1) and C≡A (mod B-1) together always give the correct quotient, and 2) That using just the C≡B (mod A-1) test, finding the smallest matching quotient, will always give the right answer when A^2>C≥A (or perhaps a looser inequality)

I'm going to try it myself now... first need to refresh myself on the first proof.

Hello @Greedo :)

@H.PWiz I'm afraid I have no clue how to proceed. I need your help, please. :) If you don't have time for it I'll ask on math stack exchange...

For 1), Let C=A*X, suppose B>X with B*Y=C and C≡B (mod A-1), C≡A (mod B-1). We can factor C in both cases: X≡B (mod A-1), Y≡A (mod B-1).

Now, since B>X, B≥X+A-1. Similarly, A≥Y+B-1. So B≥X+Y+B-2, so X+Y≤2, i.e X=Y=1.

So ignoring that case, the regex will never find a divisor exceeding the quotient. The case A=C can be easily reasoned about.

(I think this makes sense)

For 2), Let C=A*X, suppose B<X with C≡B (mod A-1). Then X≡B (mod A-1), so X≥B+A-1 or, equivalently, B≤X-A+1. So X≥A, i.e A²≤C.

There may be some cleverer argument that gives a better inequality, though

Sorry, I just pick letters at random each time I look at this stuff

Actually I was thinking about #2 at that point by accident.

Okay so I'm going to start with #2, because that's what I was trying to make progress with on my own before asking for your help today...

@H.PWiz How do you get X≡B (mod A-1)? That's exactly what I was trying to prove and I had no idea how

You skipped exactly the step that was flummoxing me

Well C=A*X, and A≡1 (mod A-1)

You have an incorrect step there

@H.PWiz C=A*X is not true, it's C=Y*X

Can we refer to X as B' instead and Y as A'? That's easier for me

er

Sure. I'll rewrite 2) now

C and A are the givens, and B is the unknown, but it is uniquely determined by C and A. B' is an incorrect value potentially found by the algorithm.

Let C=A*B, suppose B'<B with C≡B' (mod A-1). Then B≡B' (mod A-1), so B≥B'+A-1 or, equivalently, B'≤B-A+1. So B≥A, i.e A²≤C.

(So, when A²>C, there is no B'<B)

And how do you get B≡B' (mod A-1)?

Oh, I see now.

Why couldn't I get that on my own? I laid out all that stuff in front of me and it looked like I didn't have what was needed.

It's frustrating, I was literally trying to do that exact kind of step, and it looked like I didn't have the needed moduli.

Anyway, thanks very much! Now I'll put that into MathJax and then look at #1.

@H.PWiz Well in this case, that inequality is the exact one I got empirically, so that seems unlikely.

Okay, not so fast.

@H.PWiz Okay so to get from B'≤B-A+1 to B≥A (the target), I think you're making the argument that B'>0 therefore B-A+1>0therefore B-A>=0 so B≥A. But B'>0 is nowhere in our axioms, is it?

Oh, we can add that in

Of course.

Okay cool.

Right, I just knew that the regex would only consider positive numbers

@H.PWiz Holy shit. I looked at the math, and nowhere did it use the axiom that C≡0 (mod B'). So I tried lopping that off the regex, and sure enough (x(x*)),(x*?)(?=\1*$)(x+?)\2+$ works! That is incredibly short, there has to be a use for it in some of our regexes

That's pretty neat

@H.PWiz Okay, among things still left to prove: That the first shortened form always works when A is a prime power.