IndisputableMonolith.Foundation.DAlembert.WLOGAlphaOne
This module defines the α-parameterized cost in logarithmic coordinates as G_α(t) = (1/α²)(cosh(α t) - 1). Researchers reducing the bilinear branch via higher-derivative calibration cite it to reach the one-parameter family. It imports the Cost module and supplies supporting definitions and lemmas to establish the log form for downstream fixation steps.
claim$G_α(t) = (1/α²)(cosh(α t) - 1)$ for α ≥ 1, where t is the logarithmic coordinate.
background
The module sits in the Foundation layer and imports the Cost module, which supplies the base J-cost J(x) = (x + x^{-1})/2 - 1. In log coordinates t = ln x this becomes the scaled hyperbolic expression. The setting prepares the α-family for coordinate fixation, with the downstream AlphaCoordinateFixation module quoting the form F_α(x) = (1/α²)(cosh(α ln x) - 1) to force the J function.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the parameterized cost that AlphaCoordinateFixation relies on to show higher-derivative calibration forces J from the branch-selection theorem. It completes the reduction to the one-parameter family α ≥ 1 inside the Recognition Science forcing chain.
scope and limits
- Does not fix the numerical value of α.
- Does not derive the cost form from the RCL identity.
- Does not address the eight-tick octave or D = 3.
- Does not connect to the phi-ladder mass formula.
used by (1)
depends on (1)
declarations in this module (14)
-
def
CostAlphaLog -
def
CostAlpha -
theorem
cosh_log_eq_jcost_rpow -
theorem
cost_alpha_rescaling -
theorem
cost_alpha_one_eq_jcost -
theorem
rpow_mul_hom' -
theorem
rpow_one_base' -
theorem
rpow_inv_hom' -
lemma
hasDerivAt_alpha_mul -
lemma
hasDerivAt_costAlphaLog -
lemma
deriv_costAlphaLog_eq -
lemma
hasDerivAt_sinhDivAlpha -
theorem
costAlphaLog_unit_curvature -
theorem
wlog_alpha_eq_one