IndisputableMonolith.Foundation.DAlembert.WLOGAlphaOne
Develops the α-parameterized cost in log coordinates, G_α(t)=(1/α²)(cosh(αt)-1), and proves a rescaling that reduces any α≥1 to the canonical case α=1, where the cost equals the Recognition J-cost. Cited by anyone on the d'Alembert/branch-selection path to J-uniqueness. The argument is explicit change of variables plus real-power and derivative identities.
claimThe α-parameterized cost in log coordinates is $G_\alpha(t)=\frac{1}{\alpha^2}(\cosh(\alpha t)-1)$. For $\alpha\ge 1$, a coordinate rescaling identifies $G_\alpha$ with $G_1$, and $G_1(t)$ coincides with the standard J-cost at $e^t$.
background
Recognition Science forces a unique cost $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$ (forcing step T5). Branch selection first narrows the calibrated bilinear family to the one-parameter family [F_\alpha(x)=\frac{1}{\alpha^2}\bigl(\cosh(\alpha\ln x)-1\bigr),\qquad\alpha\ge 1.]
This module works in logarithmic coordinates $t=\ln x$, rewriting the same family as $G_\alpha(t)=\frac{1}{\alpha^2}(\cosh(\alpha t)-1)$. The imported Cost module supplies the base $J$-cost and its elementary identities. The local goal is a without-loss-of-generality reduction: any $\alpha$ is absorbed by rescaling the log-coordinate, so it is enough to study $\alpha=1$.
proof idea
Definitions introduce CostAlpha and CostAlphaLog. The identity cost_alpha_one_eq_jcost is a direct expansion of cosh at α=1. The key lemma cost_alpha_rescaling gives an explicit change of variables $t\mapsto\alpha t$ conjugating $G_\alpha$ to a multiple of $G_1$. Supporting lemmas record real-power homomorphism rules (rpow_mul_hom', rpow_one_base', rpow_inv_hom') and the derivative calculus of the α-scaled maps (hasDerivAt_alpha_mul, hasDerivAt_costAlphaLog, deriv_costAlphaLog_eq, hasDerivAt_sinhDivAlpha) needed by higher-order calibration downstream.
why it matters in Recognition Science
AlphaCoordinateFixation imports the module to force the unique cost $J$ by higher-derivative calibration. Its doc-comment states that branch selection reduces the calibrated bilinear branch to the family $F_\alpha(x)=\frac{1}{\alpha^2}(\cosh(\alpha\ln x)-1)$ for $\alpha\ge 1$. The WLOG α=1 reduction collapses that family onto the T5 J-cost $J(x)=\cosh(\log x)-1$, closing the uniqueness step in the forcing chain. Without the rescaling identity the higher-derivative matching would have to be repeated for every α.
scope and limits
- Does not prove uniqueness of J; only the WLOG reduction of the α-family.
- Does not treat α<1 or complex α.
- Does not derive the Recognition Composition Law.
- Does not fix physical constants or the eight-tick octave.
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