IndisputableMonolith.Cost.Calibration
The Cost.Calibration module supplies identities that equate the Jlog cost function to cosh(t) minus one and derive its first and second derivatives plus unit curvature. Recognition Science researchers working on cost-based derivations cite these results to simplify calculations in the J-uniqueness step. The module proceeds by algebraic substitution for the core equality followed by Mathlib differentiation tactics on the imported Cost definitions.
claim$J_{log}(t) = cosh(t) - 1$, together with results on the first derivative, second derivative at zero, and unit curvature of $J_{log}$.
background
This module belongs to the Cost domain and imports the base Cost module that defines the J-cost via the Recognition Composition Law. The central object is the Jlog function, the logarithmic calibration of J, which satisfies Jlog(t) = cosh(t) - 1 by the substitution x = e^t into the definition J(x) = (x + x^{-1})/2 - 1. The setting aligns with T5 J-uniqueness in the forcing chain, where this hyperbolic form simplifies curvature and derivative work for the phi-ladder.
proof idea
The module organizes its content as a sequence of lemmas rather than a single proof. Jlog_eq_cosh is obtained by direct algebraic substitution. Subsequent lemmas apply Mathlib differentiation rules to produce hasDerivAt_Jlog_new, deriv_Jlog, the second derivative at zero, and Jlog_unit_curvature. No complex tactic chains are required beyond standard derivative lemmas.
why it matters in Recognition Science
The module supplies the hyperbolic representation required by T5 J-uniqueness in UnifiedForcingChain, enabling clean derivative calculations that feed the phi fixed point, eight-tick octave, and D = 3 spatial dimensions. It underpins cost computations used in the phi-ladder mass formula and Berry creation threshold. No downstream declarations are listed, yet the identities close a calibration gap between the abstract J-cost and its analytic form.
scope and limits
- Does not prove the Recognition Composition Law.
- Does not address the full T0-T8 forcing chain.
- Does not compute numerical values for constants such as alpha or G.
- Does not extend the curvature results beyond the one-dimensional Jlog case.