Golden Rational Shell Rigidity

Abstract

Nonzero rational scales cannot collide under a positive golden shell translation.

Theorem 1.1 (Rational golden-shell collisions are trivial).

$$\begin{array}{c}\forall q_1,q_2:\mathbb{Q},n:\mathbb{N},q_2\ne 0\wedge q_1=(ph{i}^2{)}^n\cdot q_2\\ \Rightarrow n=0\wedge q_1=q_2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/GoldenCoding/GoldenRationalShellRigidity.rational_shell_collision_rigidity (✓ std3). ∎

Source. Repository-derived.

Commentary.

If two nonzero rational scales differ by a natural power of the orientation-preserving golden unit, then the shell depth is zero and the scales are equal.

The proof reduces positive powers of the golden unit to a nonzero rational coefficient of the irrational golden ratio. It gives exact rigidity without a quantitative near-collision bound.

References

• Truth anchor: D5/S3/Observer/GoldenCoding/GoldenRationalShellRigidity.rational_shell_collision_rigidity
• Dependency: D5/S3/Observer/GoldenCoding/PrimeGoldenScaleCoordinate