Foundations of Formal Market Microstructure Large in U.S. Equities: Machine-Checked Allocation, Composition, Necessary State, and Regulatory Traceability

This paper develops executable models of price--time priority and parity allocation in U.S. equities to establish when execution consistency holds and which state must be retained. Splitting an order can change who receives shares. In a parity wheel, resetting the rotation between executions can alter allocations even when total incoming quantity is unchanged. A counterexample shows that restarting the wheel between executions can change allocations. Preserving its participant pointer and unfinished lot allowance restores consistency between split and combined quantities on reachable states, under a positive lot size and an admissible first quantity. A further invariant recovers the unused allowance from the cumulative allocation of the current participant. Consequently, when the pointer and aligned cumulative fills are known, the allowance need not be stored independently. The information results distinguish prediction from reconstruction. On specified nondegenerate families sharing an authenticated observation, every summary sufficient to predict future fills must distinguish live pointer positions. The pointer is sufficient once the family is fixed, and a reachable family attains the exact state bound. Separate finite families characterize the additional information required when cumulative fills are unavailable. Supporting results establish allocation feasibility, conservation, priority, one-lot balance, and explicit approximation bounds relating wheel allocations to constrained equal awards. They also yield a conventional analytic limit as lot size vanishes. A decidable price--time checker is characterized by feasibility and seriality, with conformance preserved under sequential execution. Lean 4.22.0 checks 362 theorem declarations using its core library. Axiom dependencies are audited explicitly; the analytic limit is distinguished from the formalized results. A dated regulatory ledger links 58 selected provisions or identified source items to executable definitions and audit records. These mappings support inspection without proving legal interpretation, evidence authenticity, or equivalence to a production exchange. The resulting framework connects allocation mechanisms, persistent state, and reproducible conformance analysis.