RootClauseBRebasedWellPlaced #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
1. The hgradE identity at the re-based family, at the gate #
The hgradE identity at the gate, at the re-based family.
The gate identity for the child's flux-corrected family, with that family
replaced by parentRebasedFamily: both have
symmetric part ν Id, so the identity is unchanged.
2. The coarse solution object at the well-placed frame, re-based #
The Caccioppoli's coarse solution object at the print's own frame centre, at
the re-based family. The coarse-frame solution object with the family moved
onto parentRebasedFamily through InteriorRebase's equation transport; the
gate is discharged from k ≤ m alone, so no geometry binder survives.
3. The energy-norm domination at the well-placed frame, re-based #
The coarse hgradE slot at the re-based family, at no geometry binder.
The coarse-frame energy-norm domination with the family moved onto
parentRebasedFamily; the constant is still the printed volume ratio
rootClauseBTopKg d m k.