SingleChannelConservation
plain-language theorem explainer
Packages a physics framework with one independent conserved real quantity on its state space, a reference state where that quantity is strictly positive, and invariance under evolution. Cited by anyone extracting a dimensionless positive ratio interface or proving Bridge B3 (zero free parameters plus single-channel conservation). Pure structure definition: four fields, no proof obligations beyond the positivity and conservation hypotheses.
Claim. A physics framework $F$ with state space $S$ and evolution map $\mathrm{evolve}:S\to S$ carries single-channel conservation when there exist $Q:S\to\mathbb{R}$ and a reference state $s_0\in S$ such that $Q(s_0)>0$ and $Q(\mathrm{evolve}(s))=Q(s)$ for every $s\in S$.
background
The ambient setting is the exclusivity verification layer: abstract physics frameworks are compared by what dimensionless observables and free parameters they admit. A PhysicsFramework supplies a carrier type of states, an evolution operator, and observable extraction; that is the minimal interface needed to "do physics" in this module.
Single-channel conservation formalizes the ledger idea that exactly one independent real quantity is conserved. The conserved map $Q$ is not required to be unique as a function, only that the framework presents one such channel with a positive reference value. Evolution is the framework's own dynamics map, not the thermodynamic J-descent iterator from the second-law module; the name collision is incidental.
Downstream, the ratio $Q(s)/Q(s_0)$ becomes the canonical dimensionless observable once zero free real knobs are also assumed. That is the content of Bridge B3 in this file.
proof idea
No proof: this is a structure definition. It bundles four fields on a physics framework $F$: a real-valued map on states, a chosen reference state, a positivity witness at that reference, and a universal equality asserting that evolution leaves the map invariant. Inhabitants are constructed by supplying those data; lemmas that consume the structure unfold the fields directly.
why it matters
This is the conservation half of Bridge B3. Downstream, ratio_from_conservation builds the dimensionless ratio $Q(s)/Q(s_0)$, ratio_pos_of_conservation shows the ratio is positive whenever $Q$ is everywhere positive, and bridge_B3_single_channel_forces_ratio combines strong zero-parameter hypotheses with this structure to force a positive dimensionless ratio interface on the state space.
In Recognition Science terms, a single conserved ledger channel is what lets dimensionless observables factor through a one-dimensional ratio rather than an open parameter surface. That is the exclusivity move: frameworks with free real knobs or multi-channel conservation fall outside the forced interface. The structure itself does not invoke the T0–T8 chain or the Recognition Composition Law; it is a verification-side interface that those foundations are expected to inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.