ChannelEquiv
plain-language theorem explainer
Channel equivalence equates two display channels when they induce identical orderings on states of a given type. Glossary users in RRF modeling cite it to enforce observational invariance across vantage points or octaves. The abbreviation is a direct one-line wrapper to QualityEquiv with no additional derivation or lemmas.
Claim. Two observation channels $Obs_1$ and $Obs_2$ are equivalent relative to states of type $State$ precisely when they induce the same ordering on those states, written $ChannelEquiv(State, Obs_1, Obs_2) := QualityEquiv(State := State, Obs_1 := Obs_1, Obs_2 := Obs_2)$.
background
The RRF Core Glossary supplies canonical names for the Reality Recognition Framework. DisplayChannel denotes a way of observing states, while Vantage supplies the three perspectives {inside, act, outside} and Octave a scale of manifestation. Strain is the deviation from balance measured by the J-cost functional, with ledger closure enforcing debit-credit equality. The local setting is the single source of truth for RRF vocabulary so that all modules reference the same symbols for recognition pairing R, strain minimization, and consistent observation across channels.
proof idea
One-line wrapper that applies QualityEquiv with the three type parameters instantiated directly.
why it matters
The abbreviation anchors channel invariance inside the RRF consistency conditions (low strain, closed ledger, consistent observation across channels). It supports the framework landmarks of recognition as the fundamental act and the requirement that real states satisfy ledger closure and strain minimization. No downstream uses are recorded, leaving its role as a standardization point for later multi-channel or vantage-dependent arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.