refactor(displayed): use algebra terminology

[quangvdao]

Motivation and context

PR #74 introduces PFunctor.Display, the one-step dependent-polynomial layer needed for Aberle's compositional verification development. That work exposes an older naming problem: FreeM.Displayed.Shape is not a polynomial shape. It is a large, Sort-valued leaf/node algebra that computes a fiber recursively over a free tree.

The distinction matters:

• PFunctor.Display P is one-step polynomial data displayed over P. Its position and direction fields are Type-valued, and its polynomial object action supports dependent substitution.
• FreeM.Displayed.Algebra P α is a generic higher-order recursion algebra. Its node may use child fibers arbitrarily, including negatively or nonfunctorially.
• FreeM.Displayed D s evaluates that algebra at a concrete free tree.
• FreeM.Displayed.Over.Algebra D is a dependent second algebra over inhabitants of the first evaluated fiber; FreeM.Displayed.Over R s d evaluates it.

This PR gives those levels names that describe their actual semantics before the Aberle theory is built on top of them.

Final naming model

Before	After	Meaning
Displayed.Shape	Displayed.Algebra	leaf/node algebra generating first-layer fibers
Displayed.LocalHom	Displayed.LocalMap	constructor-local transformation data between algebras
Displayed.OverShape	Displayed.Over.Algebra	dependent algebra over a first-layer algebra
Displayed.Over.LocalHom	Displayed.Over.LocalMap	constructor-local dependent transformation over a base LocalMap
Displayed.Over.FiberLocalHom	Displayed.Over.FiberLocalMap	constructor-local dependent transformation with the base fixed
Displayed.Total	Displayed.Over.Total	total space of the first and second evaluated layers

The evaluated maps keep the categorical name:

• Displayed.Hom D E maps evaluated fibers over every tree and has extensionality, identity, composition, and associativity;
• Displayed.Over.Hom η R S does the same for evaluated second-layer fibers;
• LocalMap.toHom, Over.LocalMap.toHom, and Over.FiberLocalMap.toHom recursively interpret local rules as genuine evaluated morphisms.

Why not AlgHom?

An early version of this PR followed the usual mathlib abbreviation and called the local records AlgHom. Independent review found that this was mathematically false for the abstraction actually supported by the library.

For an arbitrary negative Algebra.node, constructor-local transformation data need not admit identity or composition. A unary counterexample is

leaf       := PUnit
node child := child unit → PEmpty

An identity-like local rule instantiated from source child PEmpty to target child PUnit would produce PUnit → PEmpty. Therefore the object may correctly be called an Algebra, but its local rule is only a LocalMap; Hom is reserved for the evaluated layer where the categorical laws really hold.

This is also why the PR does not add local id or comp operations.

API consolidation

The rename updates the whole owned surface together:

• structure fields use mapLeaf and mapNode;
• child-family binders use children, sourceChildren, and targetChildren;
• Section.ofConstruct becomes Section.ofConstructors;
• Displayed.Section is documented as a global dependent section, while Section.ofConstructors is the constructor-local fold;
• recursive theorem names use project camelCase, including liftBind;
• specializations use Decoration.algebra, Decoration.Over.algebra, Path.algebra, and PathAlong.algebra;
• local specialization constructors use Decoration.localMap, Decoration.Over.fiberLocalMap, Decoration.Over.baseLocalMap, and projectPathAlongLocalMap;
• cursor capabilities live at Displayed.Algebra.ChildProjection and Displayed.Over.Algebra.ChildProjection, with field project;
• Display.toDisplayedShape becomes Display.toDisplayedAlgebra;
• all downstream interaction consumers, tests, and wiki documentation are updated.

The change is intentionally alias-free: this surface is still in the open foundation stack, so retaining the old terminology would create a permanent duplicate API before release.

Proof-engineering findings

The review also identified representation-exposing proofs introduced during the first mechanical rename. Repeated tuple change blocks were replaced with owner-level recursion equations and explicit FreeM.liftBind_eq normalization at constructor-shaped goals.

One localized tuple normalization remains in Decoration.map_ofOver. This is intentional: rewriting its tree index first makes the dependent decoration argument ill-typed at tactic transparency, while the environment's simpNF linter requires the public simp equations in lift.bind normal form. A one-use helper would only relocate the same concrete packing dependency, so no public API was added to hide it.

The exact-head full build additionally caught two downstream rewrite consumers (TwoParty.Swap and Concurrent.Process); both now normalize explicitly before applying Decoration.map_liftBind.

What this PR does not do

• It does not identify Display with Displayed.Algebra: the former is the polynomial sublanguage; the latter is strictly more general.
• It does not add paper aliases such as DependentPFunctor or FreeDep.
• It does not add Aberle application theorems, responder semantics, or recursive wiring.
• It does not add a functorial-algebra subcategory merely to justify an AlgHom name.
• It does not add compatibility aliases for the old names.

Relationship to #74 and later work

This PR is one commit stacked directly on #74:

• exact base: 81a61aa3c2abdfd563cb91451220f6bc96af72cc
• exact head: 9f68b3da59b3bf59c38527415164dd2f1ebd0c1f

It should merge after #74. Subsequent Aberle general-theory PRs should use this head (or main after both merge), so the Display and Displayed layers have a stable vocabulary.

Validation and review

• ./scripts/validate.sh --lint --test passes at the exact head:
  • all 8,830 project build jobs;
  • umbrella-import and documentation-integrity checks;
  • environment lint;
  • all 1,967 test-library jobs.
• lake exe lint-style and git diff --check pass.
• Stale-name and trust-boundary audits found no compatibility aliases, sorry, admit, stop, new unsafe, axiom, or linter suppression.
• Hosted Lint Style and PR-summary checks pass. Full hosted build CI is absent because this stacked PR targets a non-default branch; local full validation is the authoritative gate.
• Independent review-lean-formalization review found the false AlgHom abstraction and the documentation/proof issues described above. The repair re-review confirms the mathematical issue is resolved, accepts the localized map_ofOver normalization, and found no remaining code/API issue after the final stale Path docstring was corrected.

This PR is ready for inspection but is not being merged here.

Final restack and audit (2026-07-19)

This final record supersedes earlier candidate SHA and count language above.

• Exact base: 81a61aa3c2abdfd563cb91451220f6bc96af72cc (feat(pfunctor): add polynomial displays #74)
• Exact head: 9f68b3da59b3bf59c38527415164dd2f1ebd0c1f
• Shape: 2 commits; 13 files; 418 additions; 384 deletions
• State: Ready, clean/mergeable, open, intentionally unmerged

The second commit is a narrow restack compatibility repair: the new heterogeneous-universe canaries inherited from #74 now use the renamed toDisplayedAlgebra API. No compatibility aliases or stale old identifiers were introduced. Independent exact-head review found zero P0-P3 code/API findings and reconfirmed the Algebra / LocalMap / evaluated Hom naming boundary.

Fresh exact-head ./scripts/validate.sh --lint --test passed: 8,838 build jobs, generated imports, docs integrity, environment lint, and the full test library. Style and diff checks pass. Because this PR targets a non-default stacked branch, hosted style and summary are the hosted gates; the full local validator is authoritative.

[dtumad]

Reviewed the complete Shape/LocalHom to Algebra/LocalMap migration. The new names better reflect that arbitrary local maps do not carry categorical laws, the public surface and tests are consistent, and no stale declarations remain. No blocking findings.

[dtumad]

Re-reviewed the restacked head. Range-diff shows both reviewed commits are patch-identical to the prior series, now based directly on current main; the endpoint diff is clean.