The First Sampling Lemma — assembly

Recombines the two proved concentration events into the space-generic First Sampling Lemma, and re-hosts its downstream consumer sampling_quantitative_icl (moved verbatim from Graphon/SamplingICL.lean, where the import direction — the event theorems live downstream of SamplingICL — prevented the assembly).

• Graphon.first_sampling_lemma_of_large_k — the asymptotic form (G(k, W) → W in probability, uniformly over graphons): point_sampling_event_of_large_k (the AFKK point-sampling half, Graphon/SamplingPointwise.lean) + rounding_event_of_large_k (the finite-Chernoff rounding half, Graphon/SamplingRounding.lean) recombined via sampleGoodMassOn_of_events at accuracies (ε/2, η/4), retaining the quantified k.
• Graphon.first_sampling_lemma — the single-sample-size interface, derived.
• Graphon.exists_simpleGraph_cutDistance_lt_of_large_k / Graphon.exists_simpleGraph_cutDistance_lt — every graphon is ε-approximated in cut distance by a finite simple graph, indeed on every sufficiently large exact vertex count, with the threshold uniform over graphons.
• Graphon.exists_tendsto_cutDistance_ofSimpleGraphOn — every graphon is a cut-distance limit of finite simple graphs.
• Graphon.sampling_quantitative_icl — sampling ⟹ the K-independent quantitative ICL, by the event-intersection argument (unchanged).

Axiom accounting: both theorems are fully axiom-clean (standard axioms only). The four corrected Rokhlin cores they rest on (exists_common_coupling_maps, cutNormDiff_pullback_le, exists_controlled_cell_alignment, exists_mpEquiv_cutNormDiff_lt_add, via cutDistance_triangle) were all proved in campaigns R2–R3 from the atomless standard-Borel measure-isomorphism theorem (Graphon/MeasureIso.lean, Graphon/Overlay.lean).

theorem Graphon.first_sampling_lemma_of_large_k {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (ε η : ℝ) (hε : 0 < ε) (hη : 0 < η) : ∃ (K : ℕ), ∀ (k : ℕ), K ≤ k → ∀ (x : NeZero k) (W : Graphon α μ), 1 - η < W.sampleGoodMassOn k ε

The First Sampling Lemma, asymptotic form — G(k, W) → W in probability, uniformly over all graphons on the space.

For every accuracy ε and failure probability η there is a threshold K such that at EVERY nonzero sample size k ≥ K (the NeZero k hypothesis; sampleGoodMassOn needs a vertex to exist) and for EVERY graphon W simultaneously, the sampled graph G(k, W) lies within cut distance ε of W with probability greater than 1 − η.

Both concentration halves (point_sampling_event_of_large_k, rounding_event_of_large_k) already hold for all sufficiently large k uniformly in W; this statement simply retains that strength, where first_sampling_lemma returns a single sample size. Classical reference: Lovász, Large Networks and Graph Limits, Lemma 10.16; BCLSV, "Convergent sequences I", Thm 4.6.

theorem Graphon.first_sampling_lemma {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (ε η : ℝ) (hε : 0 < ε) (hη : 0 < η) : ∃ (k : ℕ), ∀ (W : Graphon α μ), 1 - η < W.sampleGoodMassOn (k + 1) ε

The First Sampling Lemma (space-generic interface; PROVED).

For every accuracy ε and failure probability η, some sample size k works for EVERY graphon on the space simultaneously: the sampled graph G(k, W) lies within cut distance ε of W with probability greater than 1 − η. The W-uniformity of k is the point — it is what makes the quantitative ICL below partition-size-independent, breaking the circularity documented at headline_parameter_selection.

Proof: recombination (sampleGoodMassOn_of_events) of the two concentration events at accuracy ε/2 and failure probabilities η/4: point_sampling_event_of_large_k (the analytic AFKK half) and rounding_event_of_large_k (the finite union bound over cuts), each with W-uniform threshold. Classical reference: Lovász, Large Networks and Graph Limits, Lemma 10.16; BCLSV, "Convergent sequences I", Thm 4.6.

theorem Graphon.exists_cutDistance_lt_of_sampleGoodMassOn_pos {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {W : Graphon α μ} {k : ℕ} [NeZero k] {ε : ℝ} (h : 0 < W.sampleGoodMassOn k ε) : ∃ (G : SimpleGraph (Fin k)), W.cutDistance (ofSimpleGraphOn G) < ε

Positive good mass exhibits a good graph: if the G(k, W)-mass of the event d_□(W, K_G) < ε is positive, some simple graph on k vertices realizes it.

theorem Graphon.exists_simpleGraph_cutDistance_lt_of_large_k {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {ε : ℝ} (hε : 0 < ε) : ∃ (K : ℕ), ∀ (k : ℕ), K ≤ k → ∀ (x : NeZero k) (W : Graphon α μ), ∃ (G : SimpleGraph (Fin k)), W.cutDistance (ofSimpleGraphOn G) < ε

Finite approximation at every sufficiently large size, uniformly: for every ε > 0 there is a threshold K such that every graphon is within cut distance ε of (the embedded graphon of) some simple graph on exactly k vertices, for every nonzero k ≥ K simultaneously (the NeZero k hypothesis).

theorem Graphon.exists_simpleGraph_cutDistance_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {ε : ℝ} (hε : 0 < ε) : ∃ (k : ℕ) (G : SimpleGraph (Fin (k + 1))), W.cutDistance (ofSimpleGraphOn G) < ε

Finite approximation: every graphon is within any positive cut distance of the embedded graphon of a finite simple graph (successor-indexed, so no NeZero witness is threaded through the existential — matching the first_sampling_lemma interface).

theorem Graphon.exists_tendsto_cutDistance_ofSimpleGraphOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : ∃ (G : (k : ℕ) → SimpleGraph (Fin (k + 1))), Filter.Tendsto (fun (k : ℕ) => W.cutDistance (ofSimpleGraphOn (G k))) Filter.atTop (nhds 0)

Every graphon is a cut-distance limit of finite simple graphs: there is a sequence of simple graphs, the k-th on k + 1 vertices, whose embedded graphons converge to W in cut distance.

theorem Graphon.sampling_quantitative_icl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (ε : ℝ) (hε : 0 < ε) : ∃ (δ : ℝ) (_ : 0 < δ) (m : ℕ), ∀ (U W : Graphon α μ), (∀ (F : SimpleGraph (Fin m)) [inst : DecidableRel F.Adj], |homDensity F U - homDensity F W| < δ) → U.cutDistance W < ε

Sampling ⇒ the partition-size-independent quantitative ICL — the non-circular inverse counting lemma. The parameters (δ, m) depend only on ε (through first_sampling_lemma), on NO partition cardinality: this is the K-independence that headline_parameter_selection documents as impossible for regularity bookkeeping.

Proof (event intersection): sample at accuracy ε/2, failure probability 1/4, so both U and W have own-good mass > 3/4. Hom-density δ-closeness makes the sampled distributions < 1/4-close in total variation, so U's good event keeps mass > 1/2 under W's distribution; together with W's own good event (mass > 3/4) the two events must intersect. A common good graph G gives d(U, W) ≤ d(U, K_G) + d(K_G, W) < ε. No cutDistance U W ≤ ρ hypothesis enters anywhere (that would be circular for inverse counting); only the generic event transfer sum_sampleMass_event_sub_le is used.