Golden Midline Factorization

Abstract

The golden midline marker factors into one half and the reciprocal golden square.

Theorem 1.1 (Factorization of the golden midline marker).

$$\frac{1}{2\times {\phi }^2}=(\frac{1}{2})\times (\frac{1}{{\phi }^2}).$$

Proof. Machine-checked in Lean as D5/S0/Carrier/Powers/GoldenMidlineFactorization.golden_midline_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s generic one_div_mul_one_div identity rewrites the reciprocal of a product as the product of the two reciprocals. Specializing its factors to 2 and the square of the real golden ratio proves the displayed identity without adding a second proof of the generic law.

This is a deeper partial closure of the source remark. The conjugation and field-action interpretations, together with the other five source subitems, remain unresolved and are not asserted here.

References

• Truth anchor: D5/S0/Carrier/Powers/GoldenMidlineFactorization.golden_midline_factorization