Exact Escape Rates

Abstract

Exact finite counts turn escape reduction into positive unique capture.

Definition 1.1 (Escape denominator).

$$\mathrm{escapeDenominator}(A)=\mathrm{card}(\mathrm{offDiagonalPairs}(\mathrm{State}(A))).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeDenominator (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite arena and catalog kernels.

Theorem 1.2 (Ordered-pair denominator formula).

$$\mathrm{escapeDenominator}(A)=\mathrm{card}(A)\times (\mathrm{card}(A)-1).$$

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

Source. Repository-derived.

Commentary.

The proof uses exact Finset cardinality and rational order transport.

Theorem 1.3 (Nondegenerate denominator is positive).

$$\mathrm{Nondegenerate}(A)\Rightarrow 0<\mathrm{escapeDenominator}(A).$$

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

Source. Repository-derived.

Commentary.

The proof uses exact Finset cardinality and rational order transport.

Definition 1.4 (Escape numerator).

$$\mathrm{escapeNumerator}(C,S)=\mathrm{card}(\mathrm{escapePairs}(C,S)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeNumerator (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite arena and catalog kernels.

Definition 1.5 (Exact escape rate).

$$\mathrm{escapeRate}(C,S)=\frac{\mathrm{escapeNumerator}(C,S)}{\mathrm{escapeDenominator}(A)}.$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeRate (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite arena and catalog kernels.

Definition 1.6 (Unique capture count).

$$\mathrm{uniqueCaptureCount}(C,i)=\mathrm{card}(\mathrm{uniqueCapturePairs}(C,i)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/ExactRate.uniqueCaptureCount (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite arena and catalog kernels.

Definition 1.7 (Theorem gain rate).

$$\mathrm{theoremGainRate}(C,i)=\frac{\mathrm{uniqueCaptureCount}(C,i)}{\mathrm{escapeDenominator}(A)}.$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/ExactRate.theoremGainRate (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite arena and catalog kernels.

Definition 1.8 (Strictly lowers escape).

$$\mathrm{LowersEscape}(C,i)\iff \mathrm{escapeRate}(C,\mathrm{fullIndexSet}(C))<\mathrm{escapeRate}(C,\mathrm{without}(C,i)).$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/ExactRate.LowersEscape (✓ std3).

Source. Repository-derived.

Commentary.

This definition is computed from the finite arena and catalog kernels.

Theorem 1.9 (Leave-one-out numerator decomposition).

$$\mathrm{escapeNumerator}(C,\mathrm{without}(C,i))=\mathrm{escapeNumerator}(C,\mathrm{fullIndexSet}(C))+\mathrm{uniqueCaptureCount}(C,i).$$

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

Source. Repository-derived.

Commentary.

The proof uses exact Finset cardinality and rational order transport.

Theorem 1.10 (Rate difference equals gain).

$$\mathrm{Nondegenerate}(A)\Rightarrow \mathrm{escapeRate}(C,\mathrm{without}(C,i))-\mathrm{escapeRate}(C,\mathrm{fullIndexSet}(C))=\mathrm{theoremGainRate}(C,i).$$

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

Source. Repository-derived.

Commentary.

The proof uses exact Finset cardinality and rational order transport.

Theorem 1.11 (Strict reduction criterion).

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

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

Source. Repository-derived.

Commentary.

The proof uses exact Finset cardinality and rational order transport.

Theorem 1.12 (Unique capture witness criterion).

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

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

Source. Repository-derived.

Commentary.

The proof uses exact Finset cardinality and rational order transport.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.LowersEscape
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeDenominator
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeDenominator_eq
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeDenominator_pos
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeNumerator
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeNumerator_without_eq
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.escapeRate
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.lowersEscape_iff_uniqueCaptureCount_pos
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.theoremGainRate
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.theoremGainRate_eq
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.uniqueCaptureCount
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/ExactRate.uniqueCaptureCount_pos_iff_witness
• Dependency: D5/S3/ConceptDynamics/InformationEscape/EscapePairs