The Mysterious Lock of Monte Carlo

Chapters 8 and 13 from [The Lady or the Tiger]

Here is a [calculational solution] to this problem. This puzzle was also published as Weekly Puzzle 32: The Lock on The Weekly Puzzles. In this solution I will use that version.

Representation

We use the following abbreviations for statements about combinations:
  O.x == "x opens the lock"
  N.x == "x is neutral"
  J.x == "x jams the lock"
x and y represent combinations; a combination is a non-empty digit sequence. p and q represent (possibly empty) digit sequences. We also introduce the following notations for sequences:
  p = q == "p and q contain the same digits in the same order"
  <p> = "the sequence that is the reverse of p"
So for example <1233> = 3321.

The crucial notation that we introduce is:

  [x] = "the combination to which x is related"
In terms of the machines in Chapters 9 through 13 in [The Lady or the Tiger], [x] is the output of the machine for input x.

Solution

Using these notations we can represent the five properties as follows:
 (A)  [2x2] = x
 (B)  [1x] = 2[x]
 (C)  [5x] = <[x]>
 (D)  [9x] = [x][x]
 (E1) N.x => J.[x]
 (E2) J.x => N.[x]
We are also given that
 (Z)  exactly one of O.x, N.x, and J.x is true
One consequence of this (see my discussion of [Trilemmas]) is:
 (Z1) O.x == N.x == J.x
All these properties hold for all combinations x.

The problem is now to find the shortest x for which O.x.

Step 1

For any combination x:
   O.x
==   "(Z1)"
   N.x == J.x
==   "logic, working towards (E1) and (E2)"
   (N.x => J.x) /\ (J.x => N.x)
<=   "(E1); (E2)"
   [x] = x
So any combination that is related to itself will open the lock.

Intermezzo: operations

Properties (A)-(D) allow us to simplify values of form [...]. But it is easy to see that they only work for values of the form [m2x2], where x is an arbitrary combination, and m is a (possibly empty) sequence of 1s, 5s, and 9s. For reasons that will become clear in a moment, we call each of those digits an 'operation digit'; n stands for an arbitrary operation digit. m is an 'operation sequence', i.e., a (possibly empty) sequence of operation digits.

Because expressions of the form [m2x2] occur often, we introduce a special notation:

  m.x = [m2x2]
We use a function-application notation here, with a reason. Let's compute 1.x:
   1.x
=    "definition of ."
   [12x2]
=    "(B)"
   2[2x2]
=    "(A)"
   2x
When we do this also for 5 and 9, we get
 (B') 1.x = 2x
 (C') 5.x = <x>
 (D') 9.x = xx
So we see that these digits are operations: 1 prepends a 2, 5 reverses, and 9 duplicates a digit sequence.

We can also combine operations:

 (*)  n.(m.x) = nm.x
We prove this only for n=1; the other proofs are similar.
   1.(m.x)
=    "(B')"
   2(m.x)
=    "definition of ."
   2[m2x2]
=    "(B) from right to left"
   [1m2x2]
=    "definition of ."
   1m.x
To give a simple example, it is easy to compute that
   51.78
=    "(*) from right to left"
   5.(1.78)
=    "(B')"
   5.278
=    "(C')"
   872
In the next step we will perform a similar situation, but then from bottom to top.

Step 2

Armed with the knowledge about operations, we continue our quest for a self-related combination.
   [x] = x
<=   "write x as m2y2"
   (Em,y| x = m2y2: [m2y2] = m2y2)
Now we would like to write m2y2 as an operation on m and y. Since we know that we have a duplication operation, it seems that m2m2 is easier to rewrite. Therefore we calculate:
   m2m2
=    "(D') from right to left"
   9.m2
=    "definition of <...>, to put the 2 up front"
   9.<2<m>>
=    "(C') from right to left"
   9.(5.2<m>)
=    "(B') from right to left"
   9.(5.(1.<m>))
=    "(C') from right to left"
   9.(5.(1.(5.m)))
=    "(*), three times"
   9515.m
=    "definition of ."
   [95152m2]
With this we can continue our earlier calculation:
   (Em,y| x = m2y2: [m2y2] = m2y2)
<=   "take y:=m"
   (Em| x = m2m2: [m2m2] = m2m2)
==   "proof above"
   (Em| x = m2m2: [m2m2] = [95152m2])
<=   "Leibniz' rule"
   (Em| x = m2m2: m2m2 = 95152m2)
==   "remove 2m2 at the end"
   (Em| x = m2m2: m = 9515)
==   "one-point rule"
   x = 9515295152
Summarizing the complete calculation, we proved
  (Ax| x = 9515295152: O.x)
or equivalently O.9515295152. And this is a combination that opens the lock. I also believe this to be the shortest one, but have not been able to prove that.

Post Scriptum

It was only after I wrote the above, and contacted Tim Edmonds of The Weekly Puzzles about this solution, that I saw his. It turned out that there is a shorter combination; here is a calculational explanation.

Because of (Z) we know that a combination opens the lock iff it is not neutral and also doesn't jam it. In other words,

 (Z2) O.x == !J.x /\ !N.x
(This is another consequence of (Z): see [Trilemmas].) This allows us to prove a statement of the form O.x as follows:
   O.x
==   "(Z2)"
   !J.x /\ !N.x
<=   "(E1) and (E2) from right to left"
   !N.[x] /\ !J.[x]
==   "(Z2) from right to left"
   O.[x]
Applying this to the combination that we already found, and abbreviating m = 9515, we get
   O.m2m2                            --- already proved above
==   "(D') from right to left"
   O.(9.m2)
==   "definition of ."
   O.[92m22]
=>   "the property we've just proven"
   O.92m22
So 92951522 is also a working combination, and it is shorter that the one I (and Smullyan) found. Again, I cannot prove that it is the shortest.
This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.
Changes to calc/tlott-8-and-13.html:

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
  * Move from CVS to darcs: do not show the CVS date anymore.

Thu Feb  7 19:43:35 MET 2002  marnix
  * Updated all files to use the m4 template

Wed Sep  5 21:20:00 MEST 2001  marnix
  * Made explicit that last changed date is in GMT

Wed Sep  5 21:08:51 MEST 2001  marnix
  * Now 'last changed' is on its own line

Wed Sep  5 10:10:47 MEST 2001  marnix
  * Added date last changed

Wed Sep  5 08:50:24 MEST 2001  marnix
  * Initial revision