cancels
plain-language theorem explainer
The cancels predicate identifies when two ribbon syllables on the eight-tick clock form a neutral pair by requiring opposite directions, opposite bits, and matching gauge tags. Modelers of J-cost cancellation in enzyme catalysis or vacuum energy would reference it when checking additive neutrality in composite words. The definition is a direct Boolean conjunction on the three fields of the Ribbon structure.
Claim. For ribbons $a$ and $b$ on the eight-tick clock, cancels$(a,b)$ holds precisely when the direction of $b$ is the negation of the direction of $a$, the bit of $b$ equals the negative of the bit of $a$, and the gauge tags coincide.
background
The Ribbon structure is a syllable on the eight-tick clock carrying a start tick, Boolean direction, integer bit (intended ±1), and gauge tag. The cancels definition abstracts tick consistency for adjacent syllables in a word, allowing ledger additivity and winding to be preserved under swap. Upstream, the winding definition sums signed directions over a Word, while the for structure from UniversalForcingSelfReference records the structural properties required for meta-realization.
proof idea
The definition is a direct Boolean conjunction on the dir, bit, and tag fields of the Ribbon structure.
why it matters
This predicate supports J-cost cancellation checks that appear in catalyzedBarrier for enzyme reactions and in jcost_cancellation for the cosmological constant, where most vacuum energy cancels leaving a tiny residual. It implements the neutral commutation idea for ribbons and feeds the Recognition Composition Law machinery on the phi-ladder. The module remains a narrative scaffold, so the predicate closes a demo interface rather than a fully formalised derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.