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

independent

show as:
view Lean formalization →

RS-independence holds for two coupled axes precisely when their carrying recognition primitives differ. Researchers building cross-domain combination theorems cite this predicate to license pairwise checks before applying product or sum constructions. The definition extracts and compares the primitive tags from the CoupledAxis records.

claimTwo finite axes $A$ of cardinality $n$ and $B$ of cardinality $m$, each tagged by an RS primitive, are independent if and only if their primitives satisfy primitive$(A) ≠$ primitive$(B)$.

background

The module supplies infrastructure for cross-domain theorems by equipping finite axes with recognition-primitive tags. A CoupledAxis $n$ consists of a finite index type of cardinality exactly $n$ together with a primitive tag drawn from RSPrimitive that identifies the physical meaning carried by the axis.

proof idea

One-line definition that projects the primitive field from each CoupledAxis argument and asserts their inequality.

why it matters in Recognition Science

The predicate feeds downstream results such as space_translation_invariance_implies_momentum_conservation and all_ml_on_phi_ladder by guaranteeing that axes from distinct primitives may be combined. It implements the module's core distinction that equal cardinality alone does not imply independence, aligning with the framework's use of primitives to separate physical domains.

scope and limits

formal statement (Lean)

  39def independent {n m : ℕ} (A : CoupledAxis n) (B : CoupledAxis m) : Prop :=

proof body

Definition body.

  40  A.primitive ≠ B.primitive
  41
  42/-- Pairwise independent triple of same-size axes. -/

used by (40)

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

… and 10 more

depends on (10)

Lean names referenced from this declaration's body.