Structural Escape Novelty

Abstract

Finite escape reduction is canonical strict kernel novelty of quotient CUTs.

Definition 1.1 (Structural escape reduction).

$$\mathrm{StructurallyLowersEscape}(C,i)\iff \mathrm{StrictSubset}(\mathrm{catalogJointKernel}(C,\mathrm{univ}()),\mathrm{catalogJointKernel}(C,\mathrm{setOf}(j\mid j\ne i))).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.StructurallyLowersEscape (✓ std3).

Source. Repository-derived.

Commentary.

This definition packages the catalog kernel or its canonical quotient CUT.

Theorem 1.2 (Structural and exact reduction agree).

$$\mathrm{Nondegenerate}(A)\Rightarrow \mathrm{StructurallyLowersEscape}(C,i)\iff \mathrm{LowersEscape}(C,i).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.structurallyLowersEscape_iff_lowersEscape (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

Definition 1.3 (Leave-one-out kernel closure).

$$\mathrm{semanticClosureWithout}(C,i)=\mathrm{setOf}(K\mid \forall x,y,(\forall j,j\ne i\Rightarrow \mathrm{agrees}(\mathrm{theoremAt}(C,j),x,y))\Rightarrow \mathrm{related}(K,x,y)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.semanticClosureWithout (✓ std3).

Source. Repository-derived.

Commentary.

This definition packages the catalog kernel or its canonical quotient CUT.

Definition 1.4 (Tagged quotient output).

$$\mathrm{QuotientOutput}(C)=\mathrm{Sigma}(j,\mathrm{Quotient}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,j))))).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.QuotientOutput (✓ std3).

Source. Repository-derived.

Commentary.

This definition packages the catalog kernel or its canonical quotient CUT.

Definition 1.5 (Tagged canonical quotient CUT).

$$\mathrm{taggedQuotientCut}(C,i)=\lambda x,\mathrm{tag}(i,\mathrm{quotientCut}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,i))),x)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.taggedQuotientCut (✓ std3).

Source. Repository-derived.

Commentary.

This definition packages the catalog kernel or its canonical quotient CUT.

Definition 1.6 (Homogeneous leave-one-out CUT family).

$$\mathrm{quotientCutsWithout}(C,i)=\mathrm{image}(\lambda j,\mathrm{taggedQuotientCut}(C,j),\mathrm{setOf}(j\mid j\ne i)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.quotientCutsWithout (✓ std3).

Source. Repository-derived.

Commentary.

This definition packages the catalog kernel or its canonical quotient CUT.

Theorem 1.7 (Catalog and canonical closures agree).

$$\mathrm{taggedQuotientCut}(C,i)\in \mathrm{SemanticClosure}(\mathrm{quotientCutsWithout}(C,i))\iff \mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)))\in \mathrm{semanticClosureWithout}(C,i).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.taggedQuotientCut_mem_semanticClosure_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

Theorem 1.8 (Canonical strict novelty criterion).

$$\mathrm{Nondegenerate}(A)\Rightarrow \mathrm{LowersEscape}(C,i)\iff \mathrm{StrictSubset}(\mathrm{jointKernel}(\lambda d:\mathrm{insert}(\mathrm{taggedQuotientCut}(C,i),\mathrm{quotientCutsWithout}(C,i)),\mathrm{readout}(d)),\mathrm{jointKernel}(\lambda d:\mathrm{quotientCutsWithout}(C,i),\mathrm{readout}(d))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.lowersEscape_iff_strict_kernel_novelty (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

Theorem 1.9 (Semantic closure criterion).

$$\mathrm{Nondegenerate}(A)\Rightarrow \mathrm{LowersEscape}(C,i)\iff \neg (\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)))\in \mathrm{semanticClosureWithout}(C,i)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.lowersEscape_iff_not_mem_semanticClosureWithout (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

Theorem 1.10 (Recoverability prevents reduction).

$$\forall x,y,(\forall j,j\ne i\Rightarrow \mathrm{agrees}(\mathrm{theoremAt}(C,j),x,y))\Rightarrow \mathrm{agrees}(\mathrm{theoremAt}(C,i),x,y)\Rightarrow \neg \mathrm{LowersEscape}(C,i).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.lowersEscape_false_of_recoverable (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

Theorem 1.11 (Duplicate kernels have zero capture).

$$i\ne j\wedge (\forall x,y,\mathrm{agrees}(\mathrm{theoremAt}(C,i),x,y)\iff \mathrm{agrees}(\mathrm{theoremAt}(C,j),x,y))\Rightarrow \mathrm{uniqueCaptureCount}(C,i)=0\wedge \mathrm{uniqueCaptureCount}(C,j)=0.$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.same_kernel_both_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

Theorem 1.12 (Constant kernels have zero capture).

$$\forall x,y,\mathrm{agrees}(\mathrm{theoremAt}(C,i),x,y)\Rightarrow \mathrm{uniqueCaptureCount}(C,i)=0.$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.constant_kernel_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The proof preserves bundle kernels and reuses the canonical semantic closure.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.QuotientOutput
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.StructurallyLowersEscape
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.constant_kernel_zero
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.lowersEscape_false_of_recoverable
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.lowersEscape_iff_not_mem_semanticClosureWithout
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.lowersEscape_iff_strict_kernel_novelty
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.quotientCutsWithout
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.same_kernel_both_zero
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.semanticClosureWithout
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.structurallyLowersEscape_iff_lowersEscape
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.taggedQuotientCut
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/StructuralNovelty.taggedQuotientCut_mem_semanticClosure_iff
• Dependency: D5/S3/ConceptDynamics/DefinitionEscapeLaws/StrictKernelNoveltyCriterion
• Dependency: D5/S3/ConceptDynamics/InformationEscape/ExactRate