Removing the moment assumption from a stipulated planar no-bigeodesics theorem

Taking the pinned OpenAI planar no-bigeodesics theorem and its specified proof inputs as established, we deduce absence of bigeodesics for every nonatomic law on finite nonnegative edge weights on the square lattice, without a moment or direction condition. A dependent circuit cap preserves geometric bigeodesics and supplies an integrable metric. Dominated couplings of lifted limiting graphs, label and selected-ray transfer under underlying-coordinate modifications, changed-vertex barriers and a cubic wall replace the needed finite-energy operations. The additional class is precisely the laws with infinite second moment of the minimum of four independent weights. This is conditional on the stipulated source and is not an unconditional conjecture-resolution claim.

AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review or worldwide-priority certification. Identified OpenAI source inputs at revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb are stipulated true. Lean verifies scoped supporting results only, not the full theorem. Original prose: CC BY 4.0; original code and Lean: MIT; third-party rights preserved. See the supporting archive for precise assumptions, coverage, provenance and corrections.