Dimension Coherence via the Mereological Category

Upgrades the dimension irrelevance results in DimensionBridge.lean to formal coherence theorems using the categorical structure from MereoCat.lean.

The key claim is QUA functoriality: QUA pullback respects categorical composition in MereoObj. Any DimensionChain — temporal, spatial, object, or any future chain not yet defined — produces a morphism in the mereological category, and QUA pulls back through it. This makes dimension irrelevance a consequence of functoriality rather than a per-chain verification.

Three levels of coherence

1. Per-chain: Each DimensionChain produces a MereoMor (proved in MereoCat.lean via DimensionChain.toMereoMor).

2. Cross-chain: Given any two chains ending at the same measure type, QUA pulls back through both (dimension_coherence). This is the formal content of "the dimension doesn't matter."

3. Falsifiable prediction: Any future DimensionChain (e.g., a new perceptual or information-theoretic dimension) must automatically satisfy QUA transfer (any_chain_qua_transfer). If empirically it doesn't, the MereoDim axiom for that dimension is falsified.

Composition coherence

The categorical composition leg₁ ≫ leg₂ in MereoObj equals the composite morphism toMereoMor (DimensionChain.comp_eq in MereoCat.lean). This guarantees that the two-step QUA transfer (first through leg₁, then through leg₂) agrees with the one-step transfer through the composition.

theorem Semantics.Events.DimensionCoherence.dimension_coherence {Source₁ Inter₁ Source₂ Inter₂ Measure : Type u} [PartialOrder Source₁] [PartialOrder Inter₁] [PartialOrder Source₂] [PartialOrder Inter₂] [PartialOrder Measure] {f₁ : Source₁ → Inter₁} {μ₁ : Inter₁ → Measure} {f₂ : Source₂ → Inter₂} {μ₂ : Inter₂ → Measure} (dc₁ : Mereology.DimensionChain f₁ μ₁) (dc₂ : Mereology.DimensionChain f₂ μ₂) {P : Measure → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ μ₁ ∘ f₁) ∧ Mereology.QUA (P ∘ μ₂ ∘ f₂)

Dimension coherence: given two arbitrary dimension chains with a common measure type, QUA on the measure pulls back through both chains.

This is the formal content of dimension irrelevance: the QUA property of the pullback predicate depends only on the QUA property of the source predicate and the existence of MereoDim legs, not on which particular dimension chain is chosen.

theorem Semantics.Events.DimensionCoherence.any_chain_qua_transfer {Source Inter Measure : Type u} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : Mereology.DimensionChain f μ) {P : Measure → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ μ ∘ f)

Falsifiable prediction: any DimensionChain — including ones not yet defined — must satisfy QUA transfer.

If a linguist proposes a new mereological dimension (e.g., a perceptual salience chain Events →p Percepts →σ ℝ) and claims both legs are MereoDim, then QUA must pull back through it. If empirical data shows QUA fails for the pullback predicate, the MereoDim assumption for one of the legs is falsified.

theorem Semantics.Events.DimensionCoherence.two_step_agrees_with_composite {Source Inter Measure : Type u} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : Mereology.DimensionChain f μ) {P : Measure → Prop} (hP : Mereology.QUA P) : have one_step := ⋯; have two_step_inter := ⋯; have two_step_source := ⋯; one_step = two_step_source

The two-step QUA transfer (through leg₁ then leg₂) agrees with the one-step transfer through the composite morphism. This follows from DimensionChain.comp_eq: the composite MereoMor equals the categorical composition of the legs.

theorem Semantics.Events.DimensionCoherence.mereoMor_qua_pullback {A B : Core.Categorical.MereoObj} (m : Core.Categorical.MereoMor A B) {P : B.α → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ m.toFun)

Every MereoMor morphism supports QUA pullback. This is the functorial action: MereoMor A B → (QUA P → QUA (P ∘ f)).

theorem Semantics.Events.DimensionCoherence.mereoMor_comp_qua_pullback {A B C : Core.Categorical.MereoObj} (f : Core.Categorical.MereoMor A B) (g : Core.Categorical.MereoMor B C) {P : C.α → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ (f.comp g).toFun)

Composing two MereoMor morphisms preserves QUA pullback: pulling back through g ∘ f equals pulling back through f after pulling back through g.

theorem Semantics.Events.DimensionCoherence.licensing_factors_through_boundedness : Mereology.quaBoundedness.isLicensed = true ∧ Mereology.cumBoundedness.isLicensed = false

The licensing prediction (QUA → closed → licensed vs CUM → open → blocked) is invariant across all dimension chains. This is the theorem that DimensionBridge.dimension_irrelevance establishes pointwise; here we note that the categorical structure makes it structural.

No matter how many new dimension chains are added, the licensing prediction factors through Boundedness.isLicensed, which depends only on QUA/CUM — not on the particular chain.