High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.ExplicitScheduledRate

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

(δ), the core: the scheduled rate at an explicit C₀

the flux scheduled rate at the witness (UniformFluxScheduledRateExtraction:36) selects its constant as A.toReal, where

A = ofReal outputFactor * ofReal Cdual *
      ((Cbesov² · ofReal Kflux)^(1/2) · hardyConstant^(1/2) +
       (Cbesov² · ofReal Kflux)^(1/2) · hardyConstant^(1/2))

and hides it behind an ∃. Because the witness is opaque, the module can only conclude ∃ C₀, 0 ≤ C₀ s ρ Rad ∧ … with C₀ bound inside ∀ abar U s ρ Rad — which is exactly the defect the restated Dirichlet clause forbids.

This module repeats that proof with the head named and bounded: scheduledRateHead is A, and rowConvertedFluxScheduledRateAtWitness_of_head_le delivers RowConvertedFluxScheduledRateAtWitness d C₀ … for any C₀ dominating the head. scheduledRateHead_le_ofReal then converts a real-valued bound on the four factors into that domination, so a law-free C₀ can be built from the ρ-paid output factor, the flux slot split, that module (the energy collapse) and the uniform Hardy constant.

The Hardy-top premise is not needed here: it served only to know A ≠ ⊤ so that A.toReal could be formed. With the head bounded rather than reified, the hypothesis drops.

noncomputable def HCPolySupport.HighContrast.RowSupply.scheduledRateHead (d : ℕ) (outputFactor Cdual Kflux : ℝ) (hardyConstant : ENNReal) : ENNReal

The head of the scheduled rate: module the A premise, named.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RowSupply.rowConvertedFluxScheduledRateAtWitness_of_head_le {d : ℕ} {g kappaRate Cdual : ℝ} {capFlux hardyConstant boundaryEnergy : ENNReal} {s rho Rad epsilon Xval outputFactor : ℝ} {C₀ : ℝ → ℝ → ℝ → ℝ} (hbase : 0 ≤ epsilon * Xval) (hBoundaryTop : boundaryEnergy ≠ ⊤) {Kflux : ℝ} (hKflux : 0 ≤ Kflux) (hFlux : capFlux ≤ ENNReal.ofReal (Kflux * (epsilon * Xval) ^ (2 * kappaRate)) * boundaryEnergy) (hC₀ : 0 ≤ C₀ s rho Rad) (hhead : scheduledRateHead d outputFactor Cdual Kflux hardyConstant ≤ ENNReal.ofReal (C₀ s rho Rad)) : RowConvertedFluxScheduledRateAtWitness d C₀ g kappaRate Cdual capFlux hardyConstant boundaryEnergy s rho Rad epsilon Xval outputFactor

(δ), the core. The converted flux rate holds at any C₀ that dominates the scheduled head — in particular at a law-free one.

The real-valued bridge

theorem HCPolySupport.HighContrast.RowSupply.scheduledRateHead_le_ofReal (d : ℕ) {outputFactor Cdual Kflux hardyReal : ℝ} (hout : 0 ≤ outputFactor) (hCdual : 0 ≤ Cdual) (hKflux : 0 ≤ Kflux) (hhardyReal : 0 ≤ hardyReal) {hardyConstant : ENNReal} (hhardy : hardyConstant ≤ ENNReal.ofReal hardyReal) : scheduledRateHead d outputFactor Cdual Kflux hardyConstant ≤ ENNReal.ofReal (outputFactor * Cdual * (2 * ((fractionalDualToBesovConstant d).toReal * (√Kflux * √hardyReal))))

The head, bounded in real terms. All four factors of the scheduled head are real (the Hardy constant through any real dominating it), so a law-free C₀ built from the modules named above dominates it.