modally_equivalent
Two configurations are modally equivalent when their recognition values coincide and their integer time coordinates differ by less than one tick. Modal geometry work in Recognition Science cites this to define discrete equivalence classes over possibility space. The definition is realized directly as the conjunction of value equality with the pair of strict inequalities on the time difference.
claimTwo configurations $c_1$ and $c_2$ are modally equivalent if $c_1.value = c_2.value$ and $|c_1.time - c_2.time| < 1$, where time is an integer coordinate in ticks.
background
The ModalGeometry module works over configurations drawn from Possibility.Config, which represents a point in recognition state space. The structure supplies a positive real value (generalizing bond multiplier) together with an integer time coordinate in ticks; its doc-comment states that 'A configuration is a point in recognition state space. In the full theory, this would be a LedgerState. Here we use a simplified representation for modal logic development.'
proof idea
This is a definition whose body is the explicit predicate: value equality conjoined with the two strict inequalities ensuring the absolute time difference is less than one tick. No lemmas or tactics are invoked; the conjunction directly encodes the condition on the Config fields.
why it matters in Recognition Science
The definition supplies the base relation used to establish reflexivity and symmetry in the same module and is invoked in the Modal Nyquist Theorem, which asserts that the universe cannot distinguish possibilities finer than one tick. It supplies the modal counterpart to Nyquist sampling and Heisenberg uncertainty while respecting the discrete tick structure of the Recognition Science framework.
scope and limits
- Does not claim that modally equivalent configurations are physically identical.
- Does not apply outside integer tick coordinates.
- Does not incorporate the positivity constraint on value into the equivalence predicate.
- Does not extend to continuous time or non-discrete models.
Lean usage
example (c1 c2 : Config) (h : modally_equivalent c1 c2) : c1.value = c2.value := by simp [modally_equivalent] at h; exact h.1formal statement (Lean)
142def modally_equivalent (c1 c2 : Config) : Prop :=
proof body
Definition body.
143 c1.value = c2.value ∧ (c1.time : ℤ) - (c2.time : ℤ) < 1 ∧ (c2.time : ℤ) - (c1.time : ℤ) < 1
144
145/-- Modal equivalence is reflexive. -/