A First Accepted Submission.

The contribution

PR #1 adds LeanFrontier.Geometry.InversiveGeometry. Its two public theorems characterize the fixed points of reflection across a generalized circle and show that reflection is an involution away from its poles.

import LeanFrontier.Geometry.InversiveGeometry

#check LeanFrontier.InversiveGeometry.reflect_eq_self_iff
#check LeanFrontier.InversiveGeometry.reflect_reflect

The submission describes its mathematical source honestly: the underlying geometry is classical textbook material, not a claim of new mathematics. The contribution is an importable Lean formalization and a first real exercise of the receiver.

What the receiver observed

The accepted run built the candidate in the restricted environment, found no exact match in the pinned Mathlib fingerprint index, and completed a fresh downstream-import smoke test. Both declared entrypoints have the permitted foundational axiom closure: propext, Classical.choice, and Quot.sound. The baseline triviality probes were inconclusive, which is recorded rather than treated as evidence either way.

The complete, versioned receiver observation is kept alongside the corpus. The theorem catalogue links each public entrypoint to it.

A bootstrap lesson

The first submission exposed several receiver issues that ordinary unit tests did not: transient dependency downloads, report paths under a capability-restricted container, and a race between trusted generated-file workflows. Those were repaired without changing the submitted source or its immutable claim. The successful acceptance is therefore evidence about both the module and the boundary that admitted it.

What comes next

LeanFrontier remains deliberately small. The immediate work is to make this first version easy to pin and import, preserve its receiver evidence, and invite further carefully specified submissions. Read the contract before proposing one.