J
plain-language theorem explainer
The J functional is defined by the algebraic expression (x + x^{-1})/2 - 1 on the reals. Recognition Science researchers cite it as the canonical cost measure that realizes T5 J-uniqueness in the forcing chain. The definition is a direct one-line transcription of the closed-form expression, with no lemmas or reductions required.
Claim. $J(x) := (x + x^{-1})/2 - 1$ for $x$ real.
background
The Law of Existence module formalizes the principle that an entity exists precisely when its defect vanishes. The defect functional is introduced immediately after J and is defined by direct application: defect(x) := J(x). This construction sits inside the broader forcing chain that begins with the meta-realization structure for from UniversalForcingSelfReference, which records the structural axioms needed for self-reference.
proof idea
One-line definition that directly transcribes the algebraic form of the J-cost. No tactics or upstream lemmas are invoked; the body is the closed expression itself.
why it matters
This definition supplies the cost measure that underpins every subsequent theorem in the module, including defect_zero_iff_one and unity_unique_existent. It realizes the T5 J-uniqueness landmark of the UnifiedForcingChain, from which the self-similar fixed point phi (T6), the eight-tick octave (T7), and D = 3 (T8) are derived. The Recognition Composition Law is satisfied by this explicit form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.