distinguishability_of_absoluteFloor
plain-language theorem explainer
Absolute-floor Law-of-Logic data implies ordinary distinguishability for the comparison operator. Researchers working on the Aristotelian foundations of Recognition Science would cite this when moving from the absolute-floor closure to the canonical form. The proof extracts a pair of distinct positive ratios from the floor witness and applies the detects_floor predicate to produce a non-zero comparison cost.
Claim. If $C$ is a comparison operator satisfying the absolute-floor Law-of-Logic conditions, then there exist positive real numbers $x$ and $y$ such that $C(x,y)neq 0$.
background
The module replaces the non_trivial posit in SatisfiesLawsOfLogic with distinguishability, the claim that comparison is operative rather than vacuous. Distinguishability asserts existence of positive reals x and y with C x y ≠ 0. SatisfiesLawsOfLogicAbsoluteFloor packages the Aristotelian laws (identity, non-contradiction, excluded middle, scale invariance, route independence) together with an AbsoluteFloorWitness on PositiveRatio and the detects_floor predicate that forces non-zero cost on distinct carrier points. This result depends on the upstream bare_distinguishability_of_absolute_floor, which states that any AbsoluteFloorWitness forces existence of distinct elements in its carrier.
proof idea
The term proof obtains a pair of distinct elements from the absolute floor witness via bare_distinguishability_of_absolute_floor applied to h.floor, then applies the detects_floor field of the hypothesis to conclude that their comparison cost is non-zero.
why it matters
This theorem supplies the link that lets canonical_of_absoluteFloor produce the canonical Law-of-Logic form from the absolute-floor version. It advances the module goal of stating the residual posit in Aristotelian language without reference to the derived-cost definition. In the Recognition framework this grounds non-triviality directly in distinguishability, removing an algebraic reformulation that was introduced only to rule out the constant-zero operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.