Unique Capture Role Histogram

Abstract

The leave-one-out residual is partitioned by four-bit CIRPT role signatures.

Definition 1.1 (Leave-one-out catalog kernel).

$$\mathrm{relation}(\mathrm{withoutKernel}(C,i))=\mathrm{indistinguishable}(C,\mathrm{without}(C,i))$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.withoutKernel (✓ std3).

Source. Repository-derived.

Commentary.

The other theorem bundles form one decidable equivalence kernel.

Definition 1.2 (Residual role-signature multiplicity).

$$\mathrm{roleHistogram}(C,i,s)=\mathrm{residualSignatureHistogram}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)),\mathrm{withoutKernel}(C,i),s)$$

Formalization. D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.roleHistogram (✓ std3).

Source. Repository-derived.

Commentary.

Each bucket counts an exact four-role residual signature.

Theorem 1.3 (Unique capture is leave-one-out kernel residual).

$$\mathrm{uniqueCapturePairs}(C,i)=\mathrm{kernelResidual}(\mathrm{withoutKernel}(C,i),\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,i))))$$

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

Source. Repository-derived.

Commentary.

The proof uses the finite residual and exact-count APIs.

Theorem 1.4 (Unique capture has nonzero role signature).

$$\mathrm{Member}(p,\mathrm{uniqueCapturePairs}(C,i))\Rightarrow \mathrm{NotEqual}(\mathrm{residualRoleSignature}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)),\mathrm{withoutKernel}(C,i),\mathrm{fst}(p),\mathrm{snd}(p)),(k\mapsto false))$$

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

Source. Repository-derived.

Commentary.

The frozen residual-signature bridge turns unique capture into nonzero role coverage.

Theorem 1.5 (Unique capture is the union of its four active-role fibers).

$$\mathrm{uniqueCapturePairs}(C,i)=\mathrm{biUnion}(\mathrm{univ}(Fin4),(k\mapsto \mathrm{filter}(\mathrm{uniqueCapturePairs}(C,i),(p\mapsto \mathrm{residualRoleSignature}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)),\mathrm{withoutKernel}(C,i),\mathrm{fst}(p),\mathrm{snd}(p),k)=true))))$$

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

Source. Repository-derived.

Commentary.

The proof uses the finite residual and exact-count APIs.

Theorem 1.6 (Nonzero buckets sum to unique capture).

$$\mathrm{sum}(s,\mathrm{NotEqual}(s,(k\mapsto false)),\mathrm{roleHistogram}(C,i,s))=\mathrm{uniqueCaptureCount}(C,i)$$

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

Source. Repository-derived.

Commentary.

Fiberwise finite counting identifies the nonzero buckets with the residual finset.

Theorem 1.7 (Theorem gain depends only on primitive kernels).

$$(\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{theoremGainRate}(\mathrm{withTheoremAt}(C,U),i)=\mathrm{theoremGainRate}(C,i)$$

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

Source. Repository-derived.

Commentary.

The proof uses the finite residual and exact-count APIs.

Theorem 1.8 (Closed truth has zero unique capture).

$$(\forall x,y,\mathrm{relation}(\mathrm{toKernel}(\mathrm{primitives}(\mathrm{theoremAt}(C,i))),x,y)\iff \mathrm{relation}(\mathrm{cutKernel}((x\mapsto true)),x,y))\Rightarrow \mathrm{uniqueCaptureCount}(C,i)=0$$

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

Source. Repository-derived.

Commentary.

The proof uses the finite residual and exact-count APIs.

Theorem 1.9 (Proof certificates do not enter unique capture).

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

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

Source. Repository-derived.

Commentary.

The proof uses the finite residual and exact-count APIs.

Theorem 1.10 (Closed truth has universal kernel).

$$\mathrm{relation}(\mathrm{cutKernel}((x\mapsto true)))=(x,y\mapsto True)$$

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

Source. Repository-derived.

Commentary.

The proof uses the finite residual and exact-count APIs.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.closed_truth_cut_kernel_universal
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.closed_truth_uniqueCaptureCount_zero
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.roleHistogram
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.roleHistogram_sum_eq_uniqueCaptureCount
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.theoremAt_proof_irrelevant
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.theoremGain_depends_only_on_primitive_kernel
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.uniqueCapturePairs_eq_biUnion_roleFibers
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.uniqueCapturePairs_eq_kernelResidual
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.uniqueCapture_roleSignature_nonzero
• Truth anchor: D5/S3/ConceptDynamics/InformationEscape/RoleHistogram.withoutKernel
• Dependency: D5/S3/ConceptDynamics/InformationEscape/Laws