📏 Any chance of some #maths terminology help here, folks?

We're looking at a board of @simontatham's Loopy, and it's the logic around that squared 2-region I'm interested in.

• The Top edge has already been erased, so cannot count towards the region's total.
• We know that the line entering its bottom-left corner must continue along either its Left or Bottom edge, but not both, thus accounting for 1 of the 2 line segments the region needs drawn.
• Therefore, the Right edge must inevitably be drawn, to bring the region's total to 2.

It's that "optionality leading to inevitability" I'm wondering if there's a term for. Found my way to the Wiki article on Integer partition – https://en.wikipedia.org/wiki/Integer_partition – which I think feels kinda close, and am temped to refer to this logic as "Partitioning". But does anyone with more maths language up their sleeve than me have a better idea?

#Math

I can't help with the terminology but am delighted that someone else on here is as much into Loopy as I am ❤️ Hope you are going to get an answer.
@AngelaCarstensen Aww, cheers! Yeah, I'm actually thinking of putting together a little set of them, printed out, to introduce my 4½ year old nephew. Hoping to teach "gradually working through a problem" and "discovery of logic", you know?
Proof by exhaustion - Wikipedia

@OscarCunningham @simontatham Aaah, yeah, cheers! I'm definitely preferring the "proof by cases" wording over the notorious "brute force method", but I think this does fairly describe it. Maybe?

I suppose my only doubt: Wouldn't the cases here be the unknown choice between Left and Bottom edge, with this "proof by exhaustion" involving exhausting those two cases? In our logic, though, we're actually saying we're ignoring those cases on the understanding that one of them will end up being correct, and just letting this tell us that the Right edge must be drawn.

Unless, I dunno, do we say:

Case 1: Left or Bottom Edge (proven one, but not both, must be drawn)
Case 2: Right Edge (proven must be drawn)

@miblo @OscarCunningham in hat or Spectre Loopy I find there are a lot more arithmetic-based deductions, because of all the pairs of adjacent faces that share a path of >1 edge. Lots of "this path of 4 edges can't be on because then no other path around this face is small enough to not go over the clue count", or " the edge count is even so this path which is the only odd one must not be included".
@simontatham @OscarCunningham Oh yeah, definitely! I reckon this is why I found the spectres boards seem to solve themselves. Thinking, once we've spotted the spectres have 14 edge segments, and how adjacent ones interact in the way you describe, we're laughing.