feat(interaction): compose dependent TypeTree chains

[quangvdao]

Summary

• add path-dependent TypeTree.Chain.then composition with explicit round counts
• expose the dependent prefix/suffix path equivalence and inverse split/join operations
• add flattened left- and right-unit laws and preserve operational three-stage associativity
• name round-count transport Chain.castRounds to avoid shadowing root cast
• document why raw Chain equality is deliberately deferred
• add branch-sensitive producer regressions and update generated imports and maintained interaction docs

Stack

This branch is rebuilt as one unique commit on current main:

• base: 22c729081fce9805dfff28cea8d663aea7a8df84
• head: 0288d76aecf16239f5dd0647eca864f3087953ec

Inherited commits from the former PF-6A/PF-6R stack were dropped. The associativity contract remains operational: equality after Chain.toTypeTree. Raw equality of the round-indexed Chain presentations is intentionally deferred because it exposes dependent transport through path-indexed continuation functions without a current consumer requiring that intensional equality.

Validation

Run on exact head 0288d76aecf16239f5dd0647eca864f3087953ec:

• lake build PolyFun.Interaction.Basic.Chain.Append PolyFunTest.Interaction.Basic.ChainAppendExamples
• ./scripts/validate.sh --lint --test
• lake exe lint-style
• git diff --check origin/main...HEAD
• generated PolyFun.lean import check (170 imports)
• documentation integrity check
• trust-escape search and #print axioms for the composition, unit, path-inverse, and associativity theorems

The principal theorems use only the repository's existing standard footprints: propext, Quot.sound, and, for equivalence/path inverse and associativity results, Classical.choice.

External acceptance gate

This PR remains a draft because no actual ArkLib triple-reduction client is checked in yet.

The audit covered ArkLib origin/main plus origin/design/oracle-reduction-v2, origin/dt/downstream-pfun, origin/new-interaction-types, origin/quang/core-rebuild, and origin/archive/oracle-reduction-v2-pre-split. At design head 5cac96dea4, PF-6B appears only as a documented promotion gate; none of those implementation branches contains a TypeTree.Chain / Chain.then client. ArkLib's existing nested ProtocolSpec reductions are the legacy fixed-round representation and are not this acceptance client.

Merge readiness requires a checked-in ArkLib three-stage reduction that exercises the real dependent stage interfaces through Chain.then, path split/join, and toTypeTree_then_assoc, plus any client-required Chain.outputFamily / Chain.strategyComp coherence. A new presentation datatype remains unauthorized unless this route fails on that concrete client.

[dtumad]

Reviewed the diff. No correctness defects: Chain.then is genuinely dependent (suffix selected by the full flattened prefix path), round-count transport is confined to a small Chain.cast along Nat lemmas with no Fin arithmetic or HEq, toTypeTree_then lands exactly on #62's substitution-monoid substrate, and associativity correctly delegates to the pre-existing FreeM.Path.append_tree_assoc rather than re-proving it. The casts are computation-transparent (finalArity … = 12/23 := rfl reduce through Equiv.cast) and the tests pin both prefix branches with distinct arities. Two inline suggestions; one metadata item:

Draft status: the PR body says "intentionally a draft" with the ArkLib triple-reduction-client acceptance gate, but the PR is not actually marked draft on GitHub — nothing currently prevents an accidental merge past the self-declared gate. Suggest converting to draft (or a do-not-merge label) until the client lands.

[dtumad]

The docstring scopes the associativity claim to flattened trees well, but leaves the raw-Chain question implicit: it never says whether the stronger reassoc ((c.then k).then l) = c.then … (Chain-level equality after transport) is false, unknown, or merely deferred as cast-heavy — it's plausibly true, since both sides have identical round trees. One sentence stating the raw law is deliberately not attempted (and why) would answer the reviewer question the PR body anticipates.

[dtumad]

Two related notes: (a) the file proves associativity but no unit laws — toTypeTree_then_zero_right (composing with the empty chain flattens to toTypeTree m c, via FreeM.append's pure-continuation law) and its left counterpart are cheap with the same technique as toTypeTree_then, and an associativity-only API is lopsided for the graded-monoid story this file is telling; (b) Chain.cast shadows _root_.cast inside namespace Chain, so a downstream file that opens Chain may get surprising resolution — Mathlib has .cast precedent so this is defensible, but castRounds would be unambiguous.