lawOfLogic_iff
plain-language theorem explainer
A comparison operator on positive reals obeys the continuous positive-ratio Law of Logic exactly when it satisfies identity, reciprocal symmetry, continuity, scale invariance, route independence, and non-triviality. Cite this when treating that law as a single package rather than a structure. The proof is pure packing and unpacking of the underlying structure fields.
Claim. For a comparison operator $C:\mathbb{R}_{>0}\times\mathbb{R}_{>0}\to\mathbb{R}$, $C$ satisfies the Law of Logic if and only if: $C(x,x)=0$ for all $x>0$; $C(x,y)=C(y,x)$; $C$ is continuous on positive pairs; $C(\lambda x,\lambda y)=C(x,y)$ for $\lambda>0$; route independence holds in d'Alembert form; and $C$ is non-trivial.
background
In this module, a comparison operator is any map $C:\mathbb{R}\to\mathbb{R}\to\mathbb{R}$ intended as a real-valued cost of comparing two positive quantities. The Aristotelian content of well-posed comparison is encoded as six propositions on $C$.
Identity says self-comparison costs zero ($C(x,x)=0$). Non-contradiction is reciprocal symmetry ($C(x,y)=C(y,x)$). Excluded middle is continuity of the uncurried map on $(\mathbb{R}_{>0})^2$. Scale invariance says cost depends only on the ratio: $C(\lambda x,\lambda y)=C(x,y)$. Route independence is the d'Alembert polynomial form on composite forward/backward ratios. Non-triviality rules out the zero cost.
The Law of Logic is the public name for the structure bundling these six constraints (historically SatisfiesLawsOfLogic). Under scale invariance one derives a one-argument cost $F(r):=C(r,1)$ on positive ratios, which is the bridge to the cost axioms and d'Alembert inevitability imported by this module.
proof idea
Bidirectional structure equivalence, no mathematics beyond field projection.
Forward: assume the Law of Logic structure; project its six fields (identity, non-contradiction, excluded middle, scale invariance, route independence, non-triviality) into a conjunction.
Reverse: given the six separate hypotheses, rebuild the structure by assigning each hypothesis to the matching field.
Implemented with constructor, then intro/exact one way and rintro with an anonymous structure literal the other way. No external lemmas are applied.
why it matters
This is the theorem-facing expanded formula for the continuous positive-ratio Law of Logic. Downstream translation lemmas (Identity $\Rightarrow$ Normalization, and the other Aristotelian constraints mapped onto d'Alembert hypotheses) sit immediately below it in the module and treat the six conjuncts as separate inputs.
In the Recognition framework this is the logical front door to the cost functional equation path: the six constraints force comparison into the setting where the Recognition Composition Law and J-uniqueness (forcing chain T5: $J(x)=(x+x^{-1})/2-1$) apply, and thence to $\phi$ as the self-similar fixed point (T6). The module imports d'Alembert Inevitability and Cost.FunctionalEquation for that handoff.
No downstream dependents are recorded yet; the declaration is a packaging lemma for citation and for feeding those translation lemmas cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.