I deal only with JExocet, leaving the JE+ extension and daj's additional eliminations for later.

I hope we can agree on a final definition, at least for this core case.

Remark: I replaced "base candidate" by "base digit" because what we generally call a candidate is a <cell, digit> pair.

JEXOCET DEFINITION

Conditions on the Pattern of Cells

- Code: Select all
`*-------*-------*-------*`

| B B . | . . . | . . . | B = Base Cell Pair, in the Base Row and the Base Block/Box

| . . . | Q . . | R . . |

| . . . | Q . . | R . . | Q = 1st Object Cell Pair

*-------*-------*-------* R = 2nd Object Cell Pair

| . . S | S . . | S . . |

| . . S | S . . | S . . | S = Cross-line Cells

| . . S | S . . | S . . |

*-------*-------*-------* . = Any candidates (including base digits)

| . . S | S . . | S . . |

| . . S | S . . | S . . |

| . . S | S . . | S . . |

*-------*-------*-------*

The Base Cell Pair (B) and the two Object Cell Pairs (Q and R) occur in three different blocks/boxes in the same band (the JE band).

The three "cross-lines" intersect this band as shown, passing through the Object Cell Pairs but not through the Base Cells.

Conditions on candidates

1) No base cell is decided.

Each base cell may have up to 4 candidates, but together, they contain exactly 3 or 4 digits (called the base digits).

2) Each Object Cell Pair is made of two cells: the target cell and the companion cell

Each target cell contains at least one base digit (plus possibly non-base digits)

Companion cells contain no base digit

3) For each base digit, there are two units/houses containing/covering all its occurrences in the S cells (be it as a candidate or as a decided value).

JEXOCET RULE

Theorem: if a JExocet is present in some resolution state, then its non-base digits can be eliminated from its target cells.

PROOF OF THE JEXOCET RULE

Let a and b be the (unknown) true values of the two base cells. By the rules of Sudoku, each of a and b must be the value of a cell in each of the three "cross-lines" containing the S cells.

But condition 3 entails that each of a and b can be the value of at most two S cells. Therefore (as neither a nor b can be in the Base Row or the Base Block anywhere outside the B Cells) each of a and b must also be the value of one of the Q or one of the R cells.

By condition 2, each of a and b must therefore be the value of the Q or the R target cell.

We have thus proven that the values of the two target cells are the same as those of the two base cells.

We don't know these values, but this is enough to exclude any non base digit from the target cells.

Remark: the cardinality of the set of base digits didn't play any role in the proof.