pith. sign in
def

Identity

definition
show as:

Why this theorem is linked from mHC: Manifold-Constrained Hyper-Connections echoes

Pith linked this Lean declaration because the review connected a specific passage in the paper to this theorem. The relation tag says how strong that connection is; it is not a generic placeholder.

projects the residual connection space of HC onto a specific manifold to restore the identity mapping property

ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

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)