IndisputableMonolith.CrossDomain.JConvexityUniversality
JConvexityUniversality module certifies the squared form of J-cost together with its convexity, symmetry, and universal sensitivity properties. Researchers applying Recognition Science to cross-domain cost bounds or sensitivity analysis would cite these results. The module proceeds via direct algebraic reductions and identities drawn from the base Cost definition.
claim$J(r) = (r-1)^2/(2r)$ for $r>0$, together with the derived universal sensitivity $J(1+δ) = δ^2/2 + O(δ^3)$ and the quadratic identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$.
background
The module sits in the CrossDomain section and imports Mathlib plus the Cost module. Its doc-comment records the squared J-cost form $J(r)=(r-1)^2/(2r)$, which is algebraically equivalent to the hyperbolic expression $J(r)=(r+r^{-1})/2-1$ used throughout the forcing chain. The module develops a family of supporting lemmas that make this form computationally convenient for cross-domain arguments.
proof idea
The module is a collection of targeted lemmas rather than a single proof. Each result applies algebraic substitution or direct comparison starting from the squared expression: symmetry follows by $r↔1/r$ interchange, the quadratic identity by expansion, and sensitivity bounds by Taylor comparison at $r=1$. No complex tactics; all steps are equational rewrites.
why it matters in Recognition Science
These results supply the explicit J-convexity tools required for cross-domain applications of the Recognition Composition Law. They support T5 J-uniqueness and T6 phi fixed-point steps by giving concrete bounds that feed the eight-tick octave and D=3 forcing. The module closes the computational gap between the abstract J definition and its use in mass-ladder and alpha-band calculations.
scope and limits
- Does not apply for r ≤ 0.
- Does not derive the phi-ladder mass formula.
- Does not address Berry creation threshold.
- Does not extend to multi-variable or field-theoretic J.
depends on (1)
declarations in this module (12)
-
theorem
jcost_squared_form -
theorem
jcost_upper_bound_at_geq_one -
theorem
sensitivity_at_one -
theorem
jcost_at_one_plus_delta -
theorem
jcost_quadratic_identity -
theorem
jcost_log_symmetric -
def
universalSensitivity -
theorem
universalSensitivity_eq -
theorem
leading_order -
theorem
jcost_symmetric_pair -
structure
JConvexityUniversalityCert -
def
jConvexityUniversalityCert