Information Escape Catalog Laws

Abstract

Finite catalog laws for labels, primitive kernels, irredundancy, and augmentation.

Definition 1.1 (Catalog reindexing).

$$\mathrm{Index}(\mathrm{reindex}(C,e))=J$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/Laws.reindex (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite catalog and its canonical primitive kernels.

Definition 1.2 (Catalog theorem-family replacement).

$$\mathrm{Index}(\mathrm{withTheoremAt}(C,U))=\mathrm{Index}(C)$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/Laws.withTheoremAt (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite catalog and its canonical primitive kernels.

Theorem 1.3 (Every selected escape finset is invariant under reindexing).

$$\forall e:\mathrm{Index}(C)\equiv J,\mathrm{escapePairs}(\mathrm{reindex}(C,e),\mathrm{map}(\mathrm{toEmbedding}(e),A))=\mathrm{escapePairs}(C,A)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.4 (Every selected escape rate is invariant under reindexing).

$$\forall e:\mathrm{Index}(C)\equiv J,\mathrm{escapeRate}(\mathrm{reindex}(C,e),\mathrm{map}(\mathrm{toEmbedding}(e),A))=\mathrm{escapeRate}(C,A)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.5 (Unique capture is invariant under reindexing).

$$\forall e:\mathrm{Index}(C)\equiv J,\mathrm{uniqueCaptureCount}(\mathrm{reindex}(C,e),\mathrm{apply}(e,i))=\mathrm{uniqueCaptureCount}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.6 (Exact theorem gain is invariant under reindexing).

$$\forall e:\mathrm{Index}(C)\equiv J,\mathrm{theoremGainRate}(\mathrm{reindex}(C,e),\mathrm{apply}(e,i))=\mathrm{theoremGainRate}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.7 (Pointwise kernel equality preserves every unique capture count).

$$(\forall j,x,y,\mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,j))),x,y)\iff \mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{apply}(U,j))),x,y))\Rightarrow \mathrm{uniqueCaptureCount}(\mathrm{withTheoremAt}(C,U),i)=\mathrm{uniqueCaptureCount}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.8 (Pointwise kernel equality preserves every unique capture finset).

$$(\forall j,x,y,\mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,j))),x,y)\iff \mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{apply}(U,j))),x,y))\Rightarrow \mathrm{uniqueCapturePairs}(\mathrm{withTheoremAt}(C,U),i)=\mathrm{uniqueCapturePairs}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.9 (Pointwise kernel equality preserves full-catalog escape pairs).

$$(\forall j,x,y,\mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,j))),x,y)\iff \mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{apply}(U,j))),x,y))\Rightarrow \mathrm{escapePairs}(\mathrm{withTheoremAt}(C,U),\mathrm{fullIndexSet}(\mathrm{withTheoremAt}(C,U)))=\mathrm{escapePairs}(C,\mathrm{fullIndexSet}(C))$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.10 (Pointwise kernel equality preserves the full-catalog escape count).

$$(\forall j,x,y,\mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,j))),x,y)\iff \mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{apply}(U,j))),x,y))\Rightarrow \mathrm{card}(\mathrm{escapePairs}(\mathrm{withTheoremAt}(C,U),\mathrm{fullIndexSet}(\mathrm{withTheoremAt}(C,U))))=\mathrm{card}(\mathrm{escapePairs}(C,\mathrm{fullIndexSet}(C)))$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.11 (Pointwise kernel equality preserves the full-catalog escape rate).

$$(\forall j,x,y,\mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,j))),x,y)\iff \mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{apply}(U,j))),x,y))\Rightarrow \mathrm{escapeRate}(\mathrm{withTheoremAt}(C,U),\mathrm{fullIndexSet}(\mathrm{withTheoremAt}(C,U)))=\mathrm{escapeRate}(C,\mathrm{fullIndexSet}(C))$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.12 (Kernel-equivalent primitive realizations have identical counts).

$$(\forall x,y,\mathrm{agrees}(\mathrm{toPrimitiveBundle}(R),x,y)\iff \mathrm{agrees}(\mathrm{toPrimitiveBundle}(S),x,y))\Rightarrow \mathrm{uniqueCaptureCount}(\mathrm{withTheoremAt}(C,(j\mapsto \mathrm{ite}(j=k,\mathrm{TheoremUnit}(\mathrm{toPrimitiveBundle}(R),\mathrm{Statement}(\mathrm{theoremAt}(C,j)),\mathrm{proof}(\mathrm{theoremAt}(C,j))),\mathrm{theoremAt}(C,j)))),i)=\mathrm{uniqueCaptureCount}(\mathrm{withTheoremAt}(C,(j\mapsto \mathrm{ite}(j=k,\mathrm{TheoremUnit}(\mathrm{toPrimitiveBundle}(S),\mathrm{Statement}(\mathrm{theoremAt}(C,j)),\mathrm{proof}(\mathrm{theoremAt}(C,j))),\mathrm{theoremAt}(C,j)))),i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Definition 1.13 (Catalog irredundancy).

$$\mathrm{CatalogIrredundant}(C)=\forall i,\mathrm{LowersEscape}(C,i)$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/Laws.CatalogIrredundant (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite catalog and its canonical primitive kernels.

Theorem 1.14 (Irredundancy is positivity of all unique captures).

$$\mathrm{CatalogIrredundant}(C)\iff \forall i,0<\mathrm{uniqueCaptureCount}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Definition 1.15 (Augmented theorem statement).

$$\mathrm{AugmentedStatement}(C,i)=\mathrm{And}(\mathrm{Statement}(\mathrm{theoremAt}(C,i)),\mathrm{LowersEscape}(C,i))$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/Laws.AugmentedStatement (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite catalog and its canonical primitive kernels.

Theorem 1.16 (Augmented theorem proof constructor).

$$\mathrm{LowersEscape}(C,i)\Rightarrow \mathrm{AugmentedStatement}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

Theorem 1.17 (Every theorem in an irredundant catalog is augmented).

$$\mathrm{CatalogIrredundant}(C)\Rightarrow \forall i,\mathrm{AugmentedStatement}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the frozen finite-kernel and exact-count APIs.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.AugmentedStatement
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.CatalogIrredundant
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.augmentedProof
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.catalogIrredundant_iff_forall_pos
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.catalog_all_augmented
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.escapeCount_congr_kernel
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.escapePairs_congr_kernel
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.escapePairs_reindex
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.escapeRate_congr_kernel
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.escapeRate_reindex
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.reindex
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.theoremGainRate_reindex
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.uniqueCaptureCount_congr_kernel
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.uniqueCaptureCount_congr_primitiveRealization
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.uniqueCaptureCount_reindex
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.uniqueCapturePairs_congr_kernel
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/Laws.withTheoremAt
• Dependency: D5/S3/ConceptDynamics/InformationEscape/ExactRate