SatisfiesLawsOfLogicAbsoluteFloor
plain-language theorem explainer
SatisfiesLawsOfLogicAbsoluteFloor packages the five Aristotelian laws on a comparison operator together with an absolute-floor witness on positive ratios and an explicit detection condition that distinct points yield nonzero cost. Researchers deriving non-triviality of the cost function from distinguishability in the Recognition Science foundation cite this structure when converting the absolute-floor closure into the canonical law-of-logic data. The declaration is introduced as a direct structure definition that assembles the fields without a
Claim. A comparison operator $C: (0,∞)×(0,∞)→ℝ$ satisfies the absolute-floor laws of logic when it obeys identity ($C(x,x)=0$ for all $x>0$), reciprocal symmetry of cost, continuity on the positive quadrant, scale invariance, route independence, admits an absolute-floor witness on the positive-ratio carrier, and returns nonzero cost whenever the two positive ratios are distinct.
background
The module replaces the non-triviality posit inside SatisfiesLawsOfLogic with distinguishability, the claim that comparison is not vacuous on positive ratios. PositiveRatio is the subtype {x:ℝ | 0<x}. ComparisonOperator is the type of real-valued cost functions on pairs of positive reals. Upstream, AbsoluteFloorWitness K asserts ∃P Q, P≠Q together with Nonempty(NontrivialSpecification K); its doc-comment states that the witness forces bare distinguishability. The five laws (identity, non-contradiction, excluded middle, scale invariance, route independence) are imported from LogicAsFunctionalEquation and supply the Aristotelian structural content.
proof idea
The declaration is a structure definition that directly enumerates the required fields: the five laws from LogicAsFunctionalEquation, the AbsoluteFloorWitness on PositiveRatio, and the detection predicate. No lemmas are invoked and no tactics are executed; the structure simply collects the properties.
why it matters
This structure supplies the absolute-floor form of the law-of-logic data. It is used by canonical_of_absoluteFloor to induce the canonical form, by distinguishability_of_absoluteFloor to extract ordinary distinguishability via bare_distinguishability_of_absolute_floor, and by existing_of_absoluteFloor to reach the algebraic form used downstream. In the Recognition framework it replaces the residual non-triviality posit with Aristotelian distinguishability, eliminating reference to the derived cost function. It touches the question whether the constant-zero operator can be excluded from the Aristotelian laws alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.