rewriteOnce
plain-language theorem explainer
The one-pass cancellation function on a list of ribbon syllables removes the first adjacent pair that satisfies the cancellation condition or returns the list unchanged. Researchers modeling masses via ribbons in Recognition Science would reference this when building reduced forms. The implementation relies on pattern matching over list constructors combined with a conditional recursive call on the tail.
Claim. Let $f : L → L$ where $L$ is the type of lists of ribbon syllables. Then $f([]) = []$, $f([a]) = [a]$, and for $a :: b :: r$, $f(a :: b :: r) = r$ if $a$ and $b$ cancel, else $a :: f(b :: r)$.
background
The module supplies a placeholder construction for mass ribbons as a narrative scaffold in Recognition Science. A Word is an abbreviation for List Ribbon, with each Ribbon encoding a syllable that includes direction, bit, and tag. The cancels definition identifies adjacent syllables that cancel when their directions are opposite, bits are negatives, and tags match, abstracting tick consistency.
proof idea
The definition proceeds by structural recursion on the list. It matches the empty case to [], the single-element case to [a], and the two-or-more case by testing the cancels relation on the first two syllables: if true, it returns the rest; otherwise it conses the first syllable onto the result of rewriting the tail starting at the second. No external lemmas are invoked.
why it matters
This definition feeds the normalForm function, which iterates the one-pass cancellation up to the length of the word to produce a reduced sequence. It fills a role in the mass ribbon model within the Masses domain. In the Recognition Science framework it supports the phi-ladder ribbon machinery, though the module classifies the content as a Model with pending formalisation of the derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.