pith. machine review for the scientific record. sign in
theorem proved term proof

recognitionStep_iterates_succ

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 140theorem recognitionStep_iterates_succ (step : RecognitionStep) :
 141    step.output.tick = tickSucc step.input.tick := by

proof body

Term-mode proof.

 142  have hadv := step.tick_advance
 143  cases hin : step.input.tick with
 144  | mk i =>
 145    cases hout : step.output.tick with
 146    | mk o =>
 147      rw [hin, hout] at hadv
 148      simp [tickSucc]
 149      exact hadv
 150
 151/-! ## Headline Certificate -/
 152
 153/-- **Time-as-Orbit Certificate.**
 154
 155The temporal sequence is canonically the natural-number object forced by
 156recognition. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.