IndisputableMonolith.Foundation.JCostConvexityInLogSpace
The module translates the J-cost into logarithmic coordinates by defining g(t) = J(e^t). Researchers analyzing convexity or fixed-point behavior of the cost function in log-space would cite these results. It supplies auxiliary function h together with targeted lemmas on values at zero, parity, sign, and shared symmetry properties, culminating in the JCostLogSpaceCert.
claimLet $J(x) = (x + x^{-1})/2 - 1$. Define $g(t) := J(e^t)$ and auxiliary $h$. The module records $g(0) = 0$, $g$ even, $g(t) > 0$ for $t > 0$, and the parallel statements for $h$, plus the relations that $g$ and $h$ share the same fixed point and the same symmetry.
background
The upstream Cost module supplies the base J-cost obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). This module performs the change of variables t = log x, yielding the function g(t) = J(e^t) whose properties are easier to inspect in additive coordinates. It also introduces a companion function h and records elementary facts at t = 0 together with parity and positivity statements.
proof idea
This is a definition module, no proofs. Successive definitions introduce g and h; each is followed by a short lemma establishing the value at zero, evenness, non-negativity off zero, and the two shared relations (same_fixed_point, same_symmetry). The final declaration JCostLogSpaceCert packages the collection for downstream use.
why it matters in Recognition Science
The log-space representation is a prerequisite for convexity arguments inside the Recognition Science framework and directly supports JCostLogSpaceCert. It aligns with the T5 J-uniqueness step of the forcing chain and prepares the ground for later phi-ladder and mass-formula developments that rely on the same fixed-point and symmetry properties.
scope and limits
- Does not derive the explicit algebraic form of J.
- Does not prove convexity of g or h.
- Does not connect to physical constants or units.
- Does not address the eight-tick octave or spatial dimension D = 3.