pith. sign in
def

Identity

definition
show as:
module
IndisputableMonolith.Foundation.LogicAsFunctionalEquation
domain
Foundation
line
93 · github
papers citing
1 paper (below)

plain-language theorem explainer

Identity defines the zero self-comparison cost property for any comparison operator C on positive reals. Workers formalizing the Recognition functional equation cite it as the direct encoding of the law of identity within the four Aristotelian constraints. The declaration is a one-line definition that simply states the universal quantification C(x,x)=0.

Claim. Let $C:ℝ_{>0}×ℝ_{>0}→ℝ$ be a comparison operator. The predicate Identity$(C)$ asserts that $C(x,x)=0$ for every $x>0$.

background

ComparisonOperator is the abbreviation for maps from pairs of positive reals to reals that assign a comparison cost; the module introduces the four predicates Identity, NonContradiction, ExcludedMiddle and ScaleInvariant as the structural content of comparison being well-posed. These predicates sit inside the larger development of the Recognition Composition Law and the J-cost function derived from scale-invariant comparison. Upstream results supply the reciprocal automorphism on the positive reals and the ledger factorization that calibrate the cost algebra in which the predicates operate.

proof idea

The declaration is a direct definition consisting of the single universal quantifier over positive reals that forces the diagonal cost to vanish.

why it matters

Identity supplies the base identity law required by downstream constructions of canonical ledger and octave algebraic objects and by the CostAlg homomorphisms in the RecognitionCategory. It anchors the functional-equation treatment of logic at the initial step of the unified forcing chain before the J-uniqueness and phi fixed-point stages are derived. The predicate is referenced by forty downstream declarations that build admissible flows and layer-system morphisms.

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

papers checked against this theorem (showing 1 of 1)