pith. sign in
module module high

IndisputableMonolith.Foundation.AlphaCoordinateFixation

show as:
view Lean formalization →

The AlphaCoordinateFixation module computes the first four derivatives of CostAlphaLog and proves that high calibration pins alpha to one, which implies the J-function form. Researchers tracing the forcing chain would cite these identities to justify the WLOG alpha-equals-one reduction after the upstream calibration step. The module structure consists of successive differentiation lemmas followed by implication theorems under the high-calibration hypothesis.

claimThe first derivative satisfies $d/dt$ CostAlphaLog($alpha$)(t) = sinh($alpha$ t)/$alpha$. High calibration forces $alpha=1$, which implies the cost takes the form $J(x)$ where $J(x)=(x+x^{-1})/2-1$.

background

This module sits in the foundation layer and imports the Cost module together with the WLOGAlphaOne result. The upstream proposition states: After calibration kappa(F)=1 forces c=2 alpha squared, the calibrated solution family is F_alpha(x)=(1/alpha squared)(cosh(alpha ln x)-1) for alpha greater than or equal to 1. It further records that F_alpha(x)=(1/alpha squared) J(x^alpha) with J(x)=(x+x inverse)/2 minus 1. The module introduces CostAlphaLog as the cost expressed in logarithmic coordinates and derives its derivatives to support the alpha-fixation step.

proof idea

The module first establishes hasDerivAt for the initial derivative of costAlphaLog and equates it to sinh(alpha t)/alpha. It repeats the differentiation for the second, third, and fourth orders, evaluates the fourth derivative at zero, then proves the high-calibration condition implies alpha pinned to one and that this pinning yields the J-form via the upstream equivalence.

why it matters in Recognition Science

This module supplies the alpha pinning required by the master forcing-chain theorem exposed in the root IndisputableMonolith module. It completes the coordinate-rescaling step begun in the WLOGAlphaOne proposition, enabling the reduction to the self-similar J-cost that appears in the T5 J-uniqueness landmark of the forcing chain. By fixing alpha to one it opens the path to the eight-tick octave and D=3 derivations that follow.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)