Fused Counting Correctness

Abstract

The fused catalog census agrees with every frozen reference field.

Theorem 1.1 (Saturated pair classification).

$$\left(\mathrm{pairScan}(C,E,x,y)=none\iff \mathrm{indistinguishable}(C,\mathrm{fullIndexSet}(C),x,y)\right)\wedge (\forall i,m,\mathrm{pairScan}(C,E,x,y)=\mathrm{one}(i,m)\iff \left(m=\mathrm{selectedMask}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)),x,y)\wedge \left(\mathrm{indistinguishable}(C,\mathrm{without}(C,i),x,y)\wedge \left(\neg \mathrm{agrees}(\mathrm{primitives}(\mathrm{theoremAt}(C,i)),x,y)\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedPairClassification (✓ std3). ∎

Source. Repository-derived.

Commentary.

Content. The live escape witness is the singleton scan theorem, which identifies the sole disagreement and proves all other indices agree.

Theorem 1.2 (Fused full count is exact).

$$\mathrm{full}(\mathrm{fusedCounts}(C,S,E))=\mathrm{escapeNumerator}(C,\mathrm{fullIndexSet}(C))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedFull_eq_escapeNumerator (✓ std3). ∎

Source. Repository-derived.

Commentary.

Content. The live fusedCounts_value fold invariant counts each pair class once; the pair classifier then identifies the matching frozen finset.

Theorem 1.3 (Every fused unique count is exact).

$$\mathrm{unique}(\mathrm{fusedCounts}(C,S,E),i)=\mathrm{uniqueCaptureCount}(C,i)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedUnique_eq_uniqueCaptureCount (✓ std3). ∎

Source. Repository-derived.

Commentary.

Content. The live fusedCounts_value fold invariant counts each pair class once; the pair classifier then identifies the matching frozen finset.

Theorem 1.4 (Derived leave-one-out count is exact).

$$\mathrm{without}(\mathrm{fusedCounts}(C,S,E),i)=\mathrm{escapeNumerator}(C,\mathrm{without}(C,i))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedWithout_eq_escapeNumerator_without (✓ std3). ∎

Source. Repository-derived.

Commentary.

Bind-only companion. It rewrites full and unique correctness through the frozen leave-one-out addition law.

Theorem 1.5 (Every fused role bin is exact).

$$\mathrm{roleBins}(\mathrm{fusedCounts}(C,S,E),i,b)=\mathrm{roleHistogram}(C,i,\mathrm{roleSignatureOfBucket}(b))$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedRoleBins_eq_roleHistogram (✓ std3). ∎

Source. Repository-derived.

Commentary.

Content. The live fusedCounts_value fold invariant counts each pair class once; the pair classifier then identifies the matching frozen finset.

Theorem 1.6 (Fused role bins are complete).

$$\mathrm{sum}(b,\mathrm{roleBins}(\mathrm{fusedCounts}(C,S,E),i,b))=\mathrm{unique}(\mathrm{fusedCounts}(C,S,E),i)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedRoleBins_sum_eq_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

Content. Pointwise fused correctness stays live, and the new bucket-signature bijection transports the frozen histogram partition.

Theorem 1.7 (Fused positivity transports).

$$0<\mathrm{unique}(\mathrm{fusedCounts}(C,S,E),i)\Rightarrow 0<\mathrm{uniqueCaptureCount}(C,i)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.uniqueCaptureCount_pos_of_fused (✓ std3). ∎

Source. Repository-derived.

Commentary.

Bind-only companion. It rewrites by fused unique-count correctness.

References

• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedFull_eq_escapeNumerator
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedPairClassification
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedRoleBins_eq_roleHistogram
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedRoleBins_sum_eq_unique
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedUnique_eq_uniqueCaptureCount
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.fusedWithout_eq_escapeNumerator_without
• Truth anchor: D5/S3/ConceptDynamics/InformationEscapeCounting/FusedCorrectness.uniqueCaptureCount_pos_of_fused
• Dependency: D5/S3/ConceptDynamics/InformationEscapeCounting/Fused