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
- Truth anchor:
D5/S3/Observer/GoldenChronology/BinaryParikhStepTwoBridge.binary_doubled_magnus_center - Dependency: D5/S3/Observer/Chronology/StepTwoChronologicalSignature