Sufficiency of the Foundational-Layer Restriction

The semantic sufficiency direction of se100.constraint.Neutrality: under Referential Common Ground, restricting the foundational layer to referential commitments and permitted attribution propositions makes the substrate neutral.

Extension stability follows by generalized cut: every member of the substrate's commitment theory is, by the restriction, entailed by the referential commitments, which Referential Common Ground keeps consistent with every admissible framework. Interpretive non-commitment then follows from se100.remark.PropertyRelation.

This does not establish neutrality by design. NeutralByDesign ranges over an arbitrary DesignTimeGuaranteeSystem and requires a permitted basis. Discharging that wrapper is left to a canonical design-time-guarantee realization.

theorem SE.NeutralSubstrate.Neutrality.extensionStability_of_restricted_of_commonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hrestricted : FoundationalLayerRestrictedToPermittedClasses C S F A B s) (hcommonGround : Assumptions.ReferentialCommonGround C S F A B s M) : ExtensionStability C S s M

Under Referential Common Ground, a foundational layer restricted to the permitted classes yields extension stability.

theorem SE.NeutralSubstrate.Neutrality.neutral_of_restricted_of_commonGround {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : Attribution.AttributionSystem L} {B : Attribution.AttributionalBasisFixing C A} {s : S.Carrier} {M : Framework.FrameworkSystem L.carrier} (hrestricted : FoundationalLayerRestrictedToPermittedClasses C S F A B s) (hcommonGround : Assumptions.ReferentialCommonGround C S F A B s M) : Neutral C S s M

Under Referential Common Ground, a foundational layer restricted to the permitted classes is neutral.