3-MAR-2026

2245

Prop 3.3 is done, but nasty; it’s actually been done for a bit but I’ve been working on something else. A couple things, actually.

First I got separate working so now distinct conditions are pretty easy to deal with. Ex 3.1 is much improved as a result.

I started working on generating the blueprint; but there’s a ways to go.

The proof of 3.3 is very long, and I have to replicate it pretty heavily to prove the other half of the condition; which is pretty gnar. It’s the same up to some renaming, but I am having trouble seeing what I could extract. I did do a bit to allow collinear conditions to stand in directly for lines in all but the case where I’m trying to prove A on cL, where cL is a collinear condition. The prover gets confused about what kind of membership it should use, which breaks stuff.

I might try just winging it with the other half and see if I find a shorter approach, I have an advantage of not minding tedious cases that maybe would scare off someone in a setting where case-reasoning is cheaper.