theorem G12AuthorOutput.admitted_boundary_mesh (τ : ℝ) (hτ : 0 < τ) : ∃ (ρ : ℝ), 1 < ρ ∧ ρ ≤ 3 / 2 ∧ ∀ (ε : ℝ), 0 < ε → ε ≤ 2 / 15 → ∃ (K : ℕ), 4 ≤ K ∧ ∀ N ≥ K, Even N → G12BandOutput.boundaryOutput ρ N ε ≤ τ * G12BandOutput.HN N

A mesh simultaneously legal for the paid boundary and the safe C2 grid.

theorem G12AuthorOutput.one_le_authorWeight {N : ℕ} (hN : 4 ≤ N) (r : ℕ) : 1 ≤ MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorPrimeWeight N r

theorem G12AuthorOutput.safe_subset_mother {N : ℕ} (hN : 1 ≤ N) (ρ ε : ℝ) : G12SafeGridBudget.safeUnion ρ N ε ⊆ G12FlexibleRectangle.mother N ε

theorem G12AuthorOutput.safe_authorMass_le {N : ℕ} (hN : 4 ≤ N) (ρ ε : ℝ) {t : ℝ} (ht : 0 ≤ t) : ∑ p ∈ G12SafeGridBudget.safeUnion ρ N ε, MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12NormalizedCoefficient N p.1 * (MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11AuthorWeight (Real.log ↑p.2 / Real.log ↑N) + t) ≤ (1 + t) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG12AuthorLowMotherMass N ε

theorem G12AuthorOutput.highMass_nonneg (N : ℕ) (ε : ℝ) : 0 ≤ G12ClippedWindow.highMass N ε

theorem G12AuthorOutput.choose_loss (B τ : ℝ) (hτ : 0 < τ) : ∃ (t : ℝ), 0 < t ∧ t ≤ 1 ∧ (1 + t) * (B + t) + 3 * t ≤ B + τ

Fixed scalar loss, chosen before all analytic and mesh thresholds.