Formal Market Microstructure in U.S. Equities II: Observable Conformance, Latent-State Identification, and Clock Uncertainty

This paper develops a formal account of what market data can establish about the execution of an allocation rule. A correct matching algorithm and an observable matching decision are different achievements: a trade total can conceal a priority violation, an unknown wheel position can leave several explanations, and uncertain event order can make different executions observationally compatible. The analysis connects the verified price--time and persistent parity rules of the companion paper to three observation models for U.S. equities. First, transferring a positive fill between resting orders preserves its aggregate total while changing the vector of fills attached to those orders. A total-only projection therefore cannot identify that transfer, whereas an exact depth observation rejects it against an authenticated priority queue. Second, a finite wheel checker searches every rotation and positive allowance in a declared initial family. Its search has exactly $mL$ entries for $m$ participants and lot size $L$; acceptance exhibits an explaining state, and additional executions can only remove candidates. Worked examples show both immediate identification and persistent ambiguity. Third, a clock uncertainty checker compares fills by fixed order identity across admissible queue permutations. Acceptance grows with the uncertainty threshold. For two orders whose swapped allocations differ, masking occurs exactly when their timestamp gap lies within that threshold. An exponential-gap model supplies an analytic masking probability, illustrated by a reproducible simulation. Lean~4.22.0 checks 29 theorem declarations, none depending on classical choice, within an artifact containing 391 declarations. The mathematical guarantees concern the supplied model and inputs. They do not authenticate a feed, reconstruct hidden liquidity, or establish production compliance. The paper specifies the reconstruction and reporting obligations needed to apply its checkers, separates logical compatibility from statistical inference, and provides source code, reproducible figures, and worked instances. No exchange data are analyzed; empirical application requires validated feed reconstruction.