neutralCommute
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.