`next`

definition

show as: view math explainer →

module: IndisputableMonolith.RRF.Hypotheses.EightTick
domain: RRF
line: 63 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RRF.Hypotheses.EightTick on GitHub at line 63.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  60  omega
  61
  62/-- Successor phase (cyclic). -/
  63def next (p : Phase) : Phase := p + 1
  64
  65/-- Predecessor phase (cyclic). -/
  66def prev (p : Phase) : Phase := p - 1
  67
  68theorem next_prev (p : Phase) : (p.next).prev = p := by
  69  simp [next, prev]
  70
  71theorem prev_next (p : Phase) : (p.prev).next = p := by
  72  simp [next, prev]
  73
  74end Phase
  75
  76/-! ## The 8-Tick Hypothesis Class -/
  77
  78/-- An observed trace with tick structure. -/
  79structure TickedTrace (Event : Type*) where
  80  /-- The events in sequence. -/
  81  events : List Event
  82  /-- The phase of each event. -/
  83  phase : Fin events.length → Phase
  84
  85/-- The 8-tick hypothesis for traces.
  86
  87This is the explicit claim that traces exhibit 8-phase structure.
  88-/
  89class EightTickHypothesis (Trace : Type*) where
  90  /-- Extract tick information from a trace. -/
  91  ticks : Trace → List Phase
  92  /-- The tick sequence respects the 8-cycle. -/
  93  cyclic : ∀ t : Trace, ∀ i : Nat, ∀ hi : i < (ticks t).length,

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.