independent
plain-language theorem explainer
The independent predicate declares two CoupledAxis structures independent exactly when their carrying RSPrimitive tags differ. Cross-domain combination results in Recognition Science, including Noether conservation and nucleosynthesis tier statements, cite this predicate to enforce primitive separation before merging axes. The definition reduces to a direct field inequality on the primitive component of each CoupledAxis record.
Claim. Let $A$ be a finite axis of cardinality $n$ tagged by an RSPrimitive and $B$ a finite axis of cardinality $m$ tagged by an RSPrimitive. Then $A$ and $B$ are independent if and only if the primitive of $A$ differs from the primitive of $B$.
background
The RSCoupledAxis module supplies infrastructure for cross-domain combination theorems. A CoupledAxis of size $n$ is a finite type $Ix$ equipped with a Fintype instance, a cardinality proof, and an RSPrimitive tag that carries its meaning. Two axes of any cardinalities count as independent only when their primitives differ; same-cardinality axes are not automatically independent.
proof idea
One-line definition that returns the inequality on the primitive field of the two CoupledAxis records.
why it matters
This definition is invoked by space_translation_invariance_implies_momentum_conservation in Action.Noether and by all_ml_on_phi_ladder together with agrees_with_nucleosynthesis in Astrophysics.NucleosynthesisTiers. It directly implements the module requirement that independence be primitive-tagged rather than cardinality-based, thereby enabling the cross-domain theorems that appear in the used-by graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.