[SamuelSchlesinger]

Summary

Part of #949 (Item 8: orphan declarations whose only outside reference was a named axiom guard removed in #996 and #1004).

This PR covers the Computability.Kolmogorov area:

• Audited all 13 declarations in this area on the orphan list. Confirmed that all 13 have existing complete docstrings and represent public API.
• Added a ## Main results entry in Complexity/Computability/Kolmogorov/Depth.lean for the daggered declaration:
  • Cslib.Kolmogorov.DescriptionMethod.depthBetween_add_depth: depth between two bounds plus depth at the upper bound equals depth at the lower bound.

No statements or definitions changed meaning. No visibility was changed.

Validation

• Local validation passed all 6 gates (scripts/check.sh), hygiene checks (python3 scripts/check_hygiene.py), and tidy surface ratchet (python3 scripts/check_tidy_surface.py).
• Hosted CI: run 40184998094

---

Generated with Jetski agent assistance by worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65)

[SamuelSchlesinger]

Status: awaiting review

• Agent/Session: worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65)
• Revision: e83b173f
• Scope: Item 8 on #949 for area Computability.Kolmogorov
• Hosted CI: run 40184998094

All 6 validation gates, hygiene checks, and tidy surface ratchet passed locally. Requesting coordinator review.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-20 (agent review) at e83b173.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-20 — APPROVED at e83b173

Agent review, not human approval. Doc-only: the new Main entry names the only † declaration for Computability.Kolmogorov in #949, Cslib.Kolmogorov.DescriptionMethod.depthBetween_add_depth, and matches its statement (t₁ ≤ t₂ → depthBetween t₁ t₂ x + depth t₂ x = depth t₁ x). Its docstring states this. Nothing is made private. Hosted ci-checks is green at this head, and the head merges cleanly with current main.