High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorComposition.BlockRowSupplyProjection
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
RootBlockRowSupply against the ceiling-exporting smallness interface — what is carried and #
what is not
The stationary corrector family clause reduces to
def RootBlockRowSupply (d : ℕ) [NeZero d]
(GoodScale : Mat d → CoeffSpace d → ℝ → Prop) : Prop :=
∀ (abar : Mat d), (symmPart abar).PosDef →
∀ (a : CoeffSpace d) (x : ℝ), GoodScale abar a x →
∃ (Omega : Set (CoeffSpace d)) (s rho kappa delta : ℝ)
(S X : CoeffSpace d → ℝ),
a ∈ Omega ∧
(∀ z : Fin d → ℤ, translateCoeff z ⁻¹' Omega = Omega) ∧
0 < s ∧ s < 1 / 2 ∧
0 < rho ∧ rho ≤ 1 ∧ rho < 2 * s ∧
0 < kappa ∧ 0 ≤ delta ∧
∀ b ∈ Omega, 1 ≤ X b ∧ S b ≤ X b ∧
Quenched.HasAllLaterPhysicalBlockRow rho kappa delta
(Book.Ch02.constantBlockMatrix abar) S X b
(order-free form: the order s is supplied here, not frozen upstream; the
statement is restated below rather than imported, because importing it would
pull in the whole normalized-supply chain at the free order.)
What rootGoodScaleAt literally carries #
Destructuring rootGoodScaleAt d g c kappaRate abar a x gives
h : RowSupply.RowRetainingPrintOrderGoodScale d g c kappaRate abar a x, and
that structure carries, for the sample a only:
| demanded field | carried by | status |
|---|---|---|
rho | Certificate.printRowOrder g = (1 + 3 * g) / 4 | ✓ |
0 < rho ∧ rho ≤ 1 | g ∈ Ico 0 1 arithmetic | ✓ |
kappa and 0 < kappa | 2 * kappaRate, positive from the hole's own 0 < κ | ✓ |
delta, 0 ≤ delta | h.delta, h.delta_nonneg | ✓ |
S, X | h.sourceScale, h.activationScale | ✓ |
1 ≤ X a, S a ≤ X a | h.activation_one, h.source_le_activation | ✓ at a |
the row at a | h.row, at Book.Ch02.constantBlockMatrix abar | ✓ at a |
s with 0 < s < 1/2 and rho < 2 * s | the printed order (1 + g) / 4, chosen after g | ✓ |
Omega with ∀ z, translateCoeff z ⁻¹' Omega = Omega, a ∈ Omega, and the row **at every `b ∈ | ||
| Omega`** | — | x the missing field |
The single missing field is the translation-invariant event. The
certificate is a per-sample predicate: it carries the row at a and at no other
sample. The demanded Omega exists — it is hquenched's OmegaEnd, which
carries MeasurableSet, P.real = 1, the literal
∀ z, translateCoeff z ⁻¹' OmegaEnd = OmegaEnd, and
∀ a ∈ OmegaEnd, HasAllLaterPhysicalBlockRow ((1 + 3 * g) / 4) kappa delta Abar S X a
— but hhomogenized's binder surface applies one sample at a time
(… (a : CoeffSpace d), HasAllLaterPhysicalBlockRow … S X a → 1 ≤ X a → S a ≤ X a → GoodScale g kappaRate abar a …), so the event is discarded before
GoodScale is formed. No choice of Omega repairs this downstream:
Omega = {a} is not translation invariant, Omega = univ does not carry the
row, and the orbit of a carries the row only if the row is already known at
every integer translate — which is the demand itself.
The second missing field was an order window, not a datum — and it is now
gone. At the stationary corrector family clause's frozen rootCorrectorOrder = 3/16 the window
rho < 2 * rootCorrectorOrder read (1 + 3 * g) / 4 < 3 / 8, i.e. g < 1/6
(still proved below, as the record of what the frozen order cost). The
corrector datum records its order as a field rather than reading a
global constant, so the supply chooses the order after g, at the printed
(1 + g) / 4; the corrector cone s < 1/2 and the window rho < 2 * s are
then both equivalent to g < 1, and the admitted range is the whole of
Ico 0 1.
The repair, machine-checked: the event-retaining certificate #
Widen the certificate by the event and widen hhomogenized correspondingly.
Both directions are proved here:
- the event-level supply theorem — the event-retaining certificate discharges
RootBlockRowSupplyoutright (given the window); exists_rootGoodScaleOn_of_quenchedEventRow—hhomogenizedstill holds at the event-retaining certificate, from exactly the datahquenchedalready produces, with no new hypothesis.
So the event-retaining certificate is a pure binder-surface change to hhomogenized: replace its
per-sample row premise by the event-level one that the assembly already has in
hand at the point of application.
The stationary corrector family clause's demand, restated #
The order window #
The per-g order, and the exact admitted range #
The order the supply chooses is the printed certificate order
HighContrast.printCertificateOrder g = (1 + g) / 4, selected after g. At
that order the two constraints the supply must meet — the corrector cone
0 < s < 1/2 and the window printRowOrder g < 2 * s — are both equivalent
to g < 1, so the admitted range is exactly Ico 0 1: the whole root range,
and nothing is admitted beyond it.
The event-retaining certificate the event-retaining certificate #
The block-row event. Exactly the data hquenched produces, restricted
to what RootBlockRowSupply reads: a translation-invariant set carrying the
sample, and the physical block row on all of it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The event-retaining certificate: the ceiling-exporting smallness interface with the producing event retained.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The discharge #
hhomogenized at the event-retaining certificate #
hhomogenized survives the widening. From the event-level row —
which is precisely what hquenched hands the assembly — the event-retaining certificate holds at
every sample of the event, at every corrector smallness.
No new hypothesis is introduced: the premises below are hquenched's own
OmegaEnd data.