I don’t think 1.838 is the correct lower bound. Would a Lean proof that it’s greater than 1.9 be meaningful to you?
Separately, how small do you need C to be to be meaningful? Like, is 500 materially different from 1771 or do you need single digits for your purposes?
As small as possible would be nice. I expect that a proof of a bound that is close to tight will be much more informative of the structure of the problem than proofs of looser bounds. If the true bound is, say, 2, then I expect a proof of 500 to route through mechanisms that don’t really illuminate what’s going on here.
I don’t think 1.838 is the correct lower bound. Would a Lean proof that it’s greater than 1.9 be meaningful to you?
Separately, how small do you need C to be to be meaningful? Like, is 500 materially different from 1771 or do you need single digits for your purposes?
Could you explain the reason you think the correct lower bound is higher than 1.838?
Edit: Looks like it’s at least 1.948: https://github.com/satchlj/stoch-to-det-lower
I think I have a Lean proof that C > 1.93777676
I see, yeah—I wonder if it’s 2.
I’ve got it up to 1.96
As small as possible would be nice. I expect that a proof of a bound that is close to tight will be much more informative of the structure of the problem than proofs of looser bounds. If the true bound is, say, 2, then I expect a proof of 500 to route through mechanisms that don’t really illuminate what’s going on here.