Leren & Danny, I have now found the cause of my <false retraction> which came from my failure to realise that the posted grid that provided the assumed counter example contained an unsound JExocet.
I take a very simple truth counting approach which does away with having to consider degenerate cases - I don't care if any truth has already been proved or not, it still gets counted!
To walk through my proof:
- Code: Select all
CL1 CL2 CL3
. . S | . S . | S . . . = Any digit
. . S | . S . | S . . a,b = base digits
. . S | . S . | S . . * = a & b eliminations in sight of base cells
. . S | . S . | S . . S = Crossline cells in the other bands
. . S | . S . | S . .
. . S | . S . | S . . P = 2 Cells restricted to 1 truth for (ab)
------+--------+------- Q = 2 Cells restricted to 1 truth for (ab)
a b * | * * * | * * *
* * * | . P . | Q . .
* * * | . P . | Q . .
1. The base cells, must hold two of the base digits (ab) which will makes them false in JExocet band,crossline1 (b7c3)
2. By selection, crosslines 2 & 3 can each only hold one of the base digits in the JExocet band - in the target cells (r89c5 & r89c7)
3. This forces the parallel bands,crosslines123 to hold at least 4 truths for (a) & (b) (in the S cells, as the 3 cross lines must each hold one truth for each digit)
4. If these cells are restricted to a single truth for (a) they must therefore hold three truths for (b).
5. When no selection for (b) allows this, the base cells can't hold (a) and it can be eliminated from them.
( (a)would be true in b14c3 and in the two target cells, (b) could be true in two S cells but then couldn’t be assigned in the 3rd cross line)
I've been trying to re-absorb the various contributions made in this thread, some of which are very powerful but depend on specific extra conditions. This makes organising the material awkward to say the least. My thoughts at the moment are to create a hierarchy of JExocet patterns which reflects both the amount of effort it needs to confirm their different conditions exist, and how frequently they occur. Each level of the hierarchy will then need theorems to prove the inferences they provide. I'm afraid that will have to wait a while as I have other priorities as I hope you shall soon see.
DAJ wrote:Hopefully, I'm not covering old territory!
I'm afraid you are and have just discovered a gap in your coding.