Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Directly Provable DECT Laws With One Open Clause

Abstract

Eight direct DECT laws are packaged; source clause six remains open.

Theorem 1.1 (Eight direct laws for definition escape and completion).

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeLaws/DirectlyProvableLaws.directly_provable_laws (✓ std3). ∎

Source. Repository-derived.

Commentary.

The theorem contains source clauses one through five and seven through nine, in that order: residual intersection; sufficiency-factorization; zero gain from a redundant definition; blind-kernel impossibility; finite-object compactness; the prepared one-step defect identity; the semigroup defect identity; and the approximate cascade triangle bound. Source clause six is not a conjunct.

The first conjunct applies residual_join_law. The second uses the same fiber-constancy equivalence packaged by target_recovery_criterion, including the empty-state case without adding an inhabitedness premise. The third assumes exactly that the added definition is constant on every fiber of the baseline readout. It does not assert a total codomain map outside the baseline readout’s image. An Empty-state example satisfies this fiber condition while Refines is false, pinning the weaker premise used by the conjunct. The fourth uses the new dependent-family obstruction; its residual witness supplies the inhabited state needed by the canonical recovery criterion.

The canonical defectRelation is the only target residual throughout. Clauses four and five use dependentBlindResidual and dependentLanguageExtension because package members may have different codomains. On a constant codomain these are definitionally equal to the frozen blindResidual and languageExtension, as proved by the three specialization bridge theorems. The existing jointKernel and jointReadout remain the family primitives. For finite X, each baseline defect pair is assigned a package definition that separates it; enumeration of the finite subtype then gives a finite sufficient extension.

CAS section 4.4 defines M(S) as remaining mass, defines F(S) as M(empty) minus M(S), and then identifies F with captured mass. Those statements are incompatible with unrestricted infinite values. The compiled theorem infinite_counting_cas_bridge_fails uses the canonical defectRelation on (Nat times Bool) pairs and the complement of the Prod.snd kernel. It proves that the residual, remaining relation, and captured cut have the source-prescribed relation shape. M(empty) and M(singleton) are both infinity, so ENNReal subtraction makes F(singleton) zero while captured mass is infinity. Clause six remains open under TASK D5-T0049 and is not represented by a constant data declaration. The sixth displayed conjunct is source clause seven, the seventh is source clause eight, and the eighth is source clause nine.

The companion DirectlyProvableLawWitnesses module gives ten named and mechanically consumed checks: Boolean models witness a nonempty residual, redundant zero gain, a blind obstruction, and finite closure by one identity definition; coordinate swap gives nonzero prepared and semigroup defects; and the real identity map attains the cascade bound. Its adjacent strict capture example is not source clause six. Nine named false-neighbor declarations remain in this module; the sixth records only the bridge failure and the other eight negate nearby strengthened or premise-weakened statements.

References