neutralCommute
This definition supplies a Boolean predicate on pairs of ribbon syllables that returns true exactly when their starting ticks differ. It would be referenced in constructions of ledger factorizations or syllable words that require non-degenerate swaps to preserve additivity. The declaration is a direct one-line field extraction and inequality test on the Ribbon structure.
claimFor ribbon syllables $a$ and $b$, each equipped with a starting tick on the eight-tick clock, the predicate holds if and only if the starting ticks of $a$ and $b$ are distinct.
background
Ribbon syllables are defined by the structure consisting of a start tick, a direction flag, an integer bit intended to be ±1, and a gauge tag. The module records φ-ladder ribbon machinery as a narrative scaffold; RS derivations are not yet formalised and downstream code treats the contents as demo inputs categorised as Model. Upstream structures supply nuclear densities in discrete φ-tiers and ledger factorisation calibrated to the J-cost function.
proof idea
The declaration is a direct definition that extracts the start field from each input ribbon and returns the Boolean result of their inequality test. No lemmas or tactics are invoked.
why it matters in Recognition Science
The predicate supports non-degenerate commutation in the mass-ribbon model by excluding swaps that share the same starting tick. No parent theorems are recorded in the current dependency graph. It touches the open question of formalising the φ-ladder derivations, currently left as a model scaffold in the Masses domain.
scope and limits
- Does not assert preservation of ledger additivity under swaps.
- Does not encode winding-number rules for ribbon sequences.
- Does not constrain the direction or gauge-tag fields.
- Does not define composition or normal-form reduction for words.
formal statement (Lean)
52@[simp] def neutralCommute (a b : Ribbon) : Bool := a.start ≠ b.start
proof body
Definition body.
53
54/-- A word is a list of ribbon syllables. -/