Euler 1. Parameter Coercivity Collapse (10⁶⁹⁸ Hessian Spike)
Target: ./Euler/PacketInductionStage.lean · PacketSourceScaleChoice.lean · PacketSourceScaleSequence.lean
Evaluating the preprint's explicit finite parameters (Section 5.2/5.7: log k_J = x_0 / J² = 100 or x_0 = 5.0, J = 3) collapses the positive pressure Hessian increment (goodCost)[cite: 5]. At Stage J, evaluating against Lean's guards yields an initial stage defect exceeding 10⁶⁹⁸, violating Lean's initial_shear and initial_frequency bounds by hundreds of orders of magnitude[cite: 5].
Euler 2. Quantifier Decoupling & Non-Constructive Filter (X ≥ 10²⁵)
Target: ./Euler/PacketInductionScales.lean (L123–160) · PacketInfiniteConstruction.lean (L66)
Lean avoids the Section 5 coercivity collapse only by decoupling X from J[cite: 5]. The code fixes J > 89,442 and D ≥ 2000 first, replaces stage polynomials with exponential majorants, and invokes Classical.choice over a non-constructive ∀ᶠ X in atTop filter[cite: 5]. Satisfying this filter enforces X ≥ 10²⁵ (k_J ≥ exp(10¹⁵)), diverging completely from the preprint's finite parameter schedule[cite: 5].
Navier-Stokes 3. Post-Hoc Diagonal Cutoff Schedules for Exponential Mode Growth
Target: ./NavierStokes/ActualCandidateConstruction.lean · GluedStageEstimates.lean · MixedCandidateAssembly.lean
At cycle j, active harmonic modes scale as ||k|| ≤ 2^(j+1) (cycle_residualBand), causing stage derivative constants C_{j,m} to grow exponentially[cite: 5]. To establish VanishingJointJets at (1,0), exists_schedule selects the diagonal cutoff sequence a_j → ∞ only after inspecting the sequence C_{j,m}, shrinking stage supports {q(t,x) < 1/a_j} into an arbitrarily thin cusp[cite: 5].
Navier-Stokes 4. External Realization Hypothesis (PhysicalFields / PhysicalData)
Target: ./NavierStokes/ActualCycleResidualBounds.lean (L473) · GluedStageEstimates.lean
The global physical primitives are not constructed unconditionally in Cartesian coordinates. In ActualCycleResidualBounds.lean, the codebase explicitly notes: "Only the actual physical realization remains external."[cite: 5] The Cartesian fields are assumed via an external hypothesis (velocity_germ) identifying them with cylindrical graph pullbacks.
Navier-Stokes 5. Self-Documented Gaps & GraphRestriction Counterexample
Target: ./NavierStokes/GraphRestriction.lean (L16–18) · CycleContinuationInvariant.lean (L12–17)
Module headers explicitly state: "None of these statements supplies the manuscript's claimed all-order residual estimates."[cite: 5] Furthermore, GraphRestriction.lean proves an explicit counterexample (zero_mean_does_not_force_zero), establishing that zero auxiliary mean on the torus does not force zero on the restricted graph[cite: 5].
Navier-Stokes 6. Annular Zero-Germ Isolation on the Blowup Axis
Target: ./NavierStokes/ComparatorR3Theorem.lean · MixedAxisPreservation.lean (L33, L115)
All infinite wave-packet corrections vanish identically in a neighborhood of the symmetry axis r = 0 (mixedDiagonal_eq_base_germ)[cite: 5]. Consequently, the singularity along x = 0 is isolated entirely to the Stage-0 self-similar background profile FinalSlowBase, while the external force f(t,x) on [0,1) is defined tautologically as the PDE residual[cite: 5].
Navier-Stokes 7. Conditional Implication in CandidateAssembly.lean
Target: ./NavierStokes/CandidateAssembly.lean (L10–14, L214) · DiagonalJetBoundsNoOptions.lean (L9–12)
The proof of candidate properties is conditional on analytic inputs whose existence is not established in the file. Module docs state: "A conditional implication, not a proof that its analytic inputs exist... It does not construct the input fields or the future force."[cite: 5] Pointwise stage estimates remain external premises rather than derived theorems[cite: 5].
Comparator 8. Unresolved Clay Millennium Navier-Stokes Comparator
Target: ./ComparatorChallenges/NavierStokes.lean
The upstream comparator file retains intentional sorry challenge placeholders on NavierStokesExistenceAndSmoothnessRn and periodic breakdown[cite: 5]. The file explicitly clarifies: "Neither the proof root nor the submission imports this reference."[cite: 5]
Comparator 9. Unresolved Upstream Euler Breakdown Reference
Target: ./ComparatorChallenges/Euler.lean
The challenge definition for unforced Euler breakdown on ℝ³ (EulerExistenceAndSmoothnessR3) retains upstream sorry placeholders, remaining disconnected from the internal execution in Euler/Solution.lean[cite: 5].