SatisfiesLawsOfLogicCanonical
plain-language theorem explainer
SatisfiesLawsOfLogicCanonical packages six Aristotelian conditions on a comparison operator C into one Prop, replacing algebraic non-triviality with distinguishability. Researchers deriving physics from the Recognition functional equation cite it when grounding the laws of logic in primitive comparison content. The declaration is a direct structure definition that bundles the predicates without any reduction steps.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. Then $C$ satisfies the canonical laws of logic if it obeys identity ($C(x,x)=0$ for all $x>0$), non-contradiction ($C(x,y)=C(y,x)$), excluded middle (continuity on the positive quadrant), scale invariance, route independence (composite costs are quadratic polynomials), and distinguishability (there exist $x,y>0$ with $C(x,y)≠0$).
background
The NonTrivialityFromDistinguishability module replaces the algebraic non-triviality posit in SatisfiesLawsOfLogic with distinguishability. ComparisonOperator is the type ℝ → ℝ → ℝ of cost maps on positive reals. Upstream definitions supply the components: Identity requires zero self-cost, NonContradiction requires symmetry under argument swap, ExcludedMiddle requires continuity on the positive quadrant, ScaleInvariant ensures ratio dependence, and RouteIndependence requires that symmetric composite costs are quadratic polynomials in the separate ratio costs.
proof idea
This is a structure definition that directly assembles the six predicates identity, non_contradiction, excluded_middle, scale_invariant, route_independence, and distinguishability. No lemmas are applied and no tactics are used; the body simply lists the fields.
why it matters
The structure supplies the canonical form referenced by the downstream equivalence canonical_iff_existing, which equates it to the original SatisfiesLawsOfLogic. It completes the module's program of promoting non-triviality from posit to corollary of distinguishability, removing algebraic language from the Aristotelian core. In the Recognition framework this supports the forcing chain by ensuring comparison is operative before deriving the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.