Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Golden Factor Binomial Recovery

Abstract

The fixed-length golden factor and its true-count/scattered-pair profile have the same observation fibers.

Remark 1.1 (Source-linked mathematical interpretation).

Lean statement: D5/S1/Words/GoldenRecovery/GoldenFactorSecondOrderBinomialRigidity.golden_factor_eq_iff_second_order_profile_eq

Formalization. D5/S1/Words/GoldenRecovery/GoldenFactorSecondOrderBinomialRigidity.golden_factor_eq_iff_second_order_profile_eq (✓ std3).

Source. Repository-derived.

Commentary.

The fixed-length golden factor and its true-count/scattered-pair profile have the same observation fibers.

This specializes classical Sturmian binomial rigidity using the frozen Beatty-window owner. It recovers word contents rather than occurrence positions.

This mirror supplies commentary only. The named Lean declaration and its kernel report own the exact statement and verification status.

References

  • Truth anchor: D5/S1/Words/GoldenRecovery/GoldenFactorSecondOrderBinomialRigidity.golden_factor_eq_iff_second_order_profile_eq