Jcost_val_half
plain-language theorem explainer
The declaration establishes the explicit evaluation J(1/2) = 1/4 under the Recognition Science cost function. Researchers computing concrete values on the phi-ladder or verifying reciprocal symmetry in defect calculations would cite this instance. The proof is a one-line wrapper that unfolds the Jcost definition and reduces the arithmetic expression by normalization.
Claim. $J(1/2) = 1/4$, where $J(x) = (x + x^{-1})/2 - 1$ is the cost function satisfying the Recognition Composition Law.
background
The OntologyPredicates module defines operational notions of existence and truth as outcomes of cost minimization: RSExists x holds when defect(x) collapses to zero under J, and RSTrue P holds when P stabilizes under recognition iteration. The Jcost function is imported from the core measurement module as an abbrev Cost := Quantity CostUnit whose associated Jcost implements the unique J satisfying J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This supplies the concrete numerical anchor needed for the module's later predicates that reference specific cost values.
proof idea
The proof is a one-line wrapper that unfolds Cost.Jcost and applies norm_num to evaluate the resulting rational expression directly.
why it matters
The result supplies the explicit value J(1/2) = 1/4 required for Example 3 and Table 3, confirming the reciprocal symmetry built into the J definition. It instantiates the T5 J-uniqueness step of the forcing chain and supports downstream mass-formula calculations on the phi-ladder. No parent theorems in the current used_by graph reference it, leaving the concrete value available for future closure of scaffolding around defectDist and RSExists predicates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.