[SamuelSchlesinger]

Resolves item E.6 of #949.

Adds concrete-instance tests in ComplexityTests/SideInformation.lean and ComplexityTests/Embeddability.lean:

• In ComplexityTests/SideInformation.lean, adds bitsJoint (two fair bits with trivial conditioning and side information) and instantiates sum_dist_filter_sideJoint_le on the concrete event {x | x.2 0 = true}, following ComplexityTests/ProductConditioning.lean (feat(Probability): Raz's conditioning lemma for product distributions (#886) #942).
• In ComplexityTests/Embeddability.lean, adds nonvacuity instances on both sides of IsEmbeddable:
  • correlatedTriple, a perfectly correlated triple of bits ((b, b), b), embedded with error 0 via isEmbeddable_withKernel and isEmbeddable_diag;
  • bobGuessesAlice, a target distribution where Bob must match a uniform bit held only by Alice without communication, proved not locally embeddable below error 1 / 2 (¬ IsEmbeddable aliceInput bobGuessesAlice ε for ε < 1 / 2).

Hosted CI: https://github.com/cslib-community/complexitylib/actions/runs/40203582168

Headline abstract catalogue: No impact; test-only additions.

AI disclosure: Implemented by worker-jetski-a59549e8 (Gemini).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-35 (agent review) at d3d8e2a.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-35 — CHANGES REQUESTED at d3d8e2a

Agent review. The two-fair-bits instance of sum_dist_filter_sideJoint_le matches #942's pattern and has a real support witness. Both embeddability instances are correct, and hosted ci-checks is green at this head (run 40200786000). The PR merges cleanly with main.

1. ComplexityTests/Embeddability.lean:14-16: the module doc says the target "is not locally embeddable below error 1 / 2", but the test proves only ¬ IsEmbeddable aliceInput bobGuessesAlice (1 / 4). Since IsEmbeddable is dist ≤ ε, that excludes only ε ≤ 1 / 4. The proof already gives the sharp bound, so state it as example {ε : ℝ} (hε : ε < 1 / 2) : ¬ IsEmbeddable aliceInput bobGuessesAlice ε. The final linarith should close it unchanged. Alternatively, change the doc to 1 / 4. Update the comment above the example to match.

Nonblocking: correlatedTriple is used only through map Prod.fst, so its third coordinate is unused. Either define the pair PMF (Bool × Bool) directly, or exercise Lemma 8 by applying isEmbeddable_diag correlatedTriple.

[SamuelSchlesinger]

Fixed in e1a44b7:

• Generalized the negative embeddability example for aliceInput / bobGuessesAlice to arbitrary ε < 1 / 2 to match the module docstring.
• Instantiated isEmbeddable_diag on correlatedTriple.

Validation: ./scripts/check.sh, check_hygiene.py --check-simp, check_tidy_surface.py, and check_changed_files.py --base origin/main all passed locally. Hosted Lean Action CI: https://github.com/cslib-community/complexitylib/actions/runs/40203582168

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-42 (agent review) at e1a44b7.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-42 — APPROVED at e1a44b7

Agent review, not human approval. This is a delta review against reviewer-claude-c4b0c164-35's change request at d3d8e2af. The new head adds one commit, e1a44b70, which touches only ComplexityTests/Embeddability.lean. Everything else that -35 checked is unchanged.

• Blocking item 1 is resolved. The negative test is now example {ε : ℝ} (hε : ε < 1 / 2) : ¬ IsEmbeddable aliceInput bobGuessesAlice ε, and the comment above it says "below error 1 / 2". The module doc and the test now agree. The bound is sharp: the averaged distance is ½(d(q, δ_true) + d(q, δ_false)) ≥ ½, and a uniform guess by Bob attains ½.
• The nonblocking suggestion was taken. isEmbeddable_diag is now applied to correlatedTriple. That example replaces main's generic ∀ J restatement of Lemma 8. The concrete instance still pins the lemma's statement shape, so no coverage is lost.
• CI and merge. Hosted ci-checks passed at this exact head (run 40203582168), and the branch merges cleanly with main at 9e552300.

Nonblocking: the PR body still says the target is "proved not locally embeddable within error 1 / 4". Please update it to ε < 1 / 2 so the squash message matches.