identity_implies_normalized
plain-language theorem explainer
A comparison operator obeying the identity law yields a derived cost function that vanishes at the multiplicative identity. Researchers deriving d'Alembert hypotheses from logical axioms cite this normalization result. The proof proceeds by direct substitution of the identity condition into the definition of the derived cost at unity.
Claim. If a comparison operator $C$ satisfies $C(x,x)=0$ for every positive real $x$, then the derived cost function $F(x)=C(x,1)$ satisfies $F(1)=0$.
background
In the LogicAsFunctionalEquation module, comparison operators encode the cost of comparing positive quantities, subject to Aristotelian constraints. The Identity property states that comparing any quantity to itself incurs zero cost. The derived cost function is obtained by fixing one argument to the multiplicative identity 1, so that $F(x)=C(x,1)$. Normalization requires that this function evaluates to zero at 1.
proof idea
The proof unfolds IsNormalized and derivedCost to expose the claim that the derived cost at 1 equals zero. It then invokes the Identity hypothesis at the positive real 1. The entire argument is a single exact application of the hypothesis after unfolding.
why it matters
This result is the first translation lemma in the chain that converts the laws of logic into the hypotheses of the d'Alembert theorem. It is invoked inside laws_of_logic_imply_dalembert_hypotheses to establish normalization of the derived cost, and also supports log_aczel_data_of_laws in the GeneralizedDAlembert module. The normalization condition is essential for calibrating the J-cost in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.