Elementary Exact Values

Abstract

The elementary constants have exact forms in the quadratic field generated by square root five.

Theorem 1.1 (The elementary constants lie in the golden quadratic field).

$$A_F=\kappa =\frac{1}{2\phi }=\frac{\sqrt{5}-1}{4},\overline{h}=-\frac{1}{2},s_1=\frac{1+\sqrt{5}}{12},A_h=\frac{5\sqrt{5}-3}{24},E=\frac{137-61\sqrt{5}}{24}.$$

Proof. Machine-checked in Lean as D5/S3/Constants/ElementaryExactValues.elementary_exact_values (✓ std3). ∎

Source. Repository-derived.

Commentary.

Write A_F for the slope constant kappa. Its defining reciprocal golden-ratio expression rationalizes to (sqrt(5) - 1) / 4. The correction-fiber mean, dimension-reduction coefficient, h-side constant, and elementary shell are already given by their exact expressions in the same quadratic field.

The proof unfolds the repository’s canonical constant definitions. All clauses except the rationalized form of kappa are definitional; that clause follows by clearing the nonzero golden-ratio denominator and using the identity (sqrt(5))^2 = 5. Thus the theorem is an exact algebraic package and introduces no numerical approximation.

References

• Truth anchor: D5/S3/Constants/ElementaryExactValues.elementary_exact_values