bendprover

Solver and existence prover for the bends of unit-equilateral triangulated spheres ("nets"), at uniform multiprecision.

The pipeline is one C program, csrc/euclid_lm_mp.c: Levenberg–Marquardt with a dent gate on the quaternion holonomy system, from a closed-form wish start, at --prec bits (default 128). In --prove mode each net gets the full treatment in one invocation:

solve from scratch -> classify flat edges (1e-8) -> re-solve with
flats frozen to exactly 0 -> take-1 existence certificate
(Newton polish on quaternion pairs, numerically selected square
subsystem, Cholesky factor witness, Kantorovich) -> emit record

Records follow FORMAT.md: bends in halfturns, integer values exact (0 = flat, 1 = folded shut; degenerate pancakes are all-integer with benderr 0), decimals certified within the record's benderr, proof internals in a # provenance comment.

Build and run

make csrc/euclid_lm_mp csrc/embcheck_mp   # needs mpfr + gmp

Linear algebra: the LM normal equations are factored by a fixed-pattern sparse Cholesky (natural pivot order) by default; --dense restores the previous dense path. The sparse path performs the same mpfr operations in the same order on the nonzero pattern, skipping only operations whose operands are structural zeros, and is byte-identity-swept against --dense (full --prove transcripts) on the validation corpus before each change of default. --walk adds a gated rung-ladder fallback (59.9/59/57/54, within-member seeding only, no randomization) for nets whose direct hopestart solve dies at the dent gate; the record then carries a # route comment. --frames (with --bends-only, alpha < 60) develops the solved bends on the hyperboloid in MPFR -- solve precision sized up front from the net's face-BFS depth, since development accuracy is bounded by bend accuracy amplified e^(ell*depth) -- and emits Klein-normalized per-vertex doubles (# pos v kx ky kz 1, plus # devresid / # devbits), refusing with a stated reason whenever the emitted doubles cannot meet the acceptance (never silent).

echo 'CCAE 1,2,3;1,3,4;1,4,2;2,4,3' | csrc/euclid_lm_mp --prove --batch

Batch lines are NAME NETCODE (name optional). run/prove_v4_50.sh is the v4--50 batch driver: chunked netcode lists, one solver process per chunk.

Downstream checks

Records are the sole deliverable; consumers need nothing else.

• neoconvexity: the turning window per vertex is reported in the provenance comment and rechecked trivially from the bends.
• embeddedness: csrc/embcheck_mp.c develops ball-arithmetic vertex enclosures from (bends, benderr) and certifies shared-edge, vertex-link, and pairwise-separation conditions. Verdicts per net: PASS (embedded certified), PANCAKE (all bends integer halfturns; the flat doubly-covered case, certified by exactness, not embedded), FAIL (nothing certified). The supporting lemma (reduction of shared-vertex crossings) is documented in embcheck.py's docstring and still needs a written proof. run/embcheck_v4_50.sh sweeps a prove run's chunks.
• objs: coordinates are derived data; euclid_lm_mp NETCODE without --bends-only develops and prints them on demand.

Python oracle

mpkernel.py, netio.py, and bendprover.py are the reference solver implementation; embcheck.py and mpball.py are the reference embeddedness checker. The C programs were ported from them. make test-oracle exercises the solver reference pipeline.

Tests

make test          # format self-tests: closed-form bend checks
make test-oracle   # the Python reference pipeline