Jcost_val_2
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.