canonical_of_absoluteFloor
plain-language theorem explainer
The theorem shows that a comparison operator satisfying the absolute-floor laws of logic also satisfies the canonical version that uses distinguishability in place of algebraic non-triviality. Foundation researchers in Recognition Science cite this when deriving the standard Aristotelian form from the absolute-floor closure. The proof is a term-mode structure construction that reuses the five shared law fields from the hypothesis and invokes distinguishability_of_absoluteFloor to supply the final field.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ satisfies the absolute-floor laws of logic (the five core laws together with an absolute-floor witness and detection of distinct points), then $C$ satisfies the canonical laws of logic (the same five laws together with distinguishability).
background
The module NonTrivialityFromDistinguishability replaces the algebraic non-triviality posit in SatisfiesLawsOfLogic with the Aristotelian notion of distinguishability, showing the two are equivalent under the core laws. A ComparisonOperator is an abbrev for a real-valued cost function on pairs of positive reals. SatisfiesLawsOfLogicAbsoluteFloor is the structure containing identity, non-contradiction, excluded middle, scale invariance, route independence, an AbsoluteFloorWitness on PositiveRatio, and the detection property that distinct points yield non-zero cost. SatisfiesLawsOfLogicCanonical is the parallel structure whose final field is instead Distinguishability. The upstream result distinguishability_of_absoluteFloor extracts a witnessing pair from the floor closure and applies the detection property to obtain ordinary distinguishability.
proof idea
The proof is a term-mode construction of the SatisfiesLawsOfLogicCanonical structure. It directly assigns the identity, non-contradiction, excluded middle, scale invariance, and route independence fields from the input hypothesis. The distinguishability field is filled by applying the upstream lemma distinguishability_of_absoluteFloor to the operator and hypothesis.
why it matters
This declaration bridges the absolute-floor specification to the canonical form required by downstream modules. It is used by existing_of_absoluteFloor, which composes it with canonical_iff_existing to recover the algebraic SatisfiesLawsOfLogic. In the framework it completes the module's program of deriving non-triviality as a corollary of distinguishability rather than positing it, thereby grounding the residual commitment in genuinely Aristotelian language as stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.