leq_antisymm_structural
plain-language theorem explainer
Mutual Boolean order on finite distinction-orbit positions packages as a two-sided order witness without leaving the forced carrier. Anyone assembling forced trichotomy or pure antisymmetry of the primitive recognition order cites this. The proof is a one-line And-constructor pairing of the two hypotheses; no recursion and no integer bridge appear.
Claim. For finite distinction-orbit positions $a$ and $b$, if the structural Boolean order holds both ways ($a \le b$ and $b \le a$ both evaluate to true), then both directions hold simultaneously as a conjunction: structural $\le$-equivalence both ways.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction: an inductive carrier with constructors zero and succ, used as the forced-side stand-in for finite $\delta$-orbit positions (K2.12).
The Boolean order leq on that carrier is defined by structural recursion only: zero is $\le$ everything; a successor is never $\le$ zero; and leq (succ a) (succ b) reduces to leq a b. No conversion to $\mathbb{N}$ or $\mathbb{Z}$ is involved in the definition.
This declaration lives in the ForcedTrichotomy grow module of the primitive recognition calculus. The local programme develops order facts (totality, trichotomy, decidability, antisymmetry) strictly on the forced carrier, deliberately avoiding the toNat display bridge that would pull in omega and choice-tainted axioms.
proof idea
Term-mode one-liner. The goal is exactly the conjunction of the two hypotheses, so the proof is the And-intro pair $\langle hab, hba \rangle$. No lemmas, no induction, and no bridge facts are applied.
why it matters
Structural antisymmetry is stated and discharged entirely on the forced side: if both Boolean directions hold, the positions are $\le$-equivalent both ways. The doc-comment stresses that the toNat bridge (which uses omega and is choice-tainted) is deliberately not used, so #print axioms stays empty and the witness remains on the forced carrier.
It sits with the sibling forced-order facts (Boolean totality, Boolean trichotomy, decidability of the forced order) that assemble the pure order package before any integer display. No downstream consumers are recorded yet; the value is foundational hygiene for later recognition-calculus steps that must not import classical arithmetic axioms into the forced layer.
In the broader Recognition Science stack this protects the purity of the primitive recognition calculus that underwrites later forcing-chain material (orbit structure feeding T5–T8 landmarks), by keeping order antisymmetry free of display-side contamination.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.