My suspicion about the thin-tailed risk here is that either congress or the SEC passes landmark regulation about SPACs (which is potentially plausible) and those stocks go to 0, very quickly, as the initial investors who IPOed the SPAC pull their money out.  See, ICOs (though those were obviously higher risk)

Ohhh, thanks. That explains it. I feel like there should exist things for which provable(not(p)), but I can't think of any offhand, so that'll do for now.

To answer the below: I'm not saying that provable(X or notX) implies provable (not X). I'm saying...I'll just put it in lemma form(P(x) means provable(x):

If P( if x then Q) AND P(if not x then Q)

Then P(not x or Q) and P(x or Q): by rules of if then

Then P( (X and not X) or Q): by rules of distribution

Then P(Q): Rules of or statements

So my proof structure is as follows: Prove that both Provable(P) and not Provable(P) imply provable(P). Then, by the above lemma, Provable(P). I don't need to prove Provable(not(Provable(P))), that's not required by the lemma. All I need to prove is that the logical operations that lead from Not(provable(P))) to Provable(P)) are truth and provability preserving

is x or not x provable? Then use my proof structure again.

So then here's a smaller lemma: for all x and all q:

If(not(x))

Then provable(if x then q): by definition of if-then

So replace x by Provable(P) and q by p.

Where's the flaw?

Oh, that's what I've been failing to get across.

I'm not saying if not(p) then (if provable(p) then q). I'm saying if not provable(p) then (if provable(p) then q)

So the statement (if not(p) then (if p then q)) is not provable in PA? Doesn't it follow immediately from the definition of if-then in PA?

That doesn't actually answer my original question--I'll try writing out the full proof.

Premises:

1. P or not-P is true in PA

2. Also, because of that, if p -> q and not(p)-> q then q--use rules of distribution over and/or

So:

1. provable(P) or not(provable(P)) by premise 1

2: If provable(P), provable(P) by: switch if p then p to not p or p, premise 1

3: if not(provable(P)) Then provable( if provable(P) then P): since if p then q=not p or q and not(not(p))=p

4: therefore, if not(provable(P)) then provable(P): 3 and Lob's theorem

5: Therefore Provable(P): By premise 2, line 2, and line 4.

Where's the flaw? Is it between lines 3 and 4?

Well, there is, unless i misunderstand what meta level provable(not(provable(consistency))) is on.

Your reasons were that not(provable(c)) isn't provable in PA, right? If so, then I will rebut thusly: the setup in my comment immediately above(I.e. either provable(c) or not provable(c)) gets rid of that.