AlphaCoordinateFixationCert
plain-language theorem explainer
The AlphaCoordinateFixationCert structure records that fourth-derivative calibration at zero on the family G_α(t) = (1/α²)(cosh(α t) − 1) forces α = 1 under the convention α ≥ 1 and thereby isolates the canonical J-cost. Researchers working on branch selection after the bilinear reduction would cite the certificate when fixing the remaining scale parameter. The structure is assembled by direct reference to the fourth-derivative identity, the calibration equivalence, and the pinning and uniqueness lemmas already proved in the WLOGAlphaOne import
Claim. The certificate asserts that for the family $G_α(t) := (1/α²)(cosh(α t) − 1)$ with α ≥ 1 the following hold: the fourth derivative satisfies $G_α^{(4)}(0) = α²$ for α ≠ 0; high calibration $G_α^{(4)}(0) = 1$ holds if and only if α² = 1; the calibration condition together with α ≥ 1 forces α = 1; the cost at α = 1 coincides with the J-cost for all x > 0; and the same calibration condition forces the cost at any α ≥ 1 to coincide with the J-cost for all x > 0.
background
In the Recognition Science framework the branch-selection theorem reduces the calibrated bilinear costs to the one-parameter family F_α(x) = (1/α²)(cosh(α ln x) − 1) for α ≥ 1. The associated log-coordinate function is G_α(t) = (1/α²)(cosh(α t) − 1). The predicate IsHighCalibratedLog(G) holds precisely when the fourth derivative of G at zero equals one. The module records the consequences of imposing this higher-derivative calibration on the α-family.
proof idea
The structure is populated by direct references to four lemmas already established in the same module and its WLOGAlphaOne import: the explicit fourth-derivative evaluation supplies the equality to α²; the equivalence converts the calibration predicate into the condition α² = 1; the pinning lemma forces α = 1 under the convention α ≥ 1; and the uniqueness statement together with the α = 1 case shows that the cost collapses to the J-cost.
why it matters
This certificate supplies the concrete content for Option 2 (higher-derivative calibration) listed in §5 of the companion paper RS_Branch_Selection.tex. It is used to construct the inhabited instance alphaCoordinateFixationCert, which in turn feeds the main branch-selection theorems that isolate the canonical J-cost. Within the T0–T8 forcing chain the result realises the J-uniqueness step once the bilinear branch has been selected, confirming that the self-similar fixed point is recovered precisely when the fourth-derivative calibration is imposed. The other two candidate fixations remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Tsallis entropy yields Van der Waals black hole transitions
"constraint −1/36 < η < 1 ... critical point at η_C ≈ −0.0274 for Q=0.06 ... numerically determined T_c ≈ 0.159, Q_c ≈ 0.222"