/machines/1RB0LD_0RC1RA_1LD1RC_1LE0RF_---1LA_1LF0LA/LocalEntrance.v · raw
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(** Exact finite entrance from blank tape for line 593.
    This is a finite reachability theorem, not a halting classification.
    The 85-cell replay window is anchored at coordinates [-32,52].
    AI assistance: GPT-6 Astra (OpenAI). *)
From BusyCoq Require Import Individual62.
From AstraWindow Require Import WindowChecker.
From AstraLocal Require Import LocalRules.
Require Import List ZArith.
Import BoundedConfig.
Open Scope list.

(** Residual word w, ASCII SHA256:
    91a32a80878536b121a4453bb90f82e0973b686106fb9108713b3d133e78b5ec. *)
Definition entrance_word : list Sym := [1;1;1;0;0;1;1;1;1;0;1;1;0;0;1;1;1;0;1;1;1;0;1;1;1;0;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1;1;0;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1;0;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;1;1].
Definition entrance_start : T :=
  Build_T (repeat 0 32) (repeat 0 53) A R.
Definition entrance_finish : T :=
  Build_T ([0;1;1] ++ entrance_word) [0] A L.
Definition entrance_seed : Q * tape :=
  0inf {{A}}> [0;0;1;1] *> entrance_word *> 0inf.

Lemma entrance_word_length : List.length entrance_word = 81%nat.
Proof. reflexivity. Qed.

Lemma entrance_compute_5104 :
  run_window tm 5104 entrance_start = Some entrance_finish.
Proof. vm_compute. reflexivity. Qed.

Theorem entrance_window_5104 l0 r0 :
  to_config entrance_start l0 r0 -[tm]->> 5104 /
  to_config entrance_finish l0 r0.
Proof. apply run_window_sound. exact entrance_compute_5104. Qed.

Lemma entrance_start_blank : to_config entrance_start 0inf 0inf = c0.
Proof. solve_const0_eq. Qed.

Lemma entrance_finish_blank :
  to_config entrance_finish 0inf 0inf = entrance_seed.
Proof. reflexivity. Qed.

Theorem blank_entrance_5104 : c0 -[tm]->> 5104 / entrance_seed.
Proof.
  rewrite <- entrance_start_blank, <- entrance_finish_blank.
  apply entrance_window_5104.
Qed.

(** Index of the scanned cell in a left-to-right finite window.
    Left-facing ahead cells are stored nearest-first; when ahead is empty
    the head is just outside the left boundary, at index -1. *)
Definition entrance_window_head_index (x : T) : Z :=
  match x with
  | Build_T behind ahead _ R => Z.of_nat (List.length behind)
  | Build_T behind ahead _ L => (Z.of_nat (List.length ahead) - 1)%Z
  end.

Lemma entrance_window_coordinates :
  window_size entrance_start = 85%nat /\
  window_size entrance_finish = 85%nat /\
  (-32 + entrance_window_head_index entrance_start = 0)%Z /\
  (-32 + entrance_window_head_index entrance_finish = -32)%Z.
Proof. repeat split; reflexivity. Qed.

Print Assumptions entrance_compute_5104.
Print Assumptions entrance_window_5104.
Print Assumptions blank_entrance_5104.
Print Assumptions entrance_window_coordinates.