Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

The original twelve-state marked law

Abstract

The original twelve-state marked law

For every natural radius r, the finite real mass function of the chronological word X(-r) through X(-1) and the two original twelve-state endpoints H(-r), H(0) is formed from the single selected joint law J, including r=0. The corresponding class mass records the same past with Q0=label(H0).

The original hidden-information application derives, for every natural r, that the natural-log conditional information I(H(-r);H(0) given X(-r:-1)) equals log(2)+H(Q0 given X(-r:-1)) and is at least log(2), while its nonnegative series is not summable. The derivation obtains equiprobable hidden lifts from the observation-preserving half-turn of each original cylinder, uses unifilarity on positive support to make the final hidden state a function of the initial state and observed word, and retains zero-mass fibers. This persistent hidden information is separate from the erased-bit defects; the retained tail argument supplies their summable geometric allowance.

Theorem 1.1 (The original one-symbol future probability).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_one

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every original hidden state and Boolean symbol, the length-one futureMass is exactly prob(i,x). This unchanged supplier is used by the native complete-past posterior proof.

Theorem 1.2 (Original empty-word mass).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_empty

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_empty (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every original hidden state i and empty Boolean word, futureMass(marked,i,0,w)=1. TwelveStateFutureRecovery uses the unchanged original empty-word supplier in its actual word-law bridge.

Theorem 1.3 (The actual original word recursion).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_rec

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_rec (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every original hidden state i, Boolean x, natural n and length-n word w, futureMass(marked,i,n+1,cons(x,w)) equals prob(i,x) times futureMass(marked,next(i,x),n,w). TwelveStateFutureRecovery consumes this unchanged supplier in the actual label-word bridge.

Theorem 1.4 (Strict positivity of each original stationary mass).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.mass_pos

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.mass_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every original hidden state i in Bool times Fin 6, mass(i) is strictly positive. This exact existing finite calculation is consumed in the actual support proofs and the all-positive retained-state equivalence in TwelveStateTail.

Theorem 1.5 (The original marked rows are unifilar).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.unifilar

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.unifilar (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every Boolean symbol and original state i, any two successors with strictly positive marked entries are equal. Every nonzero row entry is at next(i,x). TwelveStateTail consumes this original supplier on the retained positive support.

Theorem 1.6 (The explicit length-two affinity bound).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_two_word_affinity

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_two_word_affinity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every original hidden pair i,j with different phase/residue labels, the Bhattacharyya affinity of their actual length-two futureMass distributions is at most sqrt(15)/4. Normalization comes from the existing word_total supplier. Expanding the four length-two words under the actual matrices gives total variation at least one quarter for every such pair. The existing normalized total-variation/Bhattacharyya square inequality then gives this bound. The comparison includes free/free, tail/tail and free/tail pairs and retains both original lifts. TwelveStateTail uses this exact bound on the actual retained quotient.

A hidden state is a phase F or T and an index s modulo six. The rates in index order are 1/4, 1/2, 3/4, 1/4, 1/2, 3/4. Put c=3/62. A free state F(s) emits zero and stays at F(s) with weight 1-p(s), or emits one and moves to T(s+1) with weight p(s). A tail state T(s) emits zero and moves to F(s) with weight one. Every other marked entry is zero. The stationary masses are c/p(s) for F(s) and c for T(s); both original lifts are retained.

Definition 1.7 (The exact stationary parameter).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.parameter

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.parameter (✓ std3).

Source. Repository-derived.

Commentary.

The displayed masses and matrices form a Presentation on Bool times Fin 6. In particular every initial and matrix entry is nonnegative, the initial masses sum to one, the sum of the two marked matrices is stochastic, the initial row is stationary, and the stationary weighted two-one mass is zero. Each initial mass is strictly positive. The free masses 6/31, 3/31, 2/31 are repeated twice; the six tail masses are 3/62. The definition proves these equations for the original twelve states, rather than assuming a six-state law.

Theorem 1.8 (Irreducibility and aperiodicity on the original twelve states).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_hidden_primitivity

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_hidden_primitivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hidden transition A is marked(false)+marked(true), on the original emitted-bit clock. It is a Matrix.IsPrimitive matrix. For every natural n at least twelve and every original hidden pair i,j, the entry (A^n)(i,j) is strictly positive. In particular the original hidden chain is irreducible and aperiodic: every state has positive return probabilities at both lengths twelve and thirteen, and every common divisor of all its positive return lengths must divide their gcd, one.

A zero from any initial phase reaches the free state of the same index. The positive two-edge word 10 advances a free index once around its six-cycle. At most five such advances reach any chosen index. Waiting at a free state has positive weight for every natural duration. A final one reaches the required tail state when necessary. Padding this actual path by free-state zero loops supplies every total length at least twelve; all entries are nonnegative, so each selected path contributes a strictly positive summand to the transition power.

Theorem 1.9 (The actual quotient satisfies the connectivity and distinctness interface).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_quotient_interface

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_quotient_interface (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let B be OriginalUnifilarQuotient.classMatrix(marked). The matrix B(false)+B(true) is Matrix.IsIrreducible, and B is row unifilar. For every integer cut t and every original hidden pair i,j, equality of the conditional measures of the complete future under this same joint law J holds if and only if label(i)=label(j). Thus the actual six future classes have distinct complete future laws; the statement concerns this actual producer and supplies no claim of minimality among all presentations.

The exact existing row_group identity bounds each original marked edge by its outgoing quotient edge. Mapping a positive-length original hidden path along classOf gives a positive-length quotient path, and the primitive original chain therefore gives strong connectivity. The same_law_future_screening supplier is applied directly to the positive original states; its full future-measure equivalence, the retained-class bridge, and future_classes identify equality of the actual complete future measures. No separate full-future wrapper or substitute law is introduced. Together with the existing finite-word nonexactness result, these are the connectivity, unifilarity and probabilistic-distinctness hypotheses relevant to the classical synchronization characterization.

Theorem 1.10 (Exactly six finite-future equivalence classes).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_classes

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.future_classes (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every pair i,j of original hidden states, equality of their futureMass for every natural length and every Boolean word holds if and only if their phases agree and their indices agree modulo three. Thus the classes are the pairs F(s),F(s+3) and T(s),T(s+3), for s=0,1,2. This concerns the selected producer and asserts no minimality among other presentations.

A shared label has equal symbol probabilities and equal successor labels. Induction on word length propagates equality of all future cylinder masses. Conversely, the next-one probability distinguishes free residues and free from tail; the zero-then-one probability distinguishes tail residues. The empty-word cylinder has mass one from every state.

Allowed(b,n,w) tests the no11 condition after a preceding phase b: a preceding tail forbids a first one, and each subsequent one forbids the next one. Legal(n,w) is Allowed(false,n,w), so all open-path no11 words are retained, including the empty word, all-zero words, and words beginning or ending in one. There is no first-to-last constraint. joint is OriginalLawTrimming.jointLaw(parameter); visible is its output pushforward visibleLaw(parameter). These are one stationary bilateral law and its marginal on the original emitted-bit clock.

Theorem 1.11 (Exact positive support after every nonempty word).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_endpoint_support

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_endpoint_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every integer start t, natural n, word w of length n+1, and original hidden state a, the joint real mass of the event consisting of that emitted word and final future class [a] is strictly positive if and only if w is Legal and the phase of a is the last output w(n). Every final residue modulo three occurs. For a legal word ending in zero the supported classes are precisely F(0),F(1),F(2); for one they are precisely T(0),T(1),T(2). An illegal word has zero mass for every final class.

The actual_endpoint_mass and word_quotient identities express the original event mass as the sum over all twelve initial states of their stationary mass times their word weight, selected by the final class. The deterministic marked step agrees with the selected unifilar successor whenever its symbol has positive weight; zero-weight symbols contribute zero. A word has positive path weight exactly when Allowed holds. The residue map of any word is a composition of the identity and the six-cycle advance, hence is onto. Starting from a suitable free state reaches every required final residue with positive weight. The final step sets the phase to the last output, which excludes every class of the other phase.

Taking t=-(n+1) places the endpoint at the fixed hidden time zero, with the observed coordinates from -(n+1) to -1. This gives the exact positive joint cells needed for the finite-past conditional distribution on positive atoms; a conditional-expectation version on completed fields requires its own identification. No division on a null word is used here.

Theorem 1.12 (Full legal output support).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_visible_support

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_visible_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every integer start t, natural length n and Boolean word w of that length, the actual visible cylinder has strictly positive real mass if and only if Legal(n,w). Its mass is the sum of the twelve original stationary initial masses times the respective deterministic word weights. A legal word has a positive path from every free initial state. Conversely, a positive summand has Allowed initial phase and therefore is Legal. This includes length zero and every legal endpoint and seam.

Theorem 1.13 (The exact finite-atom posterior ratio).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_atom_posterior_support

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_atom_posterior_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every integer t, natural n, word w of length n+1 with positive actual visible-cylinder mass, and original state a, atomPosterior is the joint word/final-class mass divided by that same visible-cylinder mass. This ratio is strictly positive if and only if the phase of a is the last symbol w(n). Thus its support consists of exactly three future classes, each including both original hidden lifts. Only a positive denominator is used; a null word receives no conditional assertion.

Theorem 1.14 (No positive finite synchronizing word).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.no_synchronizing_word

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.no_synchronizing_word (✓ std3). ∎

Source. Repository-derived.

Commentary.

HasSynchronizingWord means that some integer start t, natural length n and Boolean word w have positive actual visible-cylinder mass and that there is one future class a such that every class with positive joint word/final-class mass equals a. The theorem is the literal negation of this property. At length zero the distinct free residues zero and one both have positive mass. At positive length, the last output selects the phase, and final residues zero and one again give two distinct positive classes. Their distinction follows from equality of future laws being equivalent to equality of phase and residue modulo three. Hence no finite positive word has a singleton final-class support.

This is a direct finite-word obstruction for the actual quotient. It does not assert hidden-state or presentation minimality. The separate original-chain primitivity and actual quotient connectivity results above supply their stated structural hypotheses.

Theorem 1.15 (All six classes remain possible at radius zero).

Lean statement: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_empty_support

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/TwelveStatePresentation.actual_empty_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every integer t and every original hidden state a, the empty-word endpoint event with future class [a] has strictly positive joint real mass. Its class contains the positive stationary mass of a. Together with the six-class characterization this gives all six possible classes for the empty observation.

References