Sensitive Leakage Monotonicity

Abstract

Joining a fixed sensitive readout preserves concept refinement.

Theorem 1.1 (Sensitive leakage is monotone under refinement).

$$\forall X\in \mathrm{Type},A\in \mathrm{Type},B\in \mathrm{Type},K\in \mathrm{Type},C\in X\to A,D\in X\to B,S\in X\to K,\mathrm{Refines}\left(C,D\right)\Rightarrow \mathrm{Refines}\left(\mathrm{conceptJoin}\left(C,S\right),\mathrm{conceptJoin}\left(D,S\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Disclosure/SensitiveLeakageMonotonicity.sensitive_leakage_monotone (✓ std3). ∎

Source. Repository-derived.

Commentary.

The current, refined, and sensitive readouts are independent public parameters. The premise says that the current readout factors through the refined one.

Both leakage objects are constructed with the canonical joint readout. The frozen augmentation law preserves the refinement while carrying the same sensitive coordinate on both sides.

References

• Truth anchor: D5/S3/ConceptDynamics/Disclosure/SensitiveLeakageMonotonicity.sensitive_leakage_monotone
• Dependency: D5/S3/ConceptDynamics/Dependency/BasicDependencyRules