Route AAssembly

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The Route A one-round interfaces: the producer propositions consumed by the bootstrap round, together with the round's exponent arithmetic.

This producer is the explicit global-to-local seam for a heat-potential core. It records both the a.e. carrier identification and the conversion from scalar component norms to the vector Morrey membership used by Route A.

def CKN.Core.Step4.routeACarrierRestrictionProducer : Prop

Transfer a scalar norm bound to componentwise Morrey bounds after restriction and a.e. equality.

Equations

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

theorem CKN.Core.Step4.routeA_carrier_restriction_producer_of_core : routeACarrierRestrictionProducer

theorem CKN.Core.Step4.routeA_round_exponents : 2 * (25 / 11) < 5 ∧ 1 / (25 / 11) - 2 / 5 = 1 / 25 ∧ 6 / 5 / (1 - 2 * (25 / 11) / 5) = 66 / 5 ∧ 25 / 11 / (1 - 2 * (25 / 11) / 5) = 25

The following producer types are the exact boundaries consumed by the one-round argument. They keep the pressure-gradient construction, the local heat representation, and the quarter-radius conclusion separate until their analytic implementations are available. The gradient boundary states a Morrey membership, so it carries no Calderón--Zygmund constant: the L^{6/5} control needed to build the selected field belongs to the construction that discharges this interface, not to its statement.

def CKN.Core.Step4.routeAGradientProducer : Prop

Pressure-gradient construction interface used in the Morrey bootstrap route.

Equations

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

def CKN.Core.Step4.routeARepresentationProducer : Prop

Weak-equation interface supplying the localized heat-potential representation.

Equations

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