existing_of_absoluteFloor
plain-language theorem explainer
The theorem shows that any comparison operator meeting the absolute-floor variant of the laws of logic also meets the standard algebraic form. Researchers replacing the non-triviality posit with distinguishability in the foundational layer would cite this equivalence. The proof is a one-line term application of the canonical equivalence after absolute-floor canonicalization.
Claim. Let $C : ℝ → ℝ → ℝ$ be a comparison operator. If $C$ satisfies the absolute-floor laws of logic (identity, non-contradiction, excluded middle, scale invariance, route independence, an absolute-floor witness on positive ratios, and detection of distinct points by nonzero cost), then $C$ satisfies the standard laws of logic.
background
A ComparisonOperator assigns a real cost to pairs of positive reals. The structure SatisfiesLawsOfLogic requires identity ($C x x = 0$), non-contradiction, excluded middle, scale invariance, and route independence. SatisfiesLawsOfLogicAbsoluteFloor augments this with an AbsoluteFloorWitness on PositiveRatio together with the detection condition that distinct carrier points yield nonzero cost, as stated in its definition.
proof idea
The proof is a one-line term wrapper: it applies canonical_of_absoluteFloor to the absolute-floor hypothesis to obtain the canonical form, then uses the mp direction of canonical_iff_existing to reach the target SatisfiesLawsOfLogic.
why it matters
This declaration completes the module's replacement of the non-triviality posit by distinguishability, as described in the module documentation. It supplies the algebraic form required by downstream modules without an extra non-trivial hypothesis and aligns with the Recognition Science move from posited non-triviality to a corollary of the functional equation structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.