used
plain-language theorem explainer
Packages the six axioms that define the Law of Logic for a comparison operator: identity, non-contradiction, excluded middle (continuity), scale invariance, route independence, and non-triviality. Downstream uniqueness and cost-algebra results cite this bundle rather than listing the axioms inline. As a structure alias there is no proof body; it is pure interface.
Claim. A comparison operator obeys the Law of Logic if and only if it satisfies identity, non-contradiction, excluded middle (continuity), scale invariance, route independence, and non-triviality. This structure is the theorem-facing packaging of that conjunction.
background
The module treats classical logical laws as constraints on a comparison (cost) operator rather than as primitive syntax. The Recognition Composition Law and the J-cost $J(x)=(x+x^{-1})/2-1$ sit upstream: logical identity is the zero-cost fixed point at $x=1$, and the remaining laws become regularity and invariance conditions on that cost.
Sibling definitions name the six pieces: Identity (canonical unit event), NonContradiction, ExcludedMiddle (continuity form), ScaleInvariant, RouteIndependence, and NonTrivial. SatisfiesLawsOfLogic and LawOfLogic assemble them; the present structure is the alias existing proofs already import when they need the full bundle.
Local setting is Foundation: forcing the unique cost functional from logical axioms before physics constants are derived (T5 J-uniqueness in the forcing chain).
proof idea
No proof body: claim status is definition (structure / abbrev). It is a named packaging of the six logical axioms already defined as sibling Props, exposed as the theorem-facing Law-of-Logic interface. Downstream lemmas unfold or coerce through this alias rather than re-listing fields.
why it matters
Gives a single citation target for "the comparison operator obeys the laws of logic," which cost-algebra uniqueness and action-minimization arguments need as ambient structure. Downstream, cost_algebra_unique (T5: any calibrated CostAlgebraData has cost $=J$) and geodesic-minimization results in Action.FunctionalConvexity sit on cost operators that are assumed to satisfy this law bundle.
In the Recognition framework this is the logic-to-functional-equation bridge: classical laws become the hypotheses that force $J$ via the Recognition Composition Law, before $\varphi$, the eight-tick octave, and $D=3$ are derived. Without a stable theorem-facing alias, every uniqueness proof would re-open the axiom list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.