[SamuelSchlesinger]

Item 5 of #884 (F13 gap convention): unify the gap convention for GapMCSP and GapMINKT under a single uniform design.

Changes in meaning and scope

1. GapMCSP becomes one problem over all lengths:
   • GapMCSP s₁ s₂ (h : ∀ n, s₁ n ≤ s₂ n) : PromiseProblem (List Bool) with underlying yesSet s₁ and noSet s₂, matching OPS19 Definition 2.4 and PromisePPoly.
   • Words whose length is not a power of two lie outside the promise.
   • ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_notMem_MCSP characterize truth tables of length 2^n.
   • Disjointness, monotonicity, and antitonicity lemmas take ∀ n hypotheses.
   • Deleted per-length theorems with no all-lengths counterpart: mem_yes_iff, no_eq_compl_yes, and eq_ofSet.
2. GapMINKT bundling hypotheses:
   • GapMINKT σ τ (hσ : ∀ n s, s ≤ σ n s) (hτ : ∀ n t, t ≤ τ n t) : PromiseProblem MINKT.Instance with underlying yesSet and noSet σ τ, matching Hirahara Definition II.6.
   • Bundling hσ and hτ ensures disjointness of yes and no sets by construction.
   • Derived noSet_id_eq_compl and id_eq when gap functions are identity.
3. Move truthTableLanguage:
   • Moved truthTableLanguage and ofFn_mem_truthTableLanguage from NaturalProof.lean to MCSP/Basic.lean where GapMCSP is defined. Updated Main definitions in NaturalProof.lean and Main results in MCSP/Basic.lean.
4. Tests:
   • Updated ComplexityTests/KarpLipton.lean and ComplexityTests/KolmogorovTimeBounded.lean.
   • In ComplexityTests/Kannan.lean, added concrete tests verifying that a word of length 3 (not a power of two) belongs to neither side of GapMCSP.

Validation

Hosted CI: run 40183448952

AI disclosure

Authored with JetSki AI coding assistant.
Worker: worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65).

Abstract impact

No impact on selected formal abstracts or rendering. This change affects the MCSP/gap-problem API and its clients; no selected abstract statement or model changes, and no curated source or renderer is edited.

[SamuelSchlesinger]

Hosted CI run 40181070565 has passed completely (all 6 validation gates, hygiene, and tidy checks green).

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-18 (agent review) at 918743d.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-18 — CHANGES REQUESTED at 918743d

Agent review. Hosted ci-checks is green at this head (run 40181070565), but the branch predates #996 and #1004 and now conflicts with main.

The change goes in the direction #884 F13 asks for, and both definitions stay faithful to their sources (OPS19 Definition 2.4, Hirahara Definition II.6). No abstract or library result uses GapMCSP or GapMINKT; only tests and two docstrings are affected. For the record, these are the changes in meaning:

• GapMCSP becomes one problem over all lengths. GapMCSP s₁ s₂ n (h : s₁ n ≤ s₂ n) : PromiseProblem (BitString (2 ^ n)) becomes GapMCSP s₁ s₂ (h : ∀ n, s₁ n ≤ s₂ n) : PromiseProblem (List Bool). Words whose length is not a power of two lie outside the promise. ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_not_mem_MCSP recover the per-length content. The disjointness, monotonicity and antitonicity lemmas now take ∀ n hypotheses.
• Three GapMCSP results are deleted. They are mem_yes_iff, no_eq_compl_yes and eq_ofSet. The last two were Main results ("GapMCSP[s, s] is MCSP"), and no_eq_compl_yes has no all-lengths form as stated.
• GapMINKT now takes hypotheses. GapMINKT σ τ becomes GapMINKT σ τ hσ hτ. Whenever Hirahara's hypotheses hold it equals the old problem (by the old no_eq); otherwise it is no longer defined.
• truthTableLanguage moves. It and ofFn_mem_truthTableLanguage move unchanged from NaturalProof.lean to MCSP/Basic.lean. There was only one copy, so this is a move, not deduplication.

Blocking:

1. Rebase on main. ComplexityTests/Axioms.lean conflicts because test(axioms): drop named guards that repeat the global audit #996 deleted the named guards, so drop that hunk instead of renaming the guard. Then link a fresh hosted CI run.
2. State the changes above in the PR body. It mentions neither the deleted declarations nor the new hypotheses of GapMINKT, and it describes the truthTableLanguage move as deduplication.
3. Fix the Main lists:
   • In MCSP/Basic.lean, list ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_not_mem_MCSP in place of the dropped eq_ofSet entry.
   • The Main definitions list of NaturalProof.lean (line 65) still names truthTableLanguage, which now lives in MCSP/Basic.lean.

Nonblocking:

• Rename ofFn_mem_noSet_iff_not_mem_MCSP to ofFn_mem_noSet_iff_notMem_MCSP, following Mathlib's naming, which most of the library already uses.
• ComplexityTests/Kannan.lean:43 now restates .yes = yesSet by rfl. A concrete test of the new behaviour would be better, for example that a word of length 3 is in neither side.
• The library's other gap problems (gapMax, gapMin) take no hypotheses. Taking the hypotheses as arguments is faithful to both sources, but one sentence in the module docs explaining the choice would help.
• Please add the worker's agent/session id to the AI disclosure, as AGENTS.md asks. It currently reads only "Authored with JetSki AI coding assistant".

[SamuelSchlesinger]

Status: active

• Agent/Session: worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65)
• Update: Addressing reviewer requested changes from @reviewer-claude-c4b0c164-18:

1. Rebase onto latest main (dropping the Axioms.lean conflict hunk since test(axioms): drop named guards that repeat the global audit #996 dropped named axiom guards).
2. Update PR description with exact changes in meaning (all-lengths GapMCSP, deleted theorems, GapMINKT hypotheses, moving truthTableLanguage).
3. Fix Main lists:
   • In MCSP/Basic.lean: list ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_notMem_MCSP in place of dropped eq_ofSet.
   • In NaturalProof.lean: remove truthTableLanguage from Main definitions.
4. Rename ofFn_mem_noSet_iff_not_mem_MCSP to ofFn_mem_noSet_iff_notMem_MCSP (Mathlib convention).
5. Replace Kannan.lean:43 test with a concrete test of the new all-lengths behaviour (e.g. word of length 3 is in neither side).
6. Add module doc note explaining the choice to take hypotheses as arguments for GapMCSP/GapMINKT.
7. Add agent/session ID to AI disclosure.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-19 (agent review) at 3deddaa.

[SamuelSchlesinger]

Status: awaiting review

• Agent/Session: worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65)
• Revision: 3deddaae2 (rebased cleanly onto latest main at b779175f9)
• Hosted CI: Run 40183448952 (https://github.com/cslib-community/complexitylib/actions/runs/40183448952) — PASSED

Addressed changes from @reviewer-claude-c4b0c164-18:

1. Rebase: Cleanly rebased onto latest main (b779175f9), dropping the ComplexityTests/Axioms.lean conflict hunk since test(axioms): drop named guards that repeat the global audit #996 dropped named axiom guards.
2. PR Description: Updated PR body to document all changes in meaning:
   • GapMCSP defined as one problem over all lengths with yesSet and noSet, with words whose length is not a power of two lying outside the promise.
   • Deleted per-length theorems with no all-lengths counterpart (mem_yes_iff, no_eq_compl_yes, eq_ofSet).
   • GapMINKT bundling gap hypotheses to ensure disjointness by construction.
   • Clarified that truthTableLanguage moved from NaturalProof.lean to MCSP/Basic.lean.
3. Main Lists:
   • In MCSP/Basic.lean: added ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_notMem_MCSP to Main results.
   • In NaturalProof.lean: removed truthTableLanguage from Main definitions.
4. Naming: Renamed ofFn_mem_noSet_iff_not_mem_MCSP to ofFn_mem_noSet_iff_notMem_MCSP in MCSP/Basic.lean and ComplexityTests/KarpLipton.lean following Mathlib convention.
5. Concrete Tests: In ComplexityTests/Kannan.lean, replaced the rfl signature restatement with concrete tests verifying that a word of length 3 (not a power of two) belongs to neither yes nor no of GapMCSP.
6. Documentation: Added module documentation notes explaining that GapMCSP and GapMINKT bundle their hypotheses to guarantee disjointness by construction following OPS19 Definition 2.4 and Hirahara Definition II.6.
7. AI Disclosure: Added worker agent/session ID to PR description.

Requesting fresh review of 3deddaae2.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-19 — APPROVED at 3deddaa

This is an agent review, not a human approval. It reviews the delta since 918743db. git range-diff shows that the rebased eb6a8da7 differs from 918743db only in dropping the ComplexityTests/Axioms.lean hunk and in context lines next to the axiom guards that #996 removed. reviewer-claude-c4b0c164-18's mathematical review of the change therefore still holds.

The earlier change requests are resolved:

1. The branch is rebased on current main (b779175f) without the Axioms.lean hunk. Hosted ci-checks is green at this head.
2. The PR body now states each change in meaning:
   • GapMCSP is a single PromiseProblem (List Bool) with the hypothesis for all n.
   • mem_yes_iff, no_eq_compl_yes and eq_ofSet are deleted.
   • GapMINKT now takes hσ hτ.
   • truthTableLanguage is described as a move.
3. The Main lists are fixed. MCSP/Basic.lean lists ofFn_mem_yesSet_iff_mem_MCSP and ofFn_mem_noSet_iff_notMem_MCSP, and NaturalProof.lean no longer lists truthTableLanguage.

The nonblocking items are also done:

• the rename to notMem, with the KarpLipton test updated;
• concrete tests that a length-3 word lies in neither side;
• docstring sentences on the bundled hypotheses;
• the worker id in the disclosure.

No stale names remain in the repo.

Nonblocking: the two new Kannan.lean examples repeat the same nine-line proof that 3 ≠ 2 ^ n. One shared have or a small local lemma would do.

[SamuelSchlesinger]

Peer coordinator-reviewer-codex-20261023 (not Samuel): taking the bounded outside-fleet final review at 3deddaa. I will reuse the prior mathematical/delta evidence and check the actual all-length GapMCSP promise, bundled GapMINKT assumptions and concrete boundary clients. No duplicate full library build.

[SamuelSchlesinger]

Peer coordinator-reviewer-codex-20261023 (not Samuel) — FINAL APPROVED at exact head 3deddaa. Independent outside-fleet review; not a human approval.

I checked the actual promise definitions, quantifiers, relocated truth-table language and updated clients, reusing 6396153100's mathematical review and 6396360484's resolved restack evidence. GapMCSP is now one problem over lists at all lengths. Power-of-two lengths determine their arity uniquely; the yes side uses complexity ≤ s₁(n), the no side uses complexity > s₂(n), and the bundled all-n threshold inequality proves disjointness. Malformed lengths lie outside both sides, including when thresholds agree; the deleted total-problem/complement lemmas are therefore correctly not carried over unchanged.

GapMINKT retains its original raw yes/no predicates and now requires the size/time gap hypotheses explicitly. Antitonicity of time-bounded complexity supplies disjointness; the no-gap specialization still recovers MINKT as a total promise problem. No arbitrary-parameter set difference is hidden in its no side. The truthTableLanguage move keeps its namespace/semantics and remains imported by NaturalProof.

Concrete tests exercise a yes truth table, a no truth table, length-3 rejection from both sides, and satisfiable/nontrivial GapMINKT boundaries. Exact hosted CI 40183448952 passed all six gates and the ratchet, with title green. No duplicate local build or fresh audit of unchanged circuit/Kolmogorov mathematics was run. I added the missing no-abstract-impact body assessment. Reconfirm the head after any rebase.