version: v0.4
project:
  name: Planar Euclidean midpoint rigidity
  description: >-
    A complete Lean proof of the dimension-two case of Nielsen–Okamura
    Conjecture 9.1. On any connected open planar Euclidean domain,
    complementarity of the actual canonical local affine-parameter midpoints
    of a smooth pair of dual torsion-free connections forces the symmetric
    cubic tensor to be constant. The proof constructs and identifies the
    short geodesic germs and derives the fourth-order obstruction, including
    the exceptional rank-deficient tensors. A second theorem needs only
    everywhere Frechet differentiability and vanishing of that obstruction;
    five fixed direction tests at every point suffice. Dimensions above two
    are outside the claim.
  authors: [JD Jones]
  responsible_maintainers: [JD Jones]
  license: MIT
classification:
  arxiv: [math.DG, math.CA]
  msc2020: [53B12, 39B22]
sources:
  - title: Planar Euclidean midpoint rigidity
    type: original-proof
    authors: [JD Jones]
    relationship: other
    location: README.md
    note: >-
      This project first presents its original planar necessity proof, analytic
      bridge and differentiability strengthening. README.md accompanies the same
      development; it is not a distinct prior source work being formalized.
      The underlying general-dimensional conjecture is credited below.
      This is not a claim of worldwide priority. Material automated
      contributions are disclosed below.
  - title: Nielsen–Okamura, arXiv:2609.07551v2, Section 9
    type: paper
    authors: [Frank Nielsen, Kazuki Okamura]
    id: https://arxiv.org/html/2609.07551v2#S9
    relationship: background
    note: >-
      Source of Conjecture 9.1, the dual-geodesic midpoint expansion adapted
      here and constant-cubic sufficiency. The source states the conjecture in
      general dimension; this project supplies the original complete
      dimension-two necessity proof.
automation:
  methods:
    - method: agent
      tool_setup: OpenAI Codex with GPT-6 Astra and collaborating agents
      notes: >-
        Agents developed the proof, exact polynomial certificates, analytic
        estimates, Lean formalization and verification workflow.
        Separate agents reviewed theorem fidelity and transitive axioms.
        Tactics elaborate proof terms checked by the Lean kernel; no custom
        axiom, unsafe evaluator or external computational oracle is used.
review:
  status: agent-reviewed
  notes: >-
    Independent agent reviews checked the full midpoint hypothesis, tensor
    normalization, exceptional loci, zero values, connectedness and transitive
    axiom sets. This was internal agent review, not external human peer review.
    The workflow records verification evidence for exact-commit GitHub Actions
    runs. See Disclosure.md for the concise AI assistance statement.
fidelity:
  divergences: >-
    Full planar case only. The geometric theorem includes the local
    geodesic-to-obstruction implication and assumes no smooth family of
    endpoint solutions. The stronger C2 geometric theorem is supporting
    material rather than an additional Comparator entry.