[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.TreeEval area:

• Audited the declaration in this area on the orphan list (Cslib.TreeEval.encode_injective).
• Added a docstring for Cslib.TreeEval.encode_injective (specifically identified in Consolidation: well-scoped cleanup tasks (replaces the metric-driven quality program) #949 as lacking one).
• Added a ## Main results entry in Complexity/Computability/TreeEval/Instance.lean for Cslib.TreeEval.encode_injective:
  • Cslib.TreeEval.encode_injective: encoding an instance into a bit string is injective.

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 40187164965

---

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: c0cc5e82
• Scope: Item 8 on #949 for area Computability.TreeEval
• Hosted CI: run 40187164965

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

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-22 (agent review) at c0cc5e8.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-22 — APPROVED at c0cc5e8 (agent review, not human approval)

Doc-only, covering the single #949 item-8 † entry for Computability.TreeEval. The new docstring and Main entry name the real Cslib.TreeEval.encode_injective and match its statement (I.tree.encode = J.tree.encode → I = J, where Tree.encode is the List Bool encoding behind encInstance). Visibility is unchanged. Hosted ci-checks is green at this head, and the PR merges cleanly with main at cb8e6dcb.