pith. machine review for the scientific record. sign in
def definition def or abbrev high

cancels

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  47@[simp] def cancels (a b : Ribbon) : Bool := (b.dir = ! a.dir) && (b.bit = - a.bit) && (b.tag = a.tag)

proof body

Definition body.

  48
  49/-- Neutral commutation predicate for adjacent syllables. Swapping preserves
  50ledger additivity and winding by construction; we additionally require the
  51start ticks to differ to avoid degenerate swaps. -/

used by (21)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.