IndisputableMonolith.Foundation.JCostConvexityInLogSpace
This module re-expresses the J-cost as g(t) = J(e^t) in logarithmic coordinates. Researchers analyzing cost convexity or symmetry in the Recognition Science framework cite it when shifting from multiplicative to additive variables. The module consists entirely of definitions and basic property statements with no central theorem or proof.
claimDefine $g(t) := J(e^t)$ where $J$ is the J-cost from the Cost module. The module also introduces $h$ together with statements $g(0)=0$, $g$ even, $g$ nonnegative off zero, and the certificate JCostLogSpaceCert.
background
The module imports Mathlib and IndisputableMonolith.Cost. Its single doc-comment states the purpose: "J-cost in log coordinates: g(t) = J(eᵗ)." The Cost module supplies the original J definition; this module performs the coordinate change to additive form. Sibling definitions g, g_at_zero, g_even, g_pos_off_zero, h, h_at_zero, h_even, h_nonneg, h_pos_off_zero, same_fixed_point, same_symmetry, and JCostLogSpaceCert record the resulting algebraic properties.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the log-space formulation of J-cost that supports J-uniqueness (T5) and the self-similar fixed point (T6) inside the forcing chain. It prepares the ground for JCostLogSpaceCert and any later convexity arguments that rely on the eight-tick octave or RCL.
scope and limits
- Does not contain any theorem with a proof body.
- Does not import or reference the UnifiedForcingChain.
- Does not derive numerical constants or the phi-ladder.
- Does not address mass formulas or Berry thresholds.