# Permitted Attribution Propositions

This module formalizes:

• se100.def.PermittedAttributionProposition — Permitted Attribution Proposition

An attribution proposition asserts x φ is permitted at the foundational layer when the attributional basis for x's assertion of φ is semantically fixed by the substrate's referential commitments.

An attributional basis may involve the source, assertion occurrence, provenance, content reference, and other information needed to identify what was asserted, by whom, and under what record basis. The presence of such records does not by itself establish that the attributional basis is fixed. That determination remains an explicit semantic judgment.

A fixed attributional basis must support entailment of the corresponding attribution proposition. This commits the substrate to the attribution asserts x φ, not to the asserted proposition φ.

In particular, attribution does not by itself establish or endorse:

• the truth of φ;
• substrate commitment to φ;
• framework commitment to φ;
• denotation or co-reference of expressions occurring in φ; or
• the authority, correctness, or evidentiary adequacy of the source's claim.

The structure of an attributional basis remains abstract. No finiteness, enumeration, decidability, or computational representation is assumed.

structure SE.NeutralSubstrate.Attribution.AttributionalBasisFixing {L : Logic.Language.PropositionalLanguage} (C : Logic.ConsequenceSystem L) (A : AttributionSystem L) : Type (max u x)

An abstract account of when an attributional basis is semantically fixed by a commitment theory.

fixedBy T x φ states that T fixes the attributional basis required to identify x's assertion of φ.

Concrete realizations may use source identifiers, assertion records, provenance, content references, or other records in determining this judgment. Their presence alone does not establish fixedBy.

The second field explicitly requires a fixed attributional basis to support entailment of the corresponding attribution proposition. It does not entail or endorse the asserted proposition φ.

• fixedBy : Logic.Theory.CommitmentTheory L.carrier → A.Source → L.Proposition → Prop

  Whether a commitment theory semantically fixes the attributional basis for a source's assertion of a proposition.

• entailsAssertsOfFixedBy {T : Logic.Theory.CommitmentTheory L.carrier} {source : A.Source} {φ : L.Proposition} : self.fixedBy T source φ → C.entails T (A.asserts source φ)

  A commitment theory that fixes an attributional basis entails the corresponding attribution proposition.

  This conclusion concerns A.asserts source φ, not φ.

def SE.NeutralSubstrate.Attribution.PermittedAttributionProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} (C : Logic.ConsequenceSystem L) (S : Substrate.SubstrateSystem L R) (F : Substrate.ReferentialFixing L R) (A : AttributionSystem L) (B : AttributionalBasisFixing C A) (s : S.Carrier) (p : L.Proposition) : Prop

An attribution proposition is permitted at the foundational layer when its attributional basis is semantically fixed by the substrate's referential commitments.

Permission applies to the attribution proposition itself and introduces no commitment to the asserted proposition.

Equations

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

@[simp]

theorem SE.NeutralSubstrate.Attribution.permittedAttributionProposition_iff {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : AttributionSystem L} {B : AttributionalBasisFixing C A} {s : S.Carrier} {p : L.Proposition} : PermittedAttributionProposition C S F A B s p ↔ ∃ (source : A.Source), ∃ (φ : L.Proposition), p = A.asserts source φ ∧ B.fixedBy (Substrate.ReferentialCommitments C S F s) source φ

A proposition is permitted exactly when it is an attribution proposition whose attributional basis is semantically fixed by the substrate's referential commitments.

theorem SE.NeutralSubstrate.Attribution.attributionProposition_of_permittedAttributionProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : AttributionSystem L} {B : AttributionalBasisFixing C A} {s : S.Carrier} {p : L.Proposition} (hp : PermittedAttributionProposition C S F A B s p) : AttributionProposition A p

Every permitted attribution proposition is an attribution proposition.

theorem SE.NeutralSubstrate.Attribution.referentialCommitments_entails_of_permittedAttributionProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : AttributionSystem L} (B : AttributionalBasisFixing C A) {s : S.Carrier} {p : L.Proposition} (hp : PermittedAttributionProposition C S F A B s p) : C.entails (Substrate.ReferentialCommitments C S F s) p

The substrate's referential commitments entail every permitted attribution proposition.

The entailed proposition is the attribution itself, not its asserted content.

theorem SE.NeutralSubstrate.Attribution.substrateCommitment_of_permittedAttributionProposition {L : Logic.Language.PropositionalLanguage} {R : Referent.ReferentCarriers} {C : Logic.ConsequenceSystem L} {S : Substrate.SubstrateSystem L R} {F : Substrate.ReferentialFixing L R} {A : AttributionSystem L} (B : AttributionalBasisFixing C A) {s : S.Carrier} {p : L.Proposition} (hp : PermittedAttributionProposition C S F A B s p) : Substrate.SubstrateCommitment C S s p

Every permitted attribution proposition is a substrate-layer commitment.

This follows by generalized cut: the substrate entails every member of its referential commitments, and those referential commitments entail the permitted attribution proposition.

The resulting substrate commitment remains a commitment to the attribution, not to the proposition attributed to the source.