Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Full Marginals Do Not Determine a Joint Domain

Abstract

An exact dependent diagonal refutes the universal full-marginal claim.

Theorem 1.1 (The joint domain contains exactly two diagonal worlds).

Lean statement: D5/S3/ConceptDynamics/SpacetimeWorld/JointMarginalBoundary.diagonal_exact

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeWorld/JointMarginalBoundary.diagonal_exact (✓ std3). ∎

Source. Repository-derived.

Commentary.

Values are the integer subtype containing exactly one and two. Pair notation is connected by an explicit equivalence to dependent valuations on the union of two singleton name sets. Formula projection is omitted; the resolving Lean declaration is the mathematical statement.

Theorem 1.2 (Both dependent marginal images are full).

Lean statement: D5/S3/ConceptDynamics/SpacetimeWorld/JointMarginalBoundary.diagonal_local_marginals

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeWorld/JointMarginalBoundary.diagonal_local_marginals (✓ std3). ∎

Source. Repository-derived.

Commentary.

The diagonal has full coordinate images and full images in the actual local valuation types. Both crossed worlds are excluded, and the diagonal is a strict subset of the natural join. Formula projection is omitted; the resolving Lean declaration is the mathematical statement.

Theorem 1.3 (Distinct names and full marginals do not force the natural join).

Lean statement: D5/S3/ConceptDynamics/SpacetimeWorld/JointMarginalBoundary.diagonal_joint_refutation

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/SpacetimeWorld/JointMarginalBoundary.diagonal_joint_refutation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The closed universal claim quantifies over disjoint name sets and nonempty domains with full local marginal images. The exact diagonal refutes that claim. The finite facts support this refutation; they are not separate positive instance deposits. Formula projection is omitted; the resolving Lean declaration is the mathematical statement.

References