canonical_iff_existing
plain-language theorem explainer
The equivalence shows that for any comparison operator C on positive reals, the canonical structure requiring distinguishability is logically equivalent to the algebraic structure requiring non-triviality of the derived cost. Foundational work in Recognition Science cites this to replace the algebraic non-triviality posit with the Aristotelian distinguishability condition. The term-mode proof constructs the equivalence by bidirectional field mapping, invoking the sibling lemmas that relate distinguishability to non-triviality under scale-invari
Claim. For any comparison operator $C : ℝ → ℝ → ℝ$, the structure requiring identity, non-contradiction, excluded middle, scale invariance, route independence and distinguishability holds if and only if the structure requiring the same five laws plus non-triviality of the derived cost function holds.
background
In NonTrivialityFromDistinguishability the module replaces the non-triviality field in SatisfiesLawsOfLogic with distinguishability. A ComparisonOperator is the abbreviation ℝ → ℝ → ℝ that returns the real-valued cost of comparing two positive quantities. SatisfiesLawsOfLogicCanonical is the structure whose fields are identity, non-contradiction, excluded middle, scale invariance, route independence and distinguishability (the existence of at least one pair of distinct positive quantities whose comparison cost is nonzero). The module doc states that this replacement makes the residual posit “stated in genuinely Aristotelian language, with no reference to the derived-cost definition.” Upstream, ComparisonOperator and the four Aristotelian laws are supplied by LogicAsFunctionalEquation.
proof idea
The term-mode proof uses constructor to split the biconditional. The forward direction copies the five common fields and obtains non_trivial by applying the sibling lemma nonTrivial_of_distinguishability to the scale_invariant and distinguishability fields. The reverse direction copies the five common fields and obtains distinguishability by applying the sibling lemma distinguishability_of_nonTrivial to the non_trivial field.
why it matters
This equivalence is the justification for the canonical form used by the downstream theorem existing_of_absoluteFloor, which derives the algebraic SatisfiesLawsOfLogic from the absolute-floor variant. It completes the module’s step that promotes non-triviality from posit to corollary, grounding the requirement of nonzero cost in distinguishability rather than an algebraic condition on the cost function. In the Recognition framework this supports the logic-as-functional-equation approach by making the Aristotelian content more fundamental.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.