User: Start with the moving mirror at speed 1/3 to the right. First one diagonal, then two down, then diagonal, two down. The input word is [()]. Show me the trace.
Response:
pos: 0 1 2 3 4 5 6 7
─────────────────────────────────────
t=0 () M─┐
│
t=1 () └─M
│
t=2 () │
│
t=3 () M─┐
│
t=4 () └─M
│
t=5 () │
User: Don't use connecting lines. Start with the input word at the top. Put M everywhere, even when it doesn't move. Use M1, M2, M3 for the state.
Response:
pos: 0 1 2 3 4 5 6 7
──────────────────────────────────────────
t=0 () M1
t=1 () M2
t=2 () M3
t=3 () M1
t=4 () M2
t=5 () M3
t=6 () M1
t=7 () M2
t=8 () M3
t=9 () M1
t=10 () M2
t=11 () M3
t=12 () M1
t=13 () M2
t=14 () M3
User: No need to mark the border "()" or whatever you mean with that. Put the input word above:
# # Unit # # #
(unit is at pos = 0, the first borders are at p = -2 and -1)
Response:
pos: -2 -1 0 1 2 3 4 5 6 7
input: # # Unit # # # # # # #
──────────────────────────────────────────────────────
t=0 M1
t=1 M2
t=2 M3
t=3 M1
t=4 M2
t=5 M3
...
User: M1 starts at t=0, p=0...
Response:
pos: -2 -1 0 1 2 3 4 5 6 7
input: # # Unit # # # # # # #
──────────────────────────────────────────────────────
t=0 M1
t=1 M2
t=2 M3
t=3 M1
t=4 M2
t=5 M3
t=6 M1
t=7 M2
t=8 M3
t=9 M1
t=10 M2
t=11 M3
t=12 M1
t=13 M2
t=14 M3
Mirror position: pos(t) = floor(t/3)
State transitions:
- M1 → M2: move right 1 position
- M2 → M3: stay
- M3 → M1: stay
Speed = 1/3.
User: Next, add a second diagram for the bouncing signal S (which includes M, so copy that). It is also at t=0 and p=0, then goes one right (like M2), but then bounces back to t=2 p=0, and then right again.
Response (assumed signal bounces at p=-1, which was wrong):
pos: -2 -1 0 1 2 3 4 5 6 7
input: # # Unit # # # # # # #
──────────────────────────────────────────────────────
t=0 S,M1 S at p=0 →, M at p=0
t=1 S,M2 S at p=1 →, M at p=1. Collision! S reflects ←
t=2 S M3 S at p=0 ←
t=3 S M1 S at p=-1 (border). Bounce →
t=4 S M2 S at p=0 →, M at p=2
t=5 S M3 S at p=1 →, M at p=2
t=6 S,M1 S at p=2, M at p=2. Collision! S reflects ←
t=7 S M2 S at p=1 ←, M at p=3
t=8 S M3 S at p=0 ←
t=9 S M1 S at p=-1 (border). Bounce →
t=10 S M2 S at p=0 →, M at p=4
t=11 S M3 S at p=1 →, M at p=4
t=12 S M1 S at p=2 →, M at p=4
t=13 S M2 S at p=3 →, M at p=5
t=14 S M3 S at p=4 →, M at p=5
t=15 S,M1 S at p=5, M at p=5. Collision! S reflects ←
t=16 S M2 S at p=4 ←, M at p=6
t=17 S M3 S at p=3 ←
t=18 S M1 S at p=2 ←
t=19 S M2 S at p=1 ←
t=20 S M3 S at p=0 ←
t=21 S M1 S at p=-1 (border). Bounce →
Signal returns to p=0: t=0, 2, 8, 20...
Differences: 2, 6, 12... not doubling. Something was wrong.
User: It bounces at 0. It will hit the mirror at M1 and needs to travel along until M2.
Response (corrected with both fixes):
Two key rules:
- Signal bounces at p=0 (not p=-1)
- Signal hits mirror at M1, travels along with it until M2, then released going left
pos: -2 -1 0 1 2 3 4 5 6 7 8
input: # # Unit # # # # # # # #
─────────────────────────────────────────────────────────────
t=0 S,M1 S at p=0 →, hits M1. Travel along.
t=1 S,M2 S,M at p=1. M2: released ←
t=2 S M3 S at p=0 ←. Bounce →
t=3 S,M1 S at p=1 →, hits M1. Travel along.
t=4 S,M2 S,M at p=2. M2: released ←
t=5 S M3 S at p=1 ←
t=6 S M1 S at p=0 ←. Bounce →
t=7 S M2 S at p=1 →
t=8 S M3 S at p=2 →
t=9 S,M1 S at p=3 →, hits M1. Travel along.
t=10 S,M2 S,M at p=4. M2: released ←
t=11 S M3 S at p=3 ←
t=12 S M1 S at p=2 ←
t=13 S M2 S at p=1 ←
t=14 S M3 S at p=0 ←. Bounce →
t=15 S M1 S at p=1 →
t=16 S M2 S at p=2 →
t=17 S M3 S at p=3 →
t=18 S M1 S at p=4 →
t=19 S M2 S at p=5 →
t=20 S M3 S at p=6 →
t=21 S,M1 S at p=7, hits M1. Travel along.
t=22 S,M2 S,M at p=8. M2: released ←
t=23 S M3 S at p=7 ←
t=24 S M1 S at p=6 ←
t=25 S S at p=5 ←
t=26 S S at p=4 ←
t=27 S S at p=3 ←
t=28 S S at p=2 ←
t=29 S S at p=1 ←
t=30 S S at p=0 ←. Bounce →
Signal at p=0 at times: t = 0, 2, 6, 14, 30
Differences: 2, 4, 8, 16 — doubles each time!
Return times: t = 2^(k+1) − 2
User: Now think about what states S needs to make this proper. Also, remove the comments to the side.
Response:
| State | Description |
|---|---|
# |
Border |
|
Empty |
SR |
Signal moving right |
SL |
Signal moving left |
M1 |
Mirror phase 1 (about to move right) |
M2 |
Mirror phase 2 (just moved) |
M3 |
Mirror phase 3 (resting) |
SM1 |
Signal caught mirror at phase 1 |
SM2 |
Signal + mirror phase 2, signal released left |
S always approaches M from the left (speed 1 > 1/3), so S and M only overlap as SM1/SM2.
pos: -2 -1 0 1 2 3 4 5 6 7 8
input: # # Unit # # # # # # # #
─────────────────────────────────────────────────────────────
t=0 SM1
t=1 SM2
t=2 SL M3
t=3 SM1
t=4 SM2
t=5 SL M3
t=6 SL M1
t=7 SR M2
t=8 SR M3
t=9 SM1
t=10 SM2
t=11 SL M3
t=12 SL M1
t=13 SL M2
t=14 SL M3
t=15 SR M1
t=16 SR M2
t=17 SR M3
t=18 SR M1
t=19 SR M2
t=20 SR M3
t=21 SM1
t=22 SM2
t=23 SL M3
t=24 SL M1
t=25 SL
t=26 SL
t=27 SL
t=28 SL
t=29 SL
t=30 SL
t=0 SM1 (start)
t=2 SL (first return) diff = 2
t=6 SL (second return) diff = 4
t=14 SL (third return) diff = 8
t=30 SL (fourth return) diff = 16
δ(left, center, right) → new center:
δ( # , SL, _ ) = SR -- bounce at border (p=0, SL→SR)
δ(SR , _ , _ ) = SR -- signal propagates right
δ( _ , _ , SL) = SL -- signal propagates left
δ( _ , SR, _ ) = -- signal left this cell
δ( _ , SL, _ ) = -- signal left this cell
δ( _ , M1, _ ) = M2 (shift right)
δ( _ , SM1, _ ) = SM2 (shift right)
δ( _ , SM2, _ ) = M3 -- mirror stays, signal released left
δ(SM2, _ , _ ) = SL -- signal appears left of SM2
δ( _ , M2, _ ) = M3 -- mirror resting
δ( _ , M3, _ ) = M1 -- mirror ready to move again
δ(SR , M1, _ ) = SM1 -- signal catches mirror → captured
The CA recognizes times t = 2^(k+1) − 2 at position 0 for input [Unit].
By composing with:
- The construction that prepends
[()]to any word - The k-step composition
We get a CA_rt recognizing { w | w.length = 2^n }.
User: Don't mix M and S. Let's keep them in a tuple — we'll later run M from a signal. I.e. SM1 is SR,M1. SR just bounces back at M2. I believe we need just 2 states for S and then just check the state of M. The invariant for M is easy, especially since it does not depend on S. I'm worried about S. Give me ideas how the invariant could look like. I want to avoid monster proofs.
Response:
Cell state = tuple (S, M):
S ∈ {∅, SR, SL}— just directionM ∈ {∅, M1, M2, M3}— independent of S
Bounce rule: SR at a cell with M2 → becomes SL. That's it.
pos: -2 -1 0 1 2 3 4 5 6 7 8
input: # # Unit # # # # # # # #
────────────────────────────────────────────────────────────────────────────
t=0 SR,M1
t=1 SR,M2 ← bounce!
t=2 SL M3
t=3 SR,M1
t=4 SR,M2 ← bounce!
t=5 SL M3
t=6 SL M1
t=7 SR M2
t=8 SR M3
t=9 SR,M1
t=10 SR,M2 ← bounce!
t=11 SL M3
t=12 SL M1
t=13 SL M2
t=14 SL M3
t=15 SR M1
t=16 SR M2
t=17 SR M3
t=18 SR M1
t=19 SR M2
t=20 SR M3
t=21 SR,M1
t=22 SR,M2 ← bounce!
t=23 SL M3
t=24 SL M1
t=25 SL
t=26 SL
t=27 SL
t=28 SL
t=29 SL
t=30 SL
Lemma 1 — Mirror invariant (easy induction, S-independent):
mirror_pos(t) = ⌊(t+2)/3⌋mirror_state(t) = M_{(t mod 3) + 1}
Lemma 2 — Phase structure (definition + arithmetic): S alternates between right-going and left-going phases:
- Phase k right: t ∈ [b(k), b(k)+2^k], signal at position t − b(k)
- Phase k left: t ∈ [b(k)+2^k, b(k+1)], signal at position b(k+1) − t
- Where b(k) = 2^(k+1) − 2
Lemma 3 — No-spurious-bounce (one calculation): During right-going phase k, S and M positions only coincide for j ∈ {2^k−1, 2^k}:
- j = 2^k: M is M2 → intended bounce ✓
- j = 2^k−1: M is M1 → no bounce ✓
During left-going phase: S goes left, M goes right → they diverge. Trivial.
Lemma 4 — Inductive step (combines lemmas): I(k) → I(k+1): bounce at p=0, travel right, bounce off M2 at 2^k, travel left back to p=0.
Each lemma is short and self-contained. No monster proofs.
User: Go more formal now. Define the CA (Q and δ) in Lean, state the invariants (sorry as proof), use comments to explain. Create a new Lean file.
Copilot's approach: Defined SigState (SR/SL/None), MirrorState (M1/M2/M3/None/Border), typed as ExpQ = SigState × MirrorState. Used a Border variant in MirrorState to detect position 0 (SL bounces when left neighbor is Border).
Problem: The Border state polluted the mirror logic. Border cells (positions outside the word) had MirrorState.Border, and the mirror had to handle Border in every match. The transition function was getting complicated.
Also: Copilot initially had the wrong bounce rule — center.2 == .M2 checked the previous state at the receiving cell, not the new state. The signal and mirror arrive simultaneously at the same cell, so the bounce must check m' (the computed new mirror state), not center.2.
Debugging trace (from Lean #eval!):
Debug code — traced state at positions -1 through 3 over time:
def debug_pos (t : ℕ) (p : ℤ) : ExpQ :=
let w : Word Unit := [()]
exp_ca'.nextt (⦋⟬w⟭⦌) t p
#eval! (List.range 8).map (fun t => (t,
(debug_pos t (-1), debug_pos t 0, debug_pos t 1, debug_pos t 2, debug_pos t 3)))First bug — signal escaped to the right, never bouncing:
t=0: p=0 (SR,M1), p=1 (None,None)
t=1: p=0 (None,None), p=1 (SR,M2) ← SR arrived at M2 but didn't bounce!
t=2: p=1 (None,M3), p=2 (SR,None) ← signal kept going right
Cause: bounce checked center.2 == .M2 (old state), but M2 only appeared via shift.
Fix: check m' == .M2 (new computed state).
Second bug — after fixing bounce, signal bounced everywhere:
t=0: p=0 (SR,M1)
t=1: p=1 (SL,M2) ← bounced correctly!
t=2: p=0 (SR,None) ← bounced at border correctly!
t=3: p=1 (SR,M1)
t=4: p=2 (SL,M2) ← bounced correctly!
t=5: p=1 (SR,None) ← WRONG! Should continue left, not bounce
Cause: SL bounce check left == (.None, .None) matched any empty cell, not just border.
Fix: used Border variant (later replaced by is_unit triple).
User: I think the mirror state shouldn't worry about where the border is. It should be a triple (S, M, is_unit), to remember where the single unit character was (it only needs to work on the word [Unit]). Does this simplify things?
Response: Yes — much cleaner.
Cell state = triple (S, M, is_unit):
S ∈ {∅, SR, SL}— signalM ∈ {∅, M1, M2, M3}— mirror (no Border variant needed)is_unit : Bool— true only at position 0, permanently
Mirror transition is pure: M1→(shift right)→M2→M3→M1, no special cases.
Signal bounce: SL bounces to SR when is_unit = true at current cell.
abbrev ExpQ := SigState × MirrorState × Bool
def exp_δ (left center right : ExpQ) : ExpQ :=
let m' := match center.2.1 with
| .M1 => MirrorState.None
| .M2 => MirrorState.M3
| .M3 => MirrorState.M1
| .None =>
match left.2.1 with
| .M1 => MirrorState.M2
| _ => MirrorState.None
let u := center.2.2 -- is_unit never changes
let s' :=
let incoming := match left.1 with
| .SR => SigState.SR
| _ => match right.1 with
| .SL => SigState.SL
| _ => SigState.None
match incoming with
| .SR => if m' == .M2 then .SL else .SR -- bounce off mirror
| .SL => if u then .SR else .SL -- bounce at unit cell
| .None => .None
(s', m', u)Embed: none ↦ (.None, .None, false), some () ↦ (.SR, .M1, true).
Lean code used to test:
def trace_p0_proj (t : ℕ) : Bool :=
exp_ca'.project (exp_ca'.nextt (⦋⟬([()] : Word Unit)⟭⦌) t 0)
#eval! (List.range 8).map trace_p0_projOutput:
[true, false, true, false, false, false, true, false]
And individual time checks:
#eval! trace_p0_proj 14 -- true
#eval! trace_p0_proj 13 -- false
#eval! trace_p0_proj 15 -- falseRan with:
$ cd /workspaces/lean-cellular-automata && timeout 120 lake build ./CellularAutomatas/proofs/exp_word_length_rt2.lean 2>&1 | grep "^info:"
info: .../exp_word_length_rt2.lean:204:0: [true, false, true, false, false, false, true, false]
info: .../exp_word_length_rt2.lean:205:0: true
info: .../exp_word_length_rt2.lean:206:0: false
info: .../exp_word_length_rt2.lean:207:0: false
Signal at p=0 at times: t = 0, 2, 6, 14 — matches b(k) = 2^(k+1) - 2 exactly.
The CA only works correctly for input [Unit] (length 1). For longer words like [(),(),()], every cell gets (.SR, .M1, true), creating 3 signals and 3 mirrors — chaos. This is by design: the construction only needs to handle the single-cell case. Composition with "prepend [()]" and k-step speedup will handle arbitrary word lengths.
What works:
- CA definition with 3×4×2 = 24 states
- Mirror moves at speed 1/3, independent of signal
- Signal bounces between p=0 (is_unit) and M2
- Computationally verified: signal at p=0 at t ∈ {0, 2, 6, 14, ...} = {2^(k+1) − 2}
Lemma structure (all sorry'd):
- Mirror invariant (pure induction on t, no S)
- Phase arithmetic (bounce_time, collision_time relations)
- No-spurious-bounce (positions coincide only at intended bounce point)
- Signal invariant (combines above)
Still needed:
- Fill in sorry proofs
- Composition with "write [Unit]" construction + k-step speedup
- Final theorem connecting to CA_rt