Semantic Overreach Legacy Bridge

Abstract

Semantic overreach is exactly its legacy propositional image.

Theorem 1.1 (Semantic overreach descends exactly to legacy overreach).

$$\begin{array}{c}\forall S,report,J,\\ \mathrm{SemanticOverreach}\left(S,report,J\right)⟺\\ \mathrm{Overreach}\left(S.toLegacy,report,J\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscapeSemantics/SemanticOverreachLegacyBridge.semantic_overreach_iff_overreach (✓ std3). ∎

Source. Repository-derived.

Commentary.

The legacy predicate is the universe-polymorphic DECT 54.3 overreach criterion on the already frozen report, certificate, and propositional-semantics carriers.

Both directions preserve strict expansion, source scope, report, claim version, and exact report conditions. At the sole license existential, the proof invokes the frozen 57.3-C equivalence to convert typed certificate validity to and from its unique legacy image.

This discharges obligation 57.3-E from definition-escape-completion-theory atom generic-residual-6a153578be42b0dc05d1bf74fa4fe146f63b6fc6a6e6cee245ad9a9835653ca4.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscapeSemantics/SemanticOverreachLegacyBridge.semantic_overreach_iff_overreach
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeSemantics/SemanticOverreachClosure