Jcost_val_2
The declaration verifies that the J-cost of the integer 2 equals one quarter in RS-native units. Researchers tabulating costs for the discrete phi-ladder or checking the paper's Tables 1-3 would cite this numeric anchor. The proof is a one-line wrapper that unfolds the Jcost definition and reduces the arithmetic by normalization.
claim$J(2) = 1/4$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost function.
background
The OntologyPredicates module defines operational notions of existence and truth via cost minimization under the unique J function, with RSExists x holding precisely when defect(x) collapses to zero. Jcost appears as the concrete cost Quantity in the RSNative.Core layer. The phi-ladder is introduced as the discrete skeleton {x | exists n in Z, x = phi^n}, and RSReal_gen D x combines RSExists x with membership in such a skeleton D. This theorem belongs to the numeric verification block that checks concrete J-cost values used in the paper's Tables 1-3.
proof idea
The proof is a one-line wrapper that unfolds Cost.Jcost and applies norm_num to evaluate the expression at input 2.
why it matters in Recognition Science
The result supplies an explicit numeric anchor required for the paper's Section 4.1 tables and the broader verification that the J-cost structure reproduces observed constants. It sits downstream of the Cost definition and supports the forcing chain steps that fix J-uniqueness and the phi-ladder. No downstream theorems currently cite it, leaving it as a standalone numeric check.
scope and limits
- Does not prove the general closed form of Jcost for arbitrary positive integers.
- Does not invoke the Recognition Composition Law or derive the value from it.
- Does not connect the result to membership in the phi-ladder or RSReal_gen.
- Does not address continuous arguments or non-integer inputs.
formal statement (Lean)
514theorem Jcost_val_2 : Cost.Jcost 2 = 1 / 4 := by
proof body
One-line wrapper that applies unfold.
515 unfold Cost.Jcost; norm_num
516