First Period-Twelve Separation Certificates

Abstract

Primitive period-twelve orbits A through M are separated from earlier states.

The first thirteen new cycles are checked against all exact state codes enumerated through period eleven.

Theorem 1.1 (Period-twelve orbit A is disjoint from earlier states).

$$\mathrm{Disjoint}\left(\mathrm{flatMap}\left(goldenOrbitStates,goldenPeriodicOrbitRepresentativesEleven\right),\mathrm{goldenOrbitStates}\left(goldenPeriodTwelveOrbitA\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Tower/GoldenPeriodicTwelve/EnumerationTwelveDisjointA.golden_old_new_periodic_orbit_state_codes_disjoint_a_twelve (✓ std3). ∎

Source. Repository-derived.

Commentary.

No phase code on orbit A occurs in the complete enumeration through period eleven.

References

• Truth anchor: D5/S0/Tower/GoldenPeriodicTwelve/EnumerationTwelveDisjointA.golden_old_new_periodic_orbit_state_codes_disjoint_a_twelve
• Dependency: D5/S0/Tower/GoldenPeriodicTwelve/EnumerationTwelveDistinct