Golden Notation
Abstract
Golden notation remains opt-in and names the carrier, generator, conjugation, and norm.
D5/S0/Conventions/Notation provides opt-in notation under the Golden scope. The symbols denote the golden integer type, its distinguished generator, the conjugation ring equivalence, and the multiplicative norm homomorphism.
The scope is not opened globally. Importers choose it explicitly, preventing collisions with other uses of phi, sigma, or N in mathlib and future theories.
References
- Dependency: D5/S0/Carrier/Units
- Dependency: D5/S0/Conventions/WDigits