Isometries of the constructed plane: the monoid, translations, rotations and reflections as instances, and a constructive refutation that doubling is one

Identifier: F:plane-isometries-and-the-doubling-non-example
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Define, for a map f : CPoint -> CPoint over the constructed (Bishop) reals, Isometry f := forall P Q, distSq (f P) (f Q) ~ distSq P Q, with ~ being CReal.Equiv and distSq the squared Euclidean distance. Then: the identity map is an isometry and the composite of two isometries is an isometry (so isometries form a monoid under composition); every translate T (P |-> P + T) is an isometry with NO hypothesis at all; and for any two reals c, s with c^2 + s^2 ~ 1, both rotate c s (P |-> (c Px - s Py, s Px + c Py)) and reflect c s (P |-> (c Px + s Py, s Px - c Py)) are isometries. NO ANGLE IS FORMED ANYWHERE: a rotation is parameterised by the normalised PAIR (c, s), never by an angle, so nothing here needs arccos. Separately, scale r (P |-> (r Px, r Py)) satisfies distSq (scale r P) (scale r Q) ~ r^2 distSq P Q exactly, and the doubling map is REFUTED as an isometry: CPoint.not_isometry_scale_two proves Isometry (scale 2) -> False.

Formal statement

theorem CPoint.not_isometry_scale_two : ((x0 : CPoint.Isometry (CPoint.scale CPoint.Scalar.two)) -> False)

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

23 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CPoint.not_isometry_scale_two

Kind: kernel-term
Status: checked

Supports: The refutation and all six positive instances (`isometry_id`, `isometry_comp`, `isometry_translate`, `isometry_rotate`, `isometry_reflect`, `scale_distSq`) are admitted with exactly the types their statement pins record, with empty axiom footprints. THE EXIT STATUS DEPENDS ON THE FINDING IN BOTH DIRECTIONS: `a_theorem_here_proves_only_its_own_statement` re-offers `isometry_id`'s proof value at the type `Isometry (scale CPoint.Scalar.two)` and FAILS unless the kernel refuses it, and re-offers `isometry_rotate`'s value at `isometry_reflect`'s type (the two differ only in two signs) and fails unless that too is refused. Each row carries a matched positive control -- the same value at its own type under a fresh name, which must be ADMITTED -- so the check cannot pass by being unable to admit anything at all.

Checker command

cargo test --release -p axeyum-lean-kernel --lib creal_point:: -- --test-threads=4

Provenance

{
  "date": "2026-09-04",
  "established_by": "lane angles-and-isometries (2026-09-04), roadmap W1-8/W2-13, ADR-1615. Kernel theorems over CReal (the constructed Bishop reals, ADR-0512) in crates/axeyum-lean-kernel/src/creal_point/angle.rs and creal_point/isometry.rs, all admitted through Kernel::add_declaration with an empty axiom_footprint.",
  "source": "classical",
  "prior_art": [
    {
      "who": "classical Euclidean geometry",
      "what": "the isometry group of the plane and its generators",
      "where": "standard",
      "attribution": "standard attribution; this lane did not consult a primary source."
    }
  ]
}