Drop the scaffolding an extracted file has no use for

[RemyDegenne]

Extracting one declaration out of a module replays that module's context commands, and until now a section/namespace block survived whenever it held a set_option — so every per-section option preamble in the source came through, declarations or not. The namespace stubs were worse: they were collected from every namespace/open in the contributing modules before filtering, so a target keeping a handful of declarations still asked for a stub for every namespace the module enters.

On a project that puts a whole development in one file this dominates the output. MetricCodes.Spherical.HigherHierarchy.main_general in ten-proofs extracted to 3237 lines for one theorem: 780 lines of namespace stubs and 440 noncomputable section/set_option/end blocks with nothing inside them. It is now 163 lines, and the corpus as a whole goes from 18.2M lines to 1.10M.

Three changes:

• set_option and universe join variable/open as soft. All four are scoped to their block, so a block holding nothing else has nothing left to act on and is dropped with them.

• Output chunks become OutChunk, carrying the namespaces each chunk needs. stripEmptyScopes returns the surviving chunks and the stub list is read off those, so a namespace no surviving line mentions is not stubbed. open … in <decl> prefixes now contribute a stub too, which they did not before.

• dropRedundantOptions removes set_option lines with no observable effect: re-setting a value already in effect (tracked on a stack that pops with each end, as Lean scopes it), and a setting immediately superseded by another of the same option.

Also fixes the root module's banner rendering as -- ═══ ═══.

Measured against the three corpora in KNOWN-ISSUES.md, comparing each changed file before and after: brownian-motion 632 files differ, 632/632 compile both ways; LML 291 differ, 707/709 both ways; alpha-rar 28 differ, 28/28 both ways. No file grew except one in brownian-motion, which gains the two-line stub the new open … in handling supplies.