Unconditional existence on genus-four Core 095

This file assembles the three Atanasov--Ranganathan length comparisons and then removes the normalization L₀ ≤ L₅ by the exact Core-095 involution. The result is a kernel-checked degree-three rank-one divisor for every positive integral subdivision of the public row-095 core.

theorem LowGenus.GenusFourRow095.bnExists_one_three_normalized (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) (hNorm : length 0 ≤ length 5) : Utilities.BNExists (Spec length hLength).graph 1 3

The three signed-window branches cover every normalized positive length assignment.

theorem LowGenus.GenusFourRow095.bnExists_one_three (length : Fin 9 → ℕ) (hLength : ∀ (edge : Fin 9), 0 < length edge) : Utilities.BNExists (Spec length hLength).graph 1 3

Every positive integral subdivision of catalog Core 095 carries a degree-three rank-one divisor.