totality_from_function_type
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not assert positivity or zero cost only on identical elements.
- Does not constrain the numerical value taken by the cost.
- Does not require $K$ to carry metric, group, or other algebraic structure.
- Does not interact with the phi-ladder, physical constants, or forcing chain steps beyond definitional totality.
formal statement (Lean)
126theorem totality_from_function_type (K : Type*) (weight : ℝ) :
127 ∀ x y : K, ∃ c : ℝ, equalityCost K weight x y = c := by
proof body
Term-mode proof.
128 intro x y
129 exact ⟨equalityCost K weight x y, rfl⟩
130
131/-- **(L1)+(L2)+(L3a) packaged.** The equality-induced cost satisfies
132the three definitional Aristotelian conditions (Identity,
133Non-Contradiction, Totality) automatically, with no structural
134assumption beyond the existence of an equality predicate on `K`. -/