Jcost_val_three_halves
plain-language theorem explainer
The theorem establishes that the J-cost of 3/2 equals 1/12, a concrete evaluation referenced in Example 3 and Table 3. Researchers citing cost values for stable configurations under the Recognition Science ontology would use this result. The proof is a direct term-mode reduction that unfolds the Jcost definition and normalizes the arithmetic.
Claim. $J(3/2) = 1/12$, where $J(x) = (x + x^{-1})/2 - 1$ is the unique cost function satisfying the Recognition Composition Law.
background
The module OntologyPredicates defines the operational ontology of Recognition Science, where RSExists x holds precisely when defect(x) collapses to zero under J-cost minimization, and RSTrue P holds when P stabilizes under recognition iteration. Jcost is imported as the abbrev Cost := Quantity CostUnit from the RSNative core, supplying the numerical cost measure on which all existence predicates rest. This theorem supplies one explicit evaluation of that cost function for use in the module's examples and tables.
proof idea
The proof is a one-line term wrapper that unfolds the definition of Jcost and applies norm_num to reduce the resulting rational expression to 1/12.
why it matters
This supplies a concrete J-value needed for Example 3 and Table 3 in the ontology predicates module. It instantiates the J function whose uniqueness is forced at T5 of the UnifiedForcingChain and whose composition law (RCL) underpins the entire cost structure. The result sits inside the proved claim_status block and closes a numerical gap that downstream predicates such as rs_exists_iff_defect_zero rely upon for concrete checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.