pith. sign in
theorem

identity_from_equality

proved
show as:
module
IndisputableMonolith.Foundation.PrimitiveDistinction
domain
Foundation
line
104 · github
papers citing
1 paper (below)

plain-language theorem explainer

The theorem shows that any equality-induced cost on a carrier type K with real weight returns zero on identical arguments. Logicians and physicists deriving Aristotelian laws from recognition costs cite it as the definitional identity condition (L1). The proof is a one-line wrapper that unfolds the cost definition and reduces via simplification to reflexivity of equality.

Claim. For any type $K$ and real weight $w$, the equality-induced cost satisfies $C(x,x)=0$ for all $x$ in $K$, where $C$ is the cost function derived from the equality predicate on $K$.

background

In the PrimitiveDistinction module the equalityCost function assigns zero to identical pairs and a positive multiple of the supplied weight to distinct pairs. This construction sits inside the derivation of logic from functional equations on costs, as imported from LogicAsFunctionalEquation. Upstream cost definitions appear in MultiplicativeRecognizerL4.cost (derivedCost on positive ratios) and ObserverForcing.cost (J-cost of a recognition event).

proof idea

The proof is a one-line wrapper: introduce the arbitrary element, unfold equalityCost, and apply simp to reduce the claim to reflexivity of equality.

why it matters

This supplies the identity component for equality_cost_satisfies_definitional_conditions, which packages the definitional Aristotelian conditions and feeds the Recognizer structure in RecognizerInducesLogic. It fills the (L1) slot in aristotelian_decomposition, showing that identity follows from reflexivity rather than an extra axiom. The result anchors the foundation layer before substantive conditions such as scale invariance or non-triviality are imposed.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 1 of 1)