Counterfactual Target Minimality

Abstract

Fiber-constant target families factor uniquely through the canonical query-profile image.

Theorem 1.1 (Target families factor through the canonical profile image).

$$\forall M,J,K:\mathrm{Type},Value:J\to \mathrm{Type},Target:K\to \mathrm{Type},queries:\forall j,M\to \mathrm{Set}(\mathrm{Value}(j)),targets:\forall k,M\to \mathrm{Target}(k),\forall k,m,n,\mathrm{queryProfile}(Value,queries,m)=\mathrm{queryProfile}(Value,queries,n)\Rightarrow \mathrm{targets}(k,m)=\mathrm{targets}(k,n)\Rightarrow \forall k,\exists !factor:\mathrm{CounterfactualImage}(Value,queries)\to \mathrm{Target}(k),\mathrm{targets}(k)=factor\circ \mathrm{counterfactualProjection}(Value,queries).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/CanonicalImage/CounterfactualTargetMinimality.target_family_factors_through_cf_image (✓ std3). ∎

Source. Repository-derived.

Commentary.

The query family sends each model to the set of possible values of each query, and queryProfile collects those answers into one canonical profile. CounterfactualImage is the realized image of this profile, with counterfactualProjection as its canonical map.

For every target index, constancy on profile fibers gives a target-valued factor on the image. Surjectivity of the canonical image map makes that factor unique, so all targets in the family descend through the same named image object.

References

• Truth anchor: D5/S3/ConceptDynamics/CanonicalImage/CounterfactualTargetMinimality.target_family_factors_through_cf_image
• Dependency: D5/S3/ConceptDynamics/Sufficiency/UniversalSufficiencyFactorization