Refinement Monotonicity of Target Risk

Abstract

Factor-map refinement monotonically shrinks target risk.

Theorem 1.1 (Refinement monotonically shrinks target risk).

$$\begin{gathered} \forall X,C,D,T:\mathrm{Type}, \\ {q}_C:X\to C,q_D:X\to D, \\ \mathcal{T}:\mathrm{Set}X\to T, \\ \mathrm{Refines}(q_C,q_D)\Rightarrow \mathrm{targetRisk}(q_D,\mathcal{T})\subseteq \mathrm{targetRisk}(q_C,\mathcal{T}). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/TargetRisk/RefinementTargetRiskMonotonicity.refinement_monotone_target_risk (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public statement uses the family’s frozen factor-map refinement, defect relation, and target-risk definitions. A finer readout cannot create a risky target absent from the coarser readout.

The proof directly applies the risk-inclusion projection of the frozen refinement theorem. The qualitative source remark about typical cost is deliberately outside this boxed theorem.

References

• Truth anchor: D5/S3/ConceptDynamics/TargetRisk/RefinementTargetRiskMonotonicity.refinement_monotone_target_risk
• Dependency: D5/S3/ConceptDynamics/TargetRisk/RefinementRiskCostTradeoff