Characterization Hypothesis

This module formalizes:

• se100.remark.CharacterizationHypothesis - Characterization as an Explicit Hypothesis

The semantic sufficiency direction of se100.constraint.Neutrality is proved in SE.NeutralSubstrate.Neutrality.Sufficiency.

This module states, as an explicit hypothesis on a realization, that for a substrate intended to remain usable by the complete intrinsic class of admissible frameworks, and under Contestability and Referential Common Ground, neutrality by design is equivalent to restricting the foundational layer to:

• referential commitments; and
• permitted attribution propositions.

The hypothesis also records the resulting exclusion of object-level causal or normative commitments.

It is not asserted to follow from the minimal consequence-system interfaces alone; the theorems below derive consequences under it.

def SE.NeutralSubstrate.NoObjectLevelCausalOrNormativeCommitment {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (K : Classification.CausalNormativeClassification L) (c : K.Context) (A : Attribution.AttributionSystem L) (I : Interpretation.ObjectLevelInterpretation L R) (S : Substrate.SubstrateSystem L R) (s : S.Carrier) : Prop

A substrate makes no object-level causal or normative commitment when no proposition satisfies the corresponding commitment predicate in the selected accountability context.

Equations

• SE.NeutralSubstrate.NoObjectLevelCausalOrNormativeCommitment C K c A I S s = ∀ (p : L.Proposition), ¬SE.NeutralSubstrate.Interpretation.ObjectLevelCausalOrNormativeCommitment C K c A I S s p

def SE.NeutralSubstrate.CharacterizationHypothesis {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (K : Classification.CausalNormativeClassification L) (c : K.Context) (G : Classification.InterpretiveStatusFixing L K.Context) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (A : Attribution.AttributionSystem L) (B : Attribution.AttributionalBasisFixing C A) (I : Interpretation.ObjectLevelInterpretation L R) (s : S.Carrier) (M : Framework.FrameworkSystem L.carrier) (D : DesignTimeGuaranteeSystem) : Prop

The characterization hypothesis states that, under Contestability and Referential Common Ground:

1. neutrality by design is equivalent to restriction of the foundational layer to referential commitments and permitted attribution propositions; and
2. that restriction excludes every object-level causal or normative commitment.

It is an explicit condition on a realization, not a theorem. The design-time guarantee ranges over the complete intrinsic framework class through NeutralByDesign; it does not depend on framework enumeration.

Equations

• One or more equations did not get rendered due to their size.

theorem SE.NeutralSubstrate.neutralByDesign_iff_foundationalLayerRestricted {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {G : Classification.InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {I : Interpretation.ObjectLevelInterpretation L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hcharacterization : CharacterizationHypothesis C K c G S F A B I s M D) (hcontestability : Assumptions.Contestability C K c G S F s M D) (hcommonGround : Assumptions.ReferentialCommonGround C S F A B s M) : Neutrality.NeutralByDesign C S s M D ↔ FoundationalLayerRestrictedToPermittedClasses C S F A B s

Under the characterization hypothesis, Contestability, and Referential Common Ground, neutrality by design is equivalent to restriction of the foundational layer to the permitted classes.

theorem SE.NeutralSubstrate.noObjectLevelCommitment_of_foundationalLayerRestricted {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {G : Classification.InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {I : Interpretation.ObjectLevelInterpretation L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hcharacterization : CharacterizationHypothesis C K c G S F A B I s M D) (hcontestability : Assumptions.Contestability C K c G S F s M D) (hcommonGround : Assumptions.ReferentialCommonGround C S F A B s M) (hrestricted : FoundationalLayerRestrictedToPermittedClasses C S F A B s) : NoObjectLevelCausalOrNormativeCommitment C K c A I S s

Under the characterization hypothesis, restriction to the permitted foundational classes excludes object-level causal or normative commitments.

theorem SE.NeutralSubstrate.noObjectLevelCommitment_of_neutralByDesign {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {K : Classification.CausalNormativeClassification L} {c : K.Context} {G : Classification.InterpretiveStatusFixing L K.Context} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {I : Interpretation.ObjectLevelInterpretation L R} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} {D : DesignTimeGuaranteeSystem} (hcharacterization : CharacterizationHypothesis C K c G S F A B I s M D) (hcontestability : Assumptions.Contestability C K c G S F s M D) (hcommonGround : Assumptions.ReferentialCommonGround C S F A B s M) (hdesign : Neutrality.NeutralByDesign C S s M D) : NoObjectLevelCausalOrNormativeCommitment C K c A I S s

Under the characterization hypothesis, a substrate that is neutral by design makes no object-level causal or normative commitment.