ChannelCoherence
ChannelCoherence packages an indexed family of display functors on a VantageCategory together with the requirement that all channels induce identical strict orderings on quality for every pair of states. Researchers formalizing vantage equivalence in the RRF setting cite it when showing that strain orderings are independent of the chosen observation channel. The declaration is a direct structure definition that assembles the family and the pairwise coherence predicate with no lemmas or tactics.
claimA structure on a vantage category $V$ consisting of a function from natural numbers to pairs (observation type, display functor on $V$) together with the axiom that for all indices $i,j$ and states $x,y$ the inequality quality$_i$(observe$_i(x)$) > quality$_i$(observe$_i(y)$) holds if and only if the same inequality holds for channel $j$.
background
The module defines the categorical structure making the three vantages (Inside, Act, Outside) formally equivalent via functors that preserve the strain functional $J$. A VantageCategory consists of a type of states, a type of transitions, identity and composition operations, and the strain functional $J$ that assigns a real cost to each state. A DisplayFunctor on $V$ supplies an observation map from states to some type Obs together with a quality map from Obs to reals that is monotonically non-increasing with respect to $J$ (higher strain yields lower or equal quality).
proof idea
The declaration is a structure definition that directly assembles the indexed family of DisplayFunctors and the coherence predicate on their quality orderings; no lemmas are applied and no tactics are used.
why it matters in Recognition Science
ChannelCoherence supplies the coherence hypothesis required by the downstream theorem one_J_thesis_coherent, which states that coherent channels preserve quality orderings across all indices. It fills the role of ensuring that the strain functional $J$ yields a unique quality ordering independent of display channel, supporting the module claim that physics, meaning, and qualia are three views of one structure. The construction connects to the Recognition Science program of deriving all physics from the $J$ functional and the equivalence of vantages.
scope and limits
- Does not assert existence of any display functors.
- Does not constrain the number of channels beyond the indexed family.
- Does not relate channels to concrete physical observables.
- Does not prove monotonicity of quality; that property is inherited from each DisplayFunctor.
Lean usage
theorem one_J_thesis_coherent (V : VantageCategory) (coh : ChannelCoherence V) (i j : ℕ) (x y : V.State) : (coh.channel i).2.quality ((coh.channel i).2.observe x) > (coh.channel i).2.quality ((coh.channel i).2.observe y) ↔ (coh.channel j).2.quality ((coh.channel j).2.observe x) > (coh.channel j).2.quality ((coh.channel j).2.observe y) := by sorryformal statement (Lean)
232structure ChannelCoherence (V : VantageCategory) where
233 /-- Indexed family of channels. -/
234 channel : ℕ → Σ (Obs : Type*), DisplayFunctor V Obs
235 /-- All channels agree: if x is better than y in channel i, same in channel j. -/
236 coherent : ∀ i j : ℕ, ∀ x y : V.State,
237 (channel i).2.quality ((channel i).2.observe x) >
238 (channel i).2.quality ((channel i).2.observe y) ↔
239 (channel j).2.quality ((channel j).2.observe x) >
240 (channel j).2.quality ((channel j).2.observe y)
241
242/-! ## The One J Thesis -/
243
244/-- The One J Thesis (weak form): lower strain implies higher or equal quality.
245
246This is provable from the monotonicity constraint.
247-/