A sharp statement and its finite evaluation

The external general assertions name a sharp constant and an attaining example. The present certificate additionally prints:

1. all four input points and all transition probabilities;

2. an exhaustive partition of the sixteen Boolean functions;

3. every representative truth table and noised value;

4. a signed coordinate attaining equality;

5. parity and a biased noncoordinate function with exact gaps;

6. finite integer-square certificates for the numerical bounds;

7. the information implication and its normalization in bits.

A three-atom posterior distribution is not automatically the three-point optimizer of the local joining problem. Neither a Lean target nor an implementation ledger supplies that missing identification.