LawOfLogic
plain-language theorem explainer
Public alias for the continuous positive-ratio Law of Logic: a two-argument comparison cost on positive reals obeys identity, non-contradiction, excluded middle (continuity), scale invariance, route independence, and non-triviality. Downstream uniqueness theorems cite this name when forcing the Recognition Composition Law and the canonical cost J. The body is a one-line abbreviation of the underlying structure.
Claim. For a comparison operator $C:\mathbb{R}_{>0}\times\mathbb{R}_{>0}\to\mathbb{R}$, the Law of Logic holds precisely when $C$ satisfies identity, non-contradiction, excluded middle (continuity), scale invariance, route independence, and non-triviality.
background
In this module, a comparison operator is any real-valued map of two positive quantities, intended as the cost of comparing them. The Aristotelian constraints (identity, non-contradiction, excluded middle) encode that comparison is a well-posed logical operation; scale invariance reduces the two-argument form to a cost on positive ratios; route independence constrains how costs compose along multiplicative paths; non-triviality rules out the zero cost.
The underlying structure packages those six properties. The present declaration is only a public short name for that package, kept so theorem statements can say "Law of Logic" while existing proofs continue to use the longer historical name.
The local setting is the continuous positive-ratio functional-equation bridge from logic-shaped comparison axioms to the Recognition Composition Law and the unique calibrated cost $J$.
proof idea
Definitional abbreviation: LawOfLogic C unfolds definitionally to the structure that asserts the six component properties. No tactics or lemmas are involved; equality with the underlying structure is by rfl via the companion lawOfLogic_iff expansion.
why it matters
This alias is the theorem-facing handle for the continuous positive-ratio Law of Logic. Two parent results depend on it: one shows the Law forces the Recognition Composition Law combiner $P(u,v)=2u+2v+c,uv$; the other, under RCL normalization and unit log-curvature calibration, forces the unique continuous positive-ratio cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). That $J$ is the T5 uniqueness landmark in the forcing chain, and RCL is the composition identity that organizes the rest of Recognition Science. The companion lawOfLogic_iff expands the alias into the six conjuncts for proof work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.