Jcost_val_8
plain-language theorem explainer
The J-cost at 8 equals 49/16. Researchers normalizing the base rung of the phi-ladder or verifying the eight-tick octave periodicity would cite this evaluation. The proof is a direct unfolding of the Jcost definition followed by numerical simplification of the resulting rational expression.
Claim. $J(8) = 49/16$, where $J(x) = (x + x^{-1})/2 - 1$.
background
Recognition Science defines RSExists x as the condition that defect(x) collapses to zero under J-cost minimization, making existence a selection outcome rather than a primitive. The J function satisfies the reciprocal symmetry J(x) = J(x^{-1}) via the automorphism in CostAlgebra, and Cost is the quantity type in RS-native units. The module OntologyPredicates links these to operational ontology: x exists precisely when its defect vanishes, and the eight-tick period (2^3) appears as a structural octave in the forcing chain.
proof idea
The proof is a one-line wrapper that unfolds Cost.Jcost and applies norm_num to reduce the arithmetic (8 + 1/8)/2 - 1 directly to the rational 49/16.
why it matters
This supplies the concrete base value at rung 8 for the phi-ladder mass formula yardstick * phi^(rung - 8 + gap(Z)). It anchors the eight-tick octave (T7) in the unified forcing chain and supports defect-zero checks underlying RSExists in the ontology predicates. No downstream uses are recorded, but the value closes a computational leaf needed for stability verification in the cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.