isOptimal
plain-language theorem explainer
isOptimal defines a state x to be optimal in display channel C when its stateQuality value is minimal among all states. Order-preservation results in the RRF core cite this definition to equate optimal states across quality-equivalent channels. The definition is a direct universal quantification over the real-valued ordering induced by the channel's composed quality map.
Claim. Let $C$ be a display channel with observation map from states to observations and quality map from observations to reals. A state $x$ is optimal in $C$ if the composed quality of $x$ is at most the composed quality of every other state $y$.
background
A display channel is a structure pairing an observe function from State to Obs with a quality function from Obs to reals; stateQuality is their composition, yielding a direct real-valued measure on states. The module sets display channels as projections for observing states in the RRF framework, relying on the standard ordering of reals from Mathlib. Upstream structures supply physical context: NucleosynthesisTiers.of for discrete phi-tiers of nuclear densities, PhiForcingDerived.of for J-cost, and SpectralEmergence.of for gauge and generation content that populate the State type.
proof idea
This is a direct definition. It sets the predicate to the universal statement that stateQuality of x is less than or equal to stateQuality of every y, using the real ordering imported from Mathlib.
why it matters
The definition anchors comparison of optimal states across channels. It is invoked by isGloballyOptimal on ChannelBundle, by optimal_iff showing equivalence of optimality under QualityEquiv, and by optimal_transfer in OrderPreservation. These results support order preservation for physical projections, consistent with the Recognition Composition Law and the phi-ladder mass formula in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.