Keyboard shortcuts

Press or to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Binary Parikh and Chen Observer

Abstract

The ordered integer matrix product realizes both letter counts and the scattered true-before-false count.

Remark 1.1 (Source-linked mathematical interpretation).

Lean statement: D5/S3/Observer/GoldenChronology/BinaryParikhStepTwoBridge.binary_doubled_magnus_center

Formalization. D5/S3/Observer/GoldenChronology/BinaryParikhStepTwoBridge.binary_doubled_magnus_center (✓ std3).

Source. Repository-derived.

Commentary.

The ordered integer matrix product realizes both letter counts and the scattered true-before-false count.

Its central doubled Magnus coordinate is twice the ordered-pair count minus the product of the two letter counts. Unrestricted binary words retain an explicit collision.

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

References