SimpleTicks
SimpleTicks encodes an alternating tick predicate on boolean states that flips with each increment of the time index. Modelers of minimal recognition graphs cite this definition to satisfy the AtomicTick interface on a two-vertex structure. The definition proceeds by direct functional equality to the parity condition on the time parameter.
claimFor the two-state recognition structure with universe in Bool, the tick predicate is $P(t,v) : Prop$ defined by $P(t,v) := v = (t mod 2 = 1)$.
background
The module presents a minimal two-vertex recognition structure equipped with a bidirectional relation. AtomicTick is the class requiring a postedAt map from Nat to the structure's universe together with the uniqueness axiom that each time step posts to exactly one state. BoundedStep is the class supplying a step relation and a neighbors function whose cardinality is bounded by a fixed degree. This definition supplies the postedAt component realizing the alternating schedule.
proof idea
The definition is a direct lambda that returns the boolean equality between the supplied state and the result of the modulo-2 parity test on the time argument.
why it matters in Recognition Science
This definition populates the postedAt field inside the AtomicTick instance for the simple structure, providing a concrete minimal model of discrete posting. It also supports the subsequent BoundedStep instance on Bool with degree 1. The construction illustrates basic periodicity in a toy recognition graph without invoking the full phi-ladder or forcing chain.
scope and limits
- Does not define the underlying graph edges or the full RecognitionStructure instance.
- Does not prove the uniqueness axiom; that is supplied by the separate instance declaration.
- Does not connect to physical constants, mass formulas, or the phi-ladder.
- Does not extend to structures with more than two states or to continuous time.
formal statement (Lean)
32def SimpleTicks : Nat → Bool → Prop := fun t v => v = (t % 2 == 1)
proof body
Definition body.
33
34instance : AtomicTick SimpleStructure := {
35 postedAt := SimpleTicks,
36 unique_post := by
37 intro t
38 use (t % 2 == 1)
39 constructor
40 · rfl
41 · intro u hu
42 simp [SimpleTicks] at hu
43 exact hu
44}
45
46/-- Example of BoundedStep on Bool with degree 1. -/
47instance : BoundedStep Bool 1 := {
48 step := SimpleStructure.R,
49 neighbors := fun b => if b then {false} else {true},
50 step_iff_mem := by
51 intro a b
52 simp [SimpleStructure]
53 cases a <;> cases b <;> simp
54}
55
56end ModelingExamples
57end IndisputableMonolith