Generated-Kernel Chains

Abstract

Classified generator schedules yield disjoint, telescoping escape decompositions.

Definition 1.1 (Generator step classification).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.GeneratorStepClass

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.GeneratorStepClass (✓ std3).

Source. Repository-derived.

Commentary.

Each scheduled addition is certified either as a strict edge or as an extensional stutter.

Definition 1.2 (Generator schedule).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.GeneratorSchedule

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.GeneratorSchedule (✓ std3).

Source. Repository-derived.

Commentary.

A complete bijective ordering records every catalog addition, its node sequence, endpoints, and classification.

Definition 1.3 (Strict kernel chain).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.StrictKernelChain

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.StrictKernelChain (✓ std3).

Source. Repository-derived.

Commentary.

A stutter-free path retains a strict generator-step certificate at every adjacency.

Definition 1.4 (Strict subsequence).

Lean statement: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence

Formalization. D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence (✓ std3).

Source. Repository-derived.

Commentary.

Deleting classified stutters produces a strict kernel chain while preserving the path endpoints.

Theorem 1.5 (Strict subsequences preserve the first node).

$$\mathrm{node}(\mathrm{strictSubsequence}(A),0)=\mathrm{node}(A,0).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence_node_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.6 (Strict subsequences preserve the terminal node).

$$\mathrm{node}(\mathrm{strictSubsequence}(A),\mathrm{last}(\mathrm{strictSubsequence}(A)))=\mathrm{node}(A,\mathrm{last}(A)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence_node_last (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.7 (Retained labels come from the schedule).

$$\mathrm{added}(\mathrm{strictSubsequence}(A),r)\in \mathrm{image}(\mathrm{added}(A),\mathrm{univ}()).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence_added_mem (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Remark 1.8 (Schedule increment rate).

$$\mathrm{incrementRate}(A,r)=\frac{\mathrm{incrementCount}(A,r)}{\mathrm{escapeDenominator}(A)}.$$

Source. Repository-derived.

Commentary.

GeneratorSchedule.incrementRate uses the canonical arena escape denominator.

Remark 1.9 (Strict-chain increment rate).

$$\mathrm{incrementRate}(K,r)=\frac{\mathrm{incrementCount}(K,r)}{\mathrm{escapeDenominator}(A)}.$$

Source. Repository-derived.

Commentary.

StrictKernelChain.incrementRate uses the canonical arena escape denominator.

Theorem 1.10 (Collapsed increments are empty).

$$\mathrm{node}(A,\mathrm{castSucc}(r))=\mathrm{node}(A,\mathrm{succ}(r))\Rightarrow \mathrm{increment}(A,r)=\varnothing .$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.collapsed_increment_eq_empty (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.11 (Chain increments are pairwise disjoint).

$$\forall r,s,r\ne s⟹\mathrm{Disjoint}(\mathrm{increment}(A,r),\mathrm{increment}(A,s)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_increment_pairwise_disjoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.12 (Increment union is terminal escape loss).

$$\mathrm{biUnion}(\mathrm{univ}(),\mathrm{increment}(A))=\mathrm{sdiff}(\mathrm{escapeAt}(\mathrm{node}(A,0)),\mathrm{escapeAt}(\mathrm{node}(A,\mathrm{last}(A)))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_increment_union (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.13 (Increment counts telescope).

$$\mathrm{sum}(\mathrm{incrementCount}(A))+\mathrm{card}(\mathrm{escapeAt}(\mathrm{node}(A,\mathrm{last}(A))))=\mathrm{card}(\mathrm{escapeAt}(\mathrm{node}(A,0))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_count_telescopes (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.14 (Increment rates telescope).

$$\mathrm{sum}(\mathrm{incrementRate}(A))+\mathrm{escapeRate}(\mathrm{node}(A,\mathrm{last}(A)))=\mathrm{escapeRate}(\mathrm{node}(A,0)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_rate_telescopes (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.15 (A strict-chain terminal is its generated union).

$$\mathrm{node}(A,0)=\mathrm{generatedKernel}(C,T)\Rightarrow \mathrm{node}(A,\mathrm{last}(A))=\mathrm{generatedKernel}(C,\mathrm{union}(T,\mathrm{image}(\mathrm{added}(A)))).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strict_chain_terminal_eq_generatedKernel_union (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.16 (Strict-chain terminals are order independent).

$$\left(\left(\mathrm{node}(A,0)=\mathrm{generatedKernel}(C,T)\wedge \mathrm{node}(B,0)=\mathrm{generatedKernel}(C,T)\right)\wedge \mathrm{image}(\mathrm{added}(A))=\mathrm{image}(\mathrm{added}(B))\right)\Rightarrow \mathrm{node}(A,\mathrm{last}(A))=\mathrm{node}(B,\mathrm{last}(B)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.terminal_order_independent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.17 (Full-schedule terminals are order independent).

$$\mathrm{node}(A,\mathrm{last}(A))=\mathrm{node}(B,\mathrm{last}(B)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.full_schedule_terminal_order_independent (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.18 (A full schedule ends at the full kernel).

$$\mathrm{node}(A,\mathrm{last}(A))=\mathrm{generatedKernel}(C,\mathrm{fullIndexSet}(C)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.schedule_terminal_eq_generatedKernel_full (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

Theorem 1.19 (The leave-one-out last step is unique capture).

$$\left(\mathrm{PositiveLength}(A)\wedge \mathrm{node}(A,\mathrm{penultimate}(A))=\mathrm{generatedKernel}(C,\mathrm{without}(C,i))\right)\Rightarrow \mathrm{increment}(A,\mathrm{last}(A))=\mathrm{uniqueCapturePairs}(C,i).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.last_step_eq_uniqueCapture (✓ std3). ∎

Source. Repository-derived.

Commentary.

The certificate follows from classified generator steps and finite escape-set algebra.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.GeneratorSchedule
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.GeneratorStepClass
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.StrictKernelChain
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_count_telescopes
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_increment_pairwise_disjoint
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_increment_union
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.chain_rate_telescopes
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.collapsed_increment_eq_empty
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.full_schedule_terminal_order_independent
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.last_step_eq_uniqueCapture
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.schedule_terminal_eq_generatedKernel_full
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence_added_mem
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence_node_last
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strictSubsequence_node_zero
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.strict_chain_terminal_eq_generatedKernel_union
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeHierarchy/KernelChain.terminal_order_independent
• Dependency: D5/S3/ConceptDynamics/InformationEscapeHierarchy/GeneratedKernel