Jcost_val_5
plain-language theorem explainer
The theorem states that the J-cost at argument 5 equals 8/5. Researchers evaluating defect distances on the phi-ladder cite this entry when stepping through integer rungs in mass formulas. The proof is a one-line wrapper that unfolds the Jcost definition and normalizes the arithmetic.
Claim. The J-cost at 5 equals $8/5$, where J(x) = (x + x^{-1})/2 - 1.
background
The OntologyPredicates module supplies operational definitions of existence and truth as outcomes of cost minimization under the unique J map. RSExists x holds precisely when defect(x) reaches zero under coercive projection. The upstream Cost abbrev defines Jcost as a Quantity of type CostUnit, supplying the numerical measure of recognition expense at each point.
proof idea
The proof is a one-line wrapper that unfolds Cost.Jcost and applies norm_num to reduce the arithmetic expression directly to 8/5.
why it matters
This supplies a concrete base value for J-cost entries used in the phi-ladder mass formula and defect calculations. It supports the T5 J-uniqueness step in the forcing chain by providing an explicit numerical anchor at rung 5. No downstream theorems are recorded, so the declaration functions as a primitive constant lookup.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.