UpperHeadSharpSplit

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Sharp separation estimates for the framed wave-head lane

The literal squared wave-head estimate carries gamma * hsep. The first part of this file prices that factor in Gamma_1. The resulting ordinary coordinate lane is controlled in Gamma_1, while the residual lane has exponent Gamma_((1 - sigma) / 3) and an explicit scale bounded by the eighth power of the frozen exceptional scale.

Spatial maxima, coordinate traces, and root/depth aggregation remain downstream.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHeadHsepOneScale (sigma gamma : ℝ) : ℝ

The Gamma_1 scale obtained by taking the upperProfileBaseSigma sigma power of the proved exponential hsep tail.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperHeadHsepOneScale_pos {sigma gamma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma : 0 < gamma) : 0 < upperHeadHsepOneScale sigma gamma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileBase_three_rpow_bfa_hsep {d : ℕ} (M : ABKModel d) (root : ℤ) {E : { E : ℝ // 1 ≤ E }} (hSroot : Frozen.Section3.inductionState M (root - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileBaseSigma sigma)) (fun (omega : Cutoff.CutoffSample d) => 3 ^ (bfaProfileB * ↑(Percolation.hsep M root (↑E) bfaProfileB omega))) (Percolation.hsepAmplitude (upperProfileSigma sigma) bfaProfileB)

Under the frozen profile gates, the basic hsep exponential at the fixed profile slope has exponent upperProfileBaseSigma sigma.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_gammaSigma_one_gamma_mul_hsep {d : ℕ} (M : ABKModel d) (root : ℤ) {E : { E : ℝ // 1 ≤ E }} (hSroot : Frozen.Section3.inductionState M (root - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => M.gamma * ↑(Percolation.hsep M root (↑E) bfaProfileB omega)) (upperHeadHsepOneScale sigma M.gamma)

The sharp squared-head factor gamma * hsep is Gamma_1 at an explicit scale. The proof uses the power rule on the proved exponential hsep tail; no new probabilistic premise is exposed.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedDepthDecay {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) : ℝ

The depth-decay factor in the tuned good-head estimate.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedDepthDecay M E k = 3 ^ (-(M.gamma * (↑k + ↑(Algsuperdiff.Section3.Provider.CoarseEllipticity.collarBandMeanDepth M E))))

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedLayerBase {d : ℕ} (M : ABKModel d) (n : ℕ) : ℝ

The deterministic per-layer base in the tuned good-head estimate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedBaseTerm {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) : ℝ

The complete deterministic coefficient of one tuned good-head layer. The factorization keeps the full k + n + ceil + k₀ negative offset.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedCoordinateCoeff {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) (j : Fin d) : ℝ

The deterministic coefficient for one coordinate of the tuned good-head estimate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedCoordinateLane {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The coordinate budget proportional to the sample's separation height.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedOrdinaryCoordinateLane {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The doubled coordinate budget used for the ordinary good-head contribution.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedRareCoordinateLane {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The coordinate budget multiplied by the residual rare-event factor.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedCoordinateScale {d : ℕ} (M : ABKModel d) (E sigma : ℝ) (k : ℕ) (j : Fin d) : ℝ

The stochastic scale assigned to one tuned good-head coordinate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedOrdinaryCoordinateScale {d : ℕ} (M : ABKModel d) (E sigma : ℝ) (k : ℕ) (j : Fin d) : ℝ

The doubled stochastic scale for the ordinary coordinate contribution.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedOrdinaryCoordinateScale M E sigma k j = 2 * Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedCoordinateScale M E sigma k j

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedRareCoordinateScale {d : ℕ} (M : ABKModel d) (E sigma : ℝ) (k : ℕ) (j : Fin d) : ℝ

The product-tail stochastic scale for the rare coordinate contribution.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedCoordinateWhitneySum {d : ℕ} (M : ABKModel d) (m : ℤ) (R : HCPolySupport.TriadicCube d) (E : ℝ) (j : Fin d) (omega : Cutoff.CutoffSample d) : ℝ

The Whitney layer sum for one coordinate of the tuned good-head contribution.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_depth_decay_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) : 0 ≤ goodHeadTunedDepthDecay M E k

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_layer_base_nonneg {d : ℕ} (M : ABKModel d) (n : ℕ) : 0 ≤ goodHeadTunedLayerBase M n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_base_term_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k n : ℕ) : 0 ≤ goodHeadTunedBaseTerm M E k n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_good_head_tuned_layer_base {d : ℕ} (M : ABKModel d) : Summable fun (n : ℕ) => goodHeadTunedLayerBase M n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_good_head_tuned_base_term {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) : Summable fun (n : ℕ) => goodHeadTunedBaseTerm M E k n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_coordinate_coeff_nonneg {d : ℕ} (M : ABKModel d) (E : ℝ) (k : ℕ) (j : Fin d) : 0 ≤ goodHeadTunedCoordinateCoeff M E k j

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_coordinate_lane_nonneg {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : 0 ≤ goodHeadTunedCoordinateLane M root E k j omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_rare_coordinate_lane_nonneg {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : 0 ≤ goodHeadTunedRareCoordinateLane M root E k j omega

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_good_head_tuned_coordinate_lane {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) : Measurable (goodHeadTunedCoordinateLane M root E k j)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.measurable_good_head_tuned_rare_coordinate_lane {d : ℕ} (M : ABKModel d) (root : ℤ) (E : ℝ) (k : ℕ) (j : Fin d) : Measurable (goodHeadTunedRareCoordinateLane M root E k j)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_coordinate_scale_nonneg {d : ℕ} (M : ABKModel d) (E sigma : ℝ) (k : ℕ) (j : Fin d) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : 0 ≤ goodHeadTunedCoordinateScale M E sigma k j

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodWavePart_le_good_head_tuned_factor {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E : ℝ) (n : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : Multiscale.probeSharpFramedGoodWavePart M R.scale E bfaProfileB (collarBandMeanDepth M E) n (m - 1) (HCPolySupport.basisVec j) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale E bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M E) n) eta ^ 2) omega ≤ Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j) * (Multiscale.probeSharpAfterBandHsepFactor M R.scale E omega * (goodHeadTunedBaseTerm M E k n * (M.gamma * ↑(Percolation.hsep M R.scale E bfaProfileB omega))))

Literal summand 2 with the complete tuned negative offset retained.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.probeSharpFramedGoodWavePart_le_good_head_tuned_ordinary_add_rare {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (n : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale (↑E) bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) ≤ have eta := Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega; have C := Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j); have B := goodHeadTunedBaseTerm M (↑E) k n; have G := M.gamma * ↑(Percolation.hsep M R.scale (↑E) bfaProfileB eta); C * (2 * (B * G)) + C * (Multiscale.probeSharpAfterBandHsepResidual M R.scale (↑E) eta * (B * G))

splits the retained framed power without touching the tuned decay.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_coordinate_whitney_sum_le_ordinary_add_rare {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) (omega : Cutoff.CutoffSample d) : goodHeadTunedCoordinateWhitneySum M m R (↑E) j omega ≤ goodHeadTunedOrdinaryCoordinateLane M R.scale (↑E) k j (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) + goodHeadTunedRareCoordinateLane M R.scale (↑E) k j (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_gammaSigma_one_good_head_tuned_ordinary_coordinate_lane_comp {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => goodHeadTunedOrdinaryCoordinateLane M R.scale (↑E) k j (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) (goodHeadTunedOrdinaryCoordinateScale M (↑E) sigma k j)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_good_head_tuned_rare_coordinate_lane_comp {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) : HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) (fun (omega : Cutoff.CutoffSample d) => goodHeadTunedRareCoordinateLane M R.scale (↑E) k j (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) (goodHeadTunedRareCoordinateScale M (↑E) sigma k j)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedMassSumConst (d : ℕ) : ℝ

The constant bounding the sum of tuned good-head layer masses.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedMassSumConst d = 5 * ↑d ^ 2 * √(6 * ↑d) * Algsuperdiff.Section3.Provider.Multiscale.waveL4HeadConst d ^ 2 * (1 - 3 ^ (-(1 / 2)))⁻¹

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedHsepOneConst : ℝ

The good-head constant converting separation height into a linear budget.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedCoordinateConst (d : ℕ) : ℝ

The dimension-dependent constant for the tuned coordinate estimate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedRarePrefactor (d : ℕ) : ℝ

The prefactor assigned to the rare part of the tuned coordinate estimate.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.goodHeadTunedOutputConst (d : ℕ) : ℝ

A common output constant dominating the tuned good-head budgets.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.good_head_tuned_output_const_pos {d : ℕ} (hd : 2 ≤ d) : 0 < goodHeadTunedOutputConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_good_head_tuned_finite_trace_split {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hstate : Frozen.Section3.inductionState M (m - 1) E) {sigma Cup : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (Cup / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (houtput : goodHeadTunedOutputConst d ≤ Cup) : ∃ (ordinary : Cutoff.CutoffSample d → ℝ) (rare : Cutoff.CutoffSample d → ℝ) (ordinaryScale : ℝ) (rareScale : ℝ), (∀ (omega : Cutoff.CutoffSample d), 0 ≤ ordinary omega) ∧ Measurable ordinary ∧ (∀ (omega : Cutoff.CutoffSample d), 0 ≤ rare omega) ∧ Measurable rare ∧ (∀ (omega : Cutoff.CutoffSample d), ∑ j : Fin d, goodHeadTunedCoordinateWhitneySum M m R (↑E) j omega ≤ ordinary omega + rare omega) ∧ (∀ (omega : Cutoff.CutoffSample d), ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale (↑E) bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) = ENNReal.ofReal (∑ j : Fin d, goodHeadTunedCoordinateWhitneySum M m R (↑E) j omega)) ∧ (∀ (omega : Cutoff.CutoffSample d), ∑ j : Fin d, ∑' (n : ℕ), ENNReal.ofReal (Multiscale.probeSharpFramedGoodWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale (↑E) bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) ≤ ENNReal.ofReal (ordinary omega) + ENNReal.ofReal (rare omega)) ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) ordinary ordinaryScale ∧ 0 ≤ ordinaryScale ∧ ordinaryScale ≤ upperSaturatedPerCubeAmplitude Cup (Disorder.cstar M) M.gamma k ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 3)) rare rareScale ∧ 0 ≤ rareScale ∧ rareScale ≤ Real.exp (-(Cup⁻¹ * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) ^ 8

Terminal finite-coordinate split for literal summand 2 of the sharp per-cube estimate. The two witnesses are explicit nonnegative measurable lanes. Their scales are paid, respectively, by the saturated ordinary amplitude and by the fixed eighth-power exceptional reserve.