Item 14: Faithful acceleration: exact inherited status, and what ports

Determine exactly what the inherited deference development establishes about faithful acceleration, separating results that are algebraic consequences of named Logical Induction hypotheses from results derived through market/trader machinery. Then port as much as legitimately ports onto the pinned dependency.

The ledger's rows for this movement are attested by the inherited audit and have not been rebuilt in this repository; the inherited tree carries its own toolchain. Confirming or correcting those rows against the source is part of the item.

Deliverable shape: a dependency map, plus either lean-proved entries in Workspace.Deference.Contrib for whatever ports, each with an inhabitation witness, or a precise obstruction. A compiling partial port with an exact dependency map is a success. Acceptance check: the lean gate builds and audits clean; each registered entry names a declaration that exists and ships a typechecking witness term.

Context: projects/deference/note-dump-2026-08-11/lean-deference/ and its AUDIT.md; lean/Workspace/Deference/. For the statement of the positive result, projects/deference/note-dump-2026-08-11/wiki/faithful-acceleration-result.md and projects/deference/note-dump-2026-08-11/wiki/delay-and-visibility.md — not note-dump-2026-06-27/notes/faithful-acceleration.md, whose §5 strength ladder the source line's own adjudication found wrong and two of whose lines it found false. That file is retained as history and is superseded for the statement. A solution ships: the strongest inherited theorem stated exactly, its hypotheses classified as derived / cited / modelling substitution, the mapping onto the pinned dependency's endpoints, and the exact residual market-trader gap. Not permitted: strengthening an inherited theorem to fit the current narrative.