totality_from_function_type
plain-language theorem explainer
Equality-induced cost on any carrier type K is total by construction, returning a real for every ordered pair. Foundation researchers cite the result when assembling the definitional Aristotelian conditions before checking substantive failures such as L4. The proof is a one-line term that exhibits the cost value itself as the existential witness via reflexivity.
Claim. Let $K$ be any type and $w$ a real weight. Let $C$ be the equality-induced cost on $K$ scaled by $w$. Then $C$ is total: for all elements $x,y$ of $K$ there exists a real $c$ such that $C(x,y)=c$.
background
The PrimitiveDistinction module develops distinction and cost structures from a functional-equation view of logic, importing LogicAsFunctionalEquation to supply the Identity predicate (comparison of an element with itself yields zero cost under positivity) and related properties. The equality-induced cost on $K$ scaled by weight is the real-valued function that assigns to each ordered pair the cost of distinguishing its elements under equality; its definition appears among the sibling declarations in the module. This totality statement follows directly from the function type and precedes the composite theorem that bundles Identity, Non-Contradiction, and Totality as definitional.
proof idea
The proof is a term-mode one-liner. It introduces arbitrary elements $x$ and $y$, then constructs the existential witness as the pair consisting of the cost value together with the reflexivity proof rfl. No additional lemmas are invoked beyond basic function application and existential introduction.
why it matters
This result supplies the totality component (L3a) for the Aristotelian decomposition theorem in the same module, which packages the three definitional properties before exhibiting the failure of the fourth condition. It feeds the Recognizer structure in RecognizerInducesLogic by confirming that equality-induced costs are well-defined total functions. In the framework it closes the definitional requirements derived from the functional equation before substantive recognition geometry and the phi-ladder are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.