Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DecisionValueScale/NormativeScaleChoiceReversalWithMeta.normative_scale_choice_reversal_with_metanormative_data (✓ std3). ∎
Source. Repository-derived.
Commentary.
The public carrier is exactly two Boolean doctrines and two Boolean actions, with real-valued utility and probability functions. Both doctrine probabilities are one half, and each doctrine’s coordinates preserve its strict internal ranking under two positive utility scales.
The displayed weighted sums evaluate to alpha over two and beta over two. The first scale therefore selects action true while the second selects action false, exposing the cross-theory scale dependence rather than hiding it in a definition.
MetaNormativeData is an independent source primitive carrying cross-theory scale, rights priority, worst-case and regret scores, and the two doctrine permission predicates. The final implication states directly that an empty permission intersection licenses no universally permitted action.
Repository and pinned-library searches found only the frozen arithmetic reversal theorem, which lacks the metanormative carrier and permission-intersection clause; no exact combined theorem was found.