Descriptive and Normative Structure Separation

Abstract

One descriptive structure admits incompatible normative extensions.

Theorem 1.1 (Descriptive structure does not uniquely determine norms).

$$\begin{gathered} \forall State,Action,Description:\mathrm{Type}, \\ descriptive:\mathrm{DescriptiveStructure}(State,Action,Description),action:Action, \\ \exists M_1,M_2:\mathrm{NormativeExtension}(State,Action,Description), \\ \mathrm{Desc}(M_1)=descriptive\wedge \mathrm{Desc}(M_2)=descriptive\wedge \\ (\forall x:State,u:Action,\mathrm{Permitted}(M_1)(x)(u))\wedge \\ (\forall x:State,u:Action,\neg \mathrm{Permitted}(M_2)(x)(u))\wedge \\ \mathrm{Permitted}(M_1)\ne \mathrm{Permitted}(M_2)\wedge \\ \forall I:\mathrm{DescriptiveStructure}(State,Action,Description)\to \left(State\to \left(Action\to \mathrm{Prop}\right)\right),\neg (I(descriptive)=\mathrm{Permitted}(M_1)\wedge I(descriptive)=\mathrm{Permitted}(M_2)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/NormativeStructure/DescriptiveNormativeSeparation.descriptive_structure_does_not_uniquely_determine_norms (✓ std3). ∎

Source. Repository-derived.

Commentary.

The descriptive record contains the state carrier, physical-admissibility predicate, state-action process, concept readout, and anchored state. A normative extension independently adds a permission predicate on state-action pairs.

The first constructed model permits every state-action pair; the second permits none. Both carry exactly the supplied descriptive record, but their permission predicates differ at the public anchor and action witness.

Consequently no single function of that shared descriptive record can equal both normative predicates. All model-separation clauses and the explicit failure of unique descriptive inference occur in the public theorem.

The source proof itself uses the all-true and all-false predicates, so the formal nontriviality is their genuine normative distinction rather than an invented requirement that each predicate be nonconstant.

Repository and pinned-library searches found no exact theorem or canonical normative-extension carrier packaging this construction.

References

• Truth anchor: D5/S3/ConceptDynamics/NormativeStructure/DescriptiveNormativeSeparation.descriptive_structure_does_not_uniquely_determine_norms
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition