total_Z
plain-language theorem explainer
Defines the total Z-charge of a ledger state as the constant integer zero. Anyone wiring recognition-operator bookkeeping can cite it as the present placeholder for net Z. The body is a one-line constant definition that ignores its state argument.
Claim. For every ledger state $s$ (here an eight-signal configuration), the total $Z$-charge is the integer $0$: $\mathrm{total\_Z}(s) := 0$.
background
In this module a ledger state is abbreviated to an eight-signal configuration (Signal8), the discrete carrier for the recognition operator. Sibling fields on that state include Z-patterns, global phase, channels, and active bonds; total_Z is the scalar that is meant to aggregate net Z over the state.
Related ledger notions elsewhere in the monolith already carry conserved totals: the variational ledger tracks total log-ratio as charge preserved under evolution, the information ledger sums recognition-event cost, and the thermodynamic ledger sums recognition cost over active bonds. The present definition sits in that family but is not yet computed from those fields.
The module imports complex-structure forcing, so the ambient setting is the foundation layer that forces complex structure and the recognition operator on discrete ledger data.
proof idea
No proof. The declaration is a definition whose right-hand side is the integer literal 0; the ledger-state argument is unused (explicitly underscored). There are no lemmas, tactics, or reductions.
why it matters
Gives a named total-Z hook on the recognition-operator ledger so downstream operator and conservation statements can mention net Z without inventing a local constant. In the broader Recognition Science ledger picture, totals of this kind are the conserved charges (log-ratio, information cost, recognition cost); a nontrivial total Z would sit beside those once Z-patterns and bond data are wired in.
No downstream uses are recorded yet, and the body is the zero stub, so the declaration currently only reserves the interface. It does not itself advance the forcing chain (T0–T8), RCL, or the mass/alpha formulae; it is bookkeeping scaffolding inside Foundation.RecognitionOperator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.