Generated closed-face checks for genus-four cubic rows

These are the public, kernel-checked fallbacks for the three cubic rows whose closed-face proofs are represented by .rpf certificate trees. They are not intended to displace human-readable positive-length arguments:

• row 096 has the symbolic cone-march proof in LowGenus.GenusFourRow096Pencil;
• row 099 has the hand-written K₃,₃ pencil retained in the private source tree;
• row 100 has its hand-written positive-length construction retained there as well.

The generated certificates add the fact needed by the public pseudocore reduction: the same pencils survive every genus-preserving nonloopy forest face. Their Farkas receipts and firing scripts are rechecked by Lean's kernel; no external checker is trusted.

theorem AtanasovRanganathan.GenusFourGeneratedRows.row096_closed (length : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFourCubicAtlas.row096Core (Configurations.zeroSlots length)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFourCubicAtlas.row096Core (Configurations.zeroSlots length)) : Utilities.BNExists (Configurations.faceSpec GenusFourCubicAtlas.row096Core row096_closed._proof_1 length hForest hNotLoopy).graph 1 3

Closed-face degree-three pencil for public atlas row 096.

theorem AtanasovRanganathan.GenusFourGeneratedRows.row099_closed (length : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFourCubicAtlas.row099Core (Configurations.zeroSlots length)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFourCubicAtlas.row099Core (Configurations.zeroSlots length)) : Utilities.BNExists (Configurations.faceSpec GenusFourCubicAtlas.row099Core row096_closed._proof_1 length hForest hNotLoopy).graph 1 3

Closed-face degree-three pencil for public atlas row 099.

theorem AtanasovRanganathan.GenusFourGeneratedRows.row100_closed (length : Fin 9 → ℕ) (hForest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFourCubicAtlas.row100Core (Configurations.zeroSlots length)) (hNotLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFourCubicAtlas.row100Core (Configurations.zeroSlots length)) : Utilities.BNExists (Configurations.faceSpec GenusFourCubicAtlas.row100Core row096_closed._proof_1 length hForest hNotLoopy).graph 1 3

Closed-face degree-three pencil for public atlas row 100.