IndisputableMonolith.Cost.JensenSketch
JensenSketch module sketches Jensen inequality for the J-cost function. Researchers deriving cost bounds in Recognition Science cite it for convexity arguments. It imports the Cost module and contains sketch definitions without full proofs.
claim$J(\mathbb{E}[X]) \le \mathbb{E}[J(X)]$ where $J(x) = \frac{x + x^{-1}}{2} - 1$.
background
This module is part of the Cost domain in Recognition Science. It builds on the J-cost introduced in the imported IndisputableMonolith.Cost module. The J function satisfies the Recognition Composition Law and is the fixed point in the forcing chain T5.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supports development of cost inequalities that feed into mass formula derivations and phi-ladder calculations on the eight-tick octave. It relates to T5 J-uniqueness and T6 phi fixed point in the UnifiedForcingChain.
scope and limits
- Does not contain a verified proof of the inequality.
- Does not connect to specific physical constants like alpha or G.