Z_patterns
plain-language theorem explainer
On any ledger state the Z-pattern list is defined to be empty. Bridge and RecognitionOperator code that still asks for integer Z-labels from a configuration can call this accessor and get a well-typed nil list. The body is a constant definition: no computation on the state.
Claim. For every ledger state $s$, the associated list of integer $Z$-patterns is the empty list.
background
In this module a ledger state is an abbreviation for the eight-channel signal type forced by the complex-structure development (the eight-tick octave). The surrounding namespace exposes a thin compatibility surface so older bridge modules can still read fields such as time, channels, active bonds, and Z-patterns off a ledger state.
Upstream, other modules define richer ledger states: finite lists of recognition events, $N$-entry configurations with a tick index and conserved total log-ratio, or thermodynamic states with active bonds and positive multipliers. Here those structures are not used; the local state type is just the eight-channel signal, and Z_patterns is a stub accessor on it.
The name recalls the integer $Z$ labels that appear elsewhere in Recognition Science (atomic number, charge rung, $Z_{\mathrm{cf}}=\varphi^5$), but this definition does not yet extract any such labels from the signal.
proof idea
Constant definition. The ledger-state argument is ignored and the value is the empty list of integers. No lemmas are applied.
why it matters
Keeps the legacy RecognitionOperator ledger API total: callers that pattern-match or fold over Z-patterns still type-check while the real extraction is unfinished. Downstream the eight-channel signal abbreviation and the compatibility surface sit on top of this namespace. Until a non-empty implementation is supplied, nothing in the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$) or the mass ladder depends on the returned list. It is a placeholder, not a physical claim about charge or rung structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.