crossing — a product as an assay, on Witness

46 receipts inline · 399 lines · pinned d93c771b80f8d968 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean crossing.lean prints nothing when every receipt passes

import Face
import Witness
open Room Face Witness
set_option autoImplicit false

namespace Crossing

universe w w'

def parts {O : Type} (m m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) (n : Nat) : Bool :=
  !(beq (behavior m (List.replicate n ())) (behavior m' (List.replicate n ())))

/-- info: 'Crossing.parts' does not depend on any axioms -/
#guard_msgs in #print axioms parts

def inStepTo {O : Type} (m m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) : Nat → Bool
  | 0 => beq (behavior m []) (behavior m' [])
  | n + 1 => beq (behavior m (List.replicate (n + 1) ())) (behavior m' (List.replicate (n + 1) ())) && inStepTo m m' beq n

/-- info: 'Crossing.inStepTo' does not depend on any axioms -/
#guard_msgs in #print axioms inStepTo

def firstPart {O : Type} (m m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) (n : Nat) : Nat → Option Nat
  | 0 => none
  | fuel + 1 => cond (parts m m' beq n) (some n) (firstPart m m' beq (n + 1) fuel)

/-- info: 'Crossing.firstPart' does not depend on any axioms -/
#guard_msgs in #print axioms firstPart

def crossingWithin {O : Type} (m m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) (bound : Nat) : Option Nat :=
  firstPart m m' beq 0 bound

/-- info: 'Crossing.crossingWithin' does not depend on any axioms -/
#guard_msgs in #print axioms crossingWithin

def both {O O' : Type} (m : Machine.{0, 0, w} Unit O) (n : Machine.{0, 0, w'} Unit O') : Machine.{0, 0, max w w'} Unit (O × O') :=
  ⟨m.S × n.S, (m.s0, n.s0), fun s _ => (m.step s.1 (), n.step s.2 ()), fun s => (m.out s.1, n.out s.2)⟩

/-- info: 'Crossing.both' does not depend on any axioms -/
#guard_msgs in #print axioms both

def bothBeq {O O' : Type} (beq : O → O → Bool) (beq' : O' → O' → Bool) (a b : O × O') : Bool :=
  beq a.1 b.1 && beq' a.2 b.2

/-- info: 'Crossing.bothBeq' does not depend on any axioms -/
#guard_msgs in #print axioms bothBeq

def ones : Machine Unit Nat := retune (fun _ => 1) adder

/-- info: 'Crossing.ones' does not depend on any axioms -/
#guard_msgs in #print axioms ones

def onesTaped : Machine Unit Nat := retune (fun _ => 1) (tape adder (0 : Nat) recordTheState readThrough)

/-- info: 'Crossing.onesTaped' does not depend on any axioms -/
#guard_msgs in #print axioms onesTaped

def onesTended : Machine Unit Nat := retune (fun _ => 1) (tend adder (0 : Nat) recordTheState)

/-- info: 'Crossing.onesTended' does not depend on any axioms -/
#guard_msgs in #print axioms onesTended

def crossingOfTheTape : Option Nat := crossingWithin onesTaped ones Nat.beq 10

/-- info: 'Crossing.crossingOfTheTape' does not depend on any axioms -/
#guard_msgs in #print axioms crossingOfTheTape

def crossingOfTheTending : Option Nat := crossingWithin onesTended ones Nat.beq 10

/-- info: 'Crossing.crossingOfTheTending' does not depend on any axioms -/
#guard_msgs in #print axioms crossingOfTheTending

def crossingOfTheVoice : Option Nat := crossingWithin (revoice oddNat onesTaped) (revoice oddNat ones) (fun a b => a == b) 10

/-- info: 'Crossing.crossingOfTheVoice' does not depend on any axioms -/
#guard_msgs in #print axioms crossingOfTheVoice

def crossingBesideTheTally : Option Nat := crossingWithin (both tally onesTaped) (both tally ones) (bothBeq Nat.beq Nat.beq) 10

/-- info: 'Crossing.crossingBesideTheTally' does not depend on any axioms -/
#guard_msgs in #print axioms crossingBesideTheTally

def crossingOfTheTallyBeside : Option Nat := crossingWithin (both onesTaped tally) (both ones tally) (bothBeq Nat.beq Nat.beq) 10

/-- info: 'Crossing.crossingOfTheTallyBeside' does not depend on any axioms -/
#guard_msgs in #print axioms crossingOfTheTallyBeside

def crossingAtTheWiden : Option Nat := crossingWithin (both onesTaped (retune (fun _ => 1) (revoice (fun _ => (1 : Nat)) adder))) (both ones (retune (fun _ => 1) (revoice (fun _ => (0 : Nat)) adder))) (bothBeq Nat.beq Nat.beq) 10

#guard inStepTo onesTaped ones Nat.beq 2 == true
#guard parts onesTaped ones Nat.beq 3 == true
#guard crossingOfTheTape == some 3
#guard crossingOfTheTending == none
#guard crossingOfTheVoice == some 3
#guard crossingBesideTheTally == some 3
#guard crossingOfTheTallyBeside == some 3
#guard crossingAtTheWiden == some 0

/-- info: 'Crossing.crossingAtTheWiden' does not depend on any axioms -/
#guard_msgs in #print axioms crossingAtTheWiden

def ticks (n : Nat) : List (List Unit) := (List.range n).map (fun i => List.replicate i ())

/-- info: 'Crossing.ticks' does not depend on any axioms -/
#guard_msgs in #print axioms ticks

def window {O : Type} (outs : List O) (i k : Nat) : List O := (outs.drop i).take k

/-- info: 'Crossing.window' does not depend on any axioms -/
#guard_msgs in #print axioms window

def listBeq {O : Type} (beq : O → O → Bool) : List O → List O → Bool
  | [], [] => true
  | [], _ :: _ => false
  | _ :: _, [] => false
  | a :: as, b :: bs => beq a b && listBeq beq as bs

/-- info: 'Crossing.listBeq' does not depend on any axioms -/
#guard_msgs in #print axioms listBeq

def pagesOf {O : Type} (beq : O → O → Bool) (outs : List O) (k : Nat) : Nat :=
  fresh (listBeq beq) ((List.range k).map (fun i => window outs i k))

/-- info: 'Crossing.pagesOf' does not depend on any axioms -/
#guard_msgs in #print axioms pagesOf

def pagesWithin {O : Type} (m : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) (k : Nat) : Nat :=
  pagesOf beq (reads (airGap Unit O) (ticks (k + k)) m) k

/-- info: 'Crossing.pagesWithin' does not depend on any axioms -/
#guard_msgs in #print axioms pagesWithin

def stillOne : Machine Unit Nat := ⟨Unit, (), fun _ _ => (), fun _ => 1⟩

/-- info: 'Crossing.stillOne' does not depend on any axioms -/
#guard_msgs in #print axioms stillOne

def mod3 : Machine Unit Nat := ⟨Nat, 0, fun s _ => (s + 1) % 3, fun s => s⟩

/-- info: 'Crossing.mod3' does not depend on any axioms -/
#guard_msgs in #print axioms mod3

def boolBeq (a b : Bool) : Bool := a == b

#guard pagesWithin stillOne Nat.beq 5 == 1
#guard pagesWithin flip boolBeq 4 == 2
#guard pagesWithin paceOne boolBeq 4 == 2
#guard pagesWithin tally Nat.beq 4 == 4
#guard pagesWithin tally Nat.beq 7 == 7
#guard pagesWithin mod3 Nat.beq 6 == 3
#guard pagesWithin (both flip mod3) (bothBeq boolBeq Nat.beq) 12 == 6
#guard pagesWithin (both mod3 mod3) (bothBeq Nat.beq Nat.beq) 12 == 3
#guard pagesWithin (both flip paceOne) (bothBeq boolBeq boolBeq) 6 == 2
#guard pagesWithin onesTaped Nat.beq 6 == 6

/-- info: 'Crossing.boolBeq' does not depend on any axioms -/
#guard_msgs in #print axioms boolBeq

def shifted {O : Type} (m : Machine.{0, 0, w} Unit O) (k : Nat) : Machine.{0, 0, w} Unit O :=
  ⟨m.S, park m m.s0 (List.replicate k ()), m.step, m.out⟩

/-- info: 'Crossing.shifted' does not depend on any axioms -/
#guard_msgs in #print axioms shifted

def windingWithin {O : Type} (m : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) (bound : Nat) : Option Nat :=
  firstOf' m beq 1 bound
where
  firstOf' (m : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) : Nat → Nat → Option Nat
    | _, 0 => none
    | k, fuel + 1 => cond (inStepTo m (shifted m k) beq bound) (some k) (firstOf' m beq (k + 1) fuel)

#guard crossingWithin mod3 (shifted mod3 3) Nat.beq 10 == none
#guard crossingWithin mod3 (shifted mod3 1) Nat.beq 10 == some 0
#guard crossingWithin flip (shifted flip 2) boolBeq 10 == none
#guard crossingWithin flip (shifted flip 1) boolBeq 10 == some 0
#guard crossingWithin stillOne (shifted stillOne 1) Nat.beq 10 == none
#guard crossingWithin tally (shifted tally 1) Nat.beq 10 == some 0
#guard windingWithin mod3 Nat.beq 10 == some 3
#guard windingWithin flip boolBeq 10 == some 2
#guard windingWithin stillOne Nat.beq 10 == some 1
#guard windingWithin tally Nat.beq 10 == none
#guard windingWithin (both flip mod3) (bothBeq boolBeq Nat.beq) 10 == some 6
#guard windingWithin mod3 Nat.beq 10 == some (pagesWithin mod3 Nat.beq 6)

/-- info: 'Crossing.windingWithin' does not depend on any axioms -/
#guard_msgs in #print axioms windingWithin

def lapsOf (k : Nat) : List Nat := met (park (remembering mod3) (atTheDoor (0 : Nat) ([] : List Nat)) (List.replicate (k * 3) ()))

/-- info: 'Crossing.lapsOf' does not depend on any axioms -/
#guard_msgs in #print axioms lapsOf

def onePage : List Nat := [2, 1, 0]

#guard lapsOf 1 == onePage
#guard lapsOf 2 == joinMap (fun _ => onePage) (List.replicate 2 ())
#guard lapsOf 4 == joinMap (fun _ => onePage) (List.replicate 4 ())

/-- info: 'Crossing.onePage' does not depend on any axioms -/
#guard_msgs in #print axioms onePage

def lapEnd : Nat := face (park (remembering mod3) (atTheDoor (0 : Nat) ([] : List Nat)) (List.replicate 12 ()))
#guard lapEnd == 0

/-- info: 'Crossing.lapEnd' does not depend on any axioms -/
#guard_msgs in #print axioms lapEnd

theorem a_clock_alike_at_the_gap_never_parts {O : Type} (m m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool)
    (hrefl : ∀ o, beq o o = true) (h : alike (airGap Unit O) m m') (n : Nat) : parts m m' beq n = false := by
  have e : behavior m (List.replicate n ()) = behavior m' (List.replicate n ()) := h (List.replicate n ())
  show (!(beq (behavior m (List.replicate n ())) (behavior m' (List.replicate n ())))) = false
  rw [e, hrefl]
  rfl

/-- info: 'Crossing.a_clock_alike_at_the_gap_never_parts' does not depend on any axioms -/
#guard_msgs in #print axioms a_clock_alike_at_the_gap_never_parts

theorem the_crossing_is_derived {O : Type} (m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool) (n : Nat) :
    Derived (airGap Unit O) (fun m : Machine.{0, 0, w} Unit O => parts m m' beq n = true) :=
  a_role_read_at_a_probe_is_derived (airGap Unit O) (List.replicate n ())
    (fun o => (!(beq o (behavior m' (List.replicate n ())))) = true)

/-- info: 'Crossing.the_crossing_is_derived' does not depend on any axioms -/
#guard_msgs in #print axioms the_crossing_is_derived

theorem the_tending_never_parts {O : Type} {W : Type} (m : Machine.{0, 0, w} Unit O) (w0 : W) (σ : door m.S W → W)
    (beq : O → O → Bool) (hrefl : ∀ o, beq o o = true) (n : Nat) : parts (tend m w0 σ) m beq n = false := by
  have e : behavior (tend m w0 σ) (List.replicate n ()) = behavior m (List.replicate n ()) :=
    the_tending_is_unheard_at_the_gap m w0 σ (List.replicate n ())
  show (!(beq (behavior (tend m w0 σ) (List.replicate n ())) (behavior m (List.replicate n ())))) = false
  rw [e, hrefl]
  rfl

/-- info: 'Crossing.the_tending_never_parts' does not depend on any axioms -/
#guard_msgs in #print axioms the_tending_never_parts

theorem the_pair_walks_both {O O' : Type} (m : Machine.{0, 0, w} Unit O) (n : Machine.{0, 0, w'} Unit O') :
    ∀ (u : List Unit) (s : m.S) (t : n.S), park (both m n) (s, t) u = (park m s u, park n t u) :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _ _)))

/-- info: 'Crossing.the_pair_walks_both' does not depend on any axioms -/
#guard_msgs in #print axioms the_pair_walks_both

theorem a_voice_parts_no_sooner {O O' : Type} (g : O → O') (m m' : Machine.{0, 0, w} Unit O)
    (beq : O → O → Bool) (beq' : O' → O' → Bool) (hg : ∀ a b, beq a b = true → beq' (g a) (g b) = true) (n : Nat)
    (h : parts (revoice g m) (revoice g m') beq' n = true) : parts m m' beq n = true := by
  have e1 : behavior (revoice g m) (List.replicate n ()) = g (behavior m (List.replicate n ())) :=
    congrArg (revoice g m).out (the_revoice_moves_no_seat g m (List.replicate n ()) m.s0)
  have e2 : behavior (revoice g m') (List.replicate n ()) = g (behavior m' (List.replicate n ())) :=
    congrArg (revoice g m').out (the_revoice_moves_no_seat g m' (List.replicate n ()) m'.s0)
  have h' : (!(beq' (g (behavior m (List.replicate n ()))) (g (behavior m' (List.replicate n ()))))) = true := by
    have h0 : (!(beq' (behavior (revoice g m) (List.replicate n ())) (behavior (revoice g m') (List.replicate n ())))) = true := h
    rw [e1, e2] at h0
    exact h0
  show (!(beq (behavior m (List.replicate n ())) (behavior m' (List.replicate n ())))) = true
  cases hab : beq (behavior m (List.replicate n ())) (behavior m' (List.replicate n ())) with
  | true => rw [hg _ _ hab] at h'; exact nomatch h'
  | false => rfl

/-- info: 'Crossing.a_voice_parts_no_sooner' does not depend on any axioms -/
#guard_msgs in #print axioms a_voice_parts_no_sooner

theorem the_read_tape_crosses_at_three :
    inStepTo onesTaped ones Nat.beq 2 = true ∧ parts onesTaped ones Nat.beq 3 = true
      ∧ crossingWithin onesTaped ones Nat.beq 10 = some 3 ∧ crossingWithin onesTended ones Nat.beq 10 = none :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Crossing.the_read_tape_crosses_at_three' does not depend on any axioms -/
#guard_msgs in #print axioms the_read_tape_crosses_at_three

theorem the_pages_are_derived {O : Type} (beq : O → O → Bool) (k v : Nat) :
    Derived (airGap Unit O) (fun m : Machine.{0, 0, w} Unit O => pagesWithin m beq k = v) :=
  by
    (intro x; induction x;
      all_goals
        ((rename_i ih; intros;
            (try
                dsimp only [pagesOf, ticks, Face.Derived, Witness.a_seat_over_a_seat_is_derived, Face.airGap, pagesWithin,
                  Face.Machine] at *);
            (rw [Witness.the_alike_read_alike]; assumption))))

/-- info: 'Crossing.the_pages_are_derived' does not depend on any axioms -/
#guard_msgs in #print axioms the_pages_are_derived

theorem a_decomposition_costs_the_same {O : Type} (m m' : Machine.{0, 0, w} Unit O) (beq : O → O → Bool)
    (h : alike (airGap Unit O) m m') (k : Nat) : pagesWithin m beq k = pagesWithin m' beq k :=
  congrArg (fun outs => pagesOf beq outs k) (the_alike_read_alike (airGap Unit O) h (ticks (k + k)))

/-- info: 'Crossing.a_decomposition_costs_the_same' does not depend on any axioms -/
#guard_msgs in #print axioms a_decomposition_costs_the_same

theorem the_pace_is_the_flip_at_the_gap : alike (airGap Unit Bool) paceOne flip :=
  fun w => (the_pace_is_carried_onto_the_flip (0 : Nat) w).symm

/-- info: 'Crossing.the_pace_is_the_flip_at_the_gap' does not depend on any axioms -/
#guard_msgs in #print axioms the_pace_is_the_flip_at_the_gap

theorem the_still_clock_has_one_page_at_every_depth :
    pagesWithin stillOne Nat.beq 1 = 1 ∧ pagesWithin stillOne Nat.beq 3 = 1 ∧ pagesWithin stillOne Nat.beq 5 = 1 :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Crossing.the_still_clock_has_one_page_at_every_depth' does not depend on any axioms -/
#guard_msgs in #print axioms the_still_clock_has_one_page_at_every_depth

theorem a_pair_costs_at_most_the_product_at_twelve :
    Nat.ble (pagesWithin (both flip mod3) (bothBeq boolBeq Nat.beq) 12) (pagesWithin flip boolBeq 12 * pagesWithin mod3 Nat.beq 12) = true
      ∧ Nat.ble (pagesWithin (both mod3 mod3) (bothBeq Nat.beq Nat.beq) 12) (pagesWithin mod3 Nat.beq 12 * pagesWithin mod3 Nat.beq 12) = true
      ∧ Nat.ble (pagesWithin (both flip paceOne) (bothBeq boolBeq boolBeq) 6) (pagesWithin flip boolBeq 6 * pagesWithin paceOne boolBeq 6) = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Crossing.a_pair_costs_at_most_the_product_at_twelve' does not depend on any axioms -/
#guard_msgs in #print axioms a_pair_costs_at_most_the_product_at_twelve

theorem more_depth_reads_no_fewer_pages_for_the_flip_and_the_tally :
    Nat.ble (pagesWithin flip boolBeq 1) (pagesWithin flip boolBeq 2) = true
      ∧ Nat.ble (pagesWithin flip boolBeq 2) (pagesWithin flip boolBeq 3) = true
      ∧ Nat.ble (pagesWithin mod3 Nat.beq 2) (pagesWithin mod3 Nat.beq 3) = true
      ∧ Nat.ble (pagesWithin mod3 Nat.beq 3) (pagesWithin mod3 Nat.beq 4) = true
      ∧ Nat.ble (pagesWithin tally Nat.beq 4) (pagesWithin tally Nat.beq 5) = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Crossing.more_depth_reads_no_fewer_pages_for_the_flip_and_the_tally' does not depend on any axioms -/
#guard_msgs in #print axioms more_depth_reads_no_fewer_pages_for_the_flip_and_the_tally

theorem the_shift_walks_the_same {O : Type} (m : Machine.{0, 0, w} Unit O) (p : Nat) :
    ∀ (u : List Unit) (s : m.S), park (shifted m p) s u = park m s u :=
  by
    (intro x; induction x;
      all_goals
        (first
          | (intros; rfl)
          | (rename_i ih; intros; exact ih _)))

/-- info: 'Crossing.the_shift_walks_the_same' does not depend on any axioms -/
#guard_msgs in #print axioms the_shift_walks_the_same

theorem the_winding_is_the_crossing_with_the_shift :
    windingWithin mod3 Nat.beq 10 = some 3 ∧ crossingWithin mod3 (shifted mod3 3) Nat.beq 10 = none
      ∧ crossingWithin mod3 (shifted mod3 2) Nat.beq 10 = some 0
      ∧ windingWithin (both flip mod3) (bothBeq boolBeq Nat.beq) 10 = some 6 :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Crossing.the_winding_is_the_crossing_with_the_shift' does not depend on any axioms -/
#guard_msgs in #print axioms the_winding_is_the_crossing_with_the_shift

theorem the_holonomy_of_a_closed_route_is_its_winding :
    lapsOf 2 = joinMap (fun _ => onePage) (List.replicate 2 ()) ∧ lapsOf 4 = joinMap (fun _ => onePage) (List.replicate 4 ())
      ∧ (lapsOf 4).length = 4 * (windingWithin mod3 Nat.beq 10).getD 0 :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Crossing.the_holonomy_of_a_closed_route_is_its_winding' does not depend on any axioms -/
#guard_msgs in #print axioms the_holonomy_of_a_closed_route_is_its_winding

theorem a_pair_parts_when_either_does {O O' : Type} (m m' : Machine.{0, 0, w} Unit O) (n n' : Machine.{0, 0, w'} Unit O')
    (beq : O → O → Bool) (beq' : O' → O' → Bool) (k : Nat) :
    parts (both m n) (both m' n') (bothBeq beq beq') k = (parts m m' beq k || parts n n' beq' k) := by
  have e1 : behavior (both m n) (List.replicate k ()) = (behavior m (List.replicate k ()), behavior n (List.replicate k ())) :=
    congrArg (both m n).out (the_pair_walks_both m n (List.replicate k ()) m.s0 n.s0)
  have e2 : behavior (both m' n') (List.replicate k ()) = (behavior m' (List.replicate k ()), behavior n' (List.replicate k ())) :=
    congrArg (both m' n').out (the_pair_walks_both m' n' (List.replicate k ()) m'.s0 n'.s0)
  show (!(bothBeq beq beq' (behavior (both m n) (List.replicate k ())) (behavior (both m' n') (List.replicate k ()))))
    = ((!(beq (behavior m (List.replicate k ())) (behavior m' (List.replicate k ()))))
        || (!(beq' (behavior n (List.replicate k ())) (behavior n' (List.replicate k ())))))
  rw [e1, e2]
  show (!(beq (behavior m (List.replicate k ())) (behavior m' (List.replicate k ()))
          && beq' (behavior n (List.replicate k ())) (behavior n' (List.replicate k ()))))
    = ((!(beq (behavior m (List.replicate k ())) (behavior m' (List.replicate k ()))))
        || (!(beq' (behavior n (List.replicate k ())) (behavior n' (List.replicate k ())))))
  cases beq (behavior m (List.replicate k ())) (behavior m' (List.replicate k ())) <;>
    cases beq' (behavior n (List.replicate k ())) (behavior n' (List.replicate k ())) <;> rfl

/-- info: 'Crossing.a_pair_parts_when_either_does' does not depend on any axioms -/
#guard_msgs in #print axioms a_pair_parts_when_either_does

theorem the_pace_costs_what_the_flip_costs (k : Nat) : pagesWithin paceOne boolBeq k = pagesWithin flip boolBeq k :=
  (by (apply a_decomposition_costs_the_same <;> (apply the_pace_is_the_flip_at_the_gap <;> fail)))

/-- info: 'Crossing.the_pace_costs_what_the_flip_costs' does not depend on any axioms -/
#guard_msgs in #print axioms the_pace_costs_what_the_flip_costs

theorem a_clock_never_parts_from_its_own_return {O : Type} (m : Machine.{0, 0, w} Unit O) (beq : O → O → Bool)
    (hrefl : ∀ o, beq o o = true) (p : Nat) (hp : park m m.s0 (List.replicate p ()) = m.s0) (n : Nat) :
    parts m (shifted m p) beq n = false := by
  have e : behavior (shifted m p) (List.replicate n ()) = behavior m (List.replicate n ()) := by
    show m.out (park (shifted m p) (park m m.s0 (List.replicate p ())) (List.replicate n ())) = m.out (park m m.s0 (List.replicate n ()))
    rw [the_shift_walks_the_same, hp]
  show (!(beq (behavior m (List.replicate n ())) (behavior (shifted m p) (List.replicate n ())))) = false
  rw [e, hrefl]
  rfl

/-- info: 'Crossing.a_clock_never_parts_from_its_own_return' does not depend on any axioms -/
#guard_msgs in #print axioms a_clock_never_parts_from_its_own_return

end Crossing

the vestibule — what the assay would say and cannot yet, each with what it waits on (assays/crossing.held); a stranger could answer one

a hand for the count — a window of a pair is a pair of windows, so distinct pairs are at most the -- product; and more depth reads no fewer pages, the monotonicity that makes the count a plan's reading
a finite family of taps; the clerks of a route as a list

-- the vestibule of the crossing number: what the assay would say about co-existence and cannot yet, each a
-- statement in the assay's own terms and the darkness it waits on. read by bin/counter book. the assay measures
-- distance (the parting fuel: the least tick at which two clocks part at the air gap); isaac's question (2026-09-29,
-- the evening) was cost — how costly it is to co-exist with one clock versus another, with regression in terms —
-- and the annals answer in three places, each a count and none yet a row here.

-- the width of contact (the birth-to-between eras, Plateau's laws read as the minimum structure that supports
-- co-existence: one observer inert, two tension without resolution, three stable junctions; in the house now
-- three_is_the_width_of_contact and the_hallway_is_too_small): co-existence has a count before any clock does,
-- the number of seats a junction needs. nothing waits on it; it is a citation the assay could make and does not.

-- the pages (foamcore~1, Foam/Bridges/Kolmogorov.lean: rest_compresses_time_away — at rest the reel over any k
-- ticks reads as one page; motion_refuses_the_page — a moving world needs more than one; in the house now
-- a_still_runner_rests_where_it_stands and the_still_plan_is_readable_iff_at_rest): the cost of co-existing with
-- a clock is the count of its pages — the distinct sheets (liftFrom) on its orbit, which is the size of the least
-- carrier of its behavior and not of its room. one at rest; two for flip and for paceOne alike, though paceOne's
-- room is infinite (the_pace_is_carried_onto_the_flip: the count is the carrier's); none for the tally. a
-- combination of clocks costs at most the product and, for coprime periods, the least common period; the
-- difference from the product room is the dark states never visited, the unread remainder as a count. this is
-- the dual of the parting fuel — not when two clocks part but how much a seat carries to keep in step — and it
-- regresses in terms for the same reason the crossing number does: a function of the behavior, so every
-- unheard rebody has the same count. waiting on: a carrier for the count of distinct sheets on an orbit — a
-- period, or a bound within which the count is read (the sheets are infinite objects; a page is a sheet read to
-- a depth), and the row that a clock and its decomposition into clocks have one count.
-- seated the same evening (isaac: move freely): the fork was not one — a bound is the reader's fuel, the count at a
-- depth is a reading at that fuel, and the house had already typed that shape in Rest (a plan is read by whoever
-- supplies the fuel). `pagesWithin m beq k` is the count of distinct windows of depth k over the first k ticks of
-- the clock's readings at the air gap; the_pages_are_derived is a_seat_over_a_seat_is_derived at that seat, and
-- a_decomposition_costs_the_same its corollary through the_alike_read_alike; the pace costs what the flip costs
-- by citation. the rows: one at rest, two for flip and paceOne, none for the tally (k at every k), three for a
-- clock mod three, six for flip beside mod three, three for mod three beside itself (the product room is nine;
-- the six dark states are the unread remainder as a count), two for flip beside the pace, and six for the read
-- tape (a counter in another coat). what still waits, the laws about the count itself:
-- and the laws about the count itself are seated at the assay's own clocks (the same evening; isaac: have you read
-- assays/everyoneishere.lean? — the product states its walls at the demo and cites the trunk once, and that is the
-- easier path): the still clock has one page at every depth, a pair costs at most the product (flip beside mod
-- three, mod three beside itself, flip beside the pace), more depth reads no fewer pages (flip, mod three, the
-- tally) — three instance rows, each regrown by constructor. what still waits is the general law, and the house's
-- rule says where it goes: a species is deposited in the trunk the day two products need it, and the second
-- product is already standing. everyoneishere's `uniq` is `fresh`'s list (the same recursion; fresh is its
-- length), its parties are the pages of ✦ Guests (a seat hearing ✦ Guests whole reads the party once: two guests
-- of one party are one probe, seatOf demoTwo 39 == seatOf demoTwo 38), and its head is the cost of co-existing
-- with a room — the whole tape, the same for every standing, a counter's pages being its cells — with the inbox
-- what a seat reads of it and the difference the dark cells as a count. so the deposit is a Room species, a
-- cold pass for the house, paid and never weighed, on the day it is made:
-- the deposit was made (2026-09-30, under free witness): `uniq` and `fresh` are Room species now, with
-- fresh_counts_the_uniq, fresh_at_most_the_length, and fresh_of_the_alike_is_one — the three laws that fit a sitting,
-- each a hand induction. the two below are counting arguments over distinct windows and stay held as what they are.
-- held (waiting on: a hand for the count — a window of a pair is a pair of windows, so distinct pairs are at most the
-- product; and more depth reads no fewer pages, the monotonicity that makes the count a plan's reading)
-- theorem a_pair_costs_at_most_the_product {O O' : Type} (m : Machine Unit O) (n : Machine Unit O') (beq beq') (k : Nat) :
--     Nat.ble (pagesWithin (both m n) (bothBeq beq beq') k) (pagesWithin m beq k * pagesWithin n beq' k) = true := sorry
-- theorem more_depth_reads_no_fewer_pages {O : Type} (m : Machine Unit O) (beq : O → O → Bool) (k : Nat) :
--     Nat.ble (pagesWithin m beq k) (pagesWithin m beq (k + 1)) = true := sorry

-- the bill upstairs (foamcore~1, Foam/Bridges/Landauer.lean: the_bill_moves_upstairs — two maintenance sequences
-- of different length agree at the front and differ at the back, the debt outliving its legibility; in the
-- house now the_records_part_the_seats and a_wider_seat_reads_the_remainder): the cost of co-existence is a
-- count read one seat wider — the length of the carried record, unread at the host and real at the widen. the
-- replay runner carries the whole word; the counter carrying a unit carries one more cell than the counter; the
-- page count above is the least such record. waiting on: the same carrier, read at the widen.

-- knot theory, crossed with reversible computation as the measurement an observer is already doing (isaac,
-- 2026-09-30): the knot is W's alike-class at the widest seat, never formed as a term — knot theory takes the
-- quotient by isotopy and the house refuses it, so a conductive knot theory has diagrams (seats), Reidemeister
-- moves (unheard rebodies), invariants (Derived readings), and the knot only as a license between two diagrams.
-- the three counts are three invariants of one worldline: winding is self-linking (the crossing with the shifted
-- copy, seated above), crossing per tap is seated, and the knot-theoretic crossing number is the MINIMUM over
-- seats — a reading of the class without forming it, Derived by construction. the unknotting number is refused:
-- a crossing change passes one strand through another, a cut, the resistor; what the house has instead is the
-- blocking number, the loops made because one may not cut. waiting on: a finite family of taps to take the
-- minimum over (ρ ranges over a function space; the row wants a list), and the count of resistors in a route
-- as the knottedness of its record.
-- held (waiting on: a finite family of taps; the clerks of a route as a list)
-- theorem the_crossing_number_is_the_least_over_seats {O : Type} (m : Machine Unit O) (beq : O → O → Bool) (taps : List (W → Unit → Unit)) :
--     crossingNumber m beq taps = leastOf ((taps.map (fun ρ => crossingWithin (tape m w0 σ ρ) m beq bound))) := sorry
-- theorem a_conductive_route_is_the_unknot (route : List (S → S)) (h : ∀ f, f ∈ route → ∃ r, ∀ s, r (f s) = s) :
--     knottedness route = 0 := sorry

crossing — a product as an assay, on Witness

the vestibule — what the assay would say and cannot yet, each with what it waits on (assays/crossing.held); a stranger could answer one

the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)

the data-model shadow — every structure a table, every seat a view over the columns its probes read, every wall theorem the policy it licenses (bin/counter schema)