The law of cosines over the constructed reals, in the classical c^2 = a^2 + b^2 - 2ab cos C form

Identifier: F:law-of-cosines-over-constructed-plane
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For two points (vectors) U, V of the plane CPoint over the constructed (Bishop) reals, with k and h : PosBound (||U|| ||V||) k as in F:pythagorean-identity-for-the-plane-angle, the squared distance satisfies distSq U V ~ ||U||^2 + ||V||^2 - 2 ||U|| ||V|| cosAngle(U,V), where doubling is written X + X (this development has no CReal-times-Nat scalar multiplication) and ~ is CReal.Equiv. A second, weaker and hypothesis-free form is also proved: CPoint.law_of_cosines_dot says distSq U V ~ (U.U) + (V.V) - 2(U.V) for ALL U and V, with no PosBound and no cosine -- that one is pure bilinearity of the dot product. The bridge between them is CPoint.norm_mul_cos_angle, ||U|| ||V|| cos = U.V.

Formal statement

theorem CPoint.law_of_cosines : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : AxNat) -> ((x3 : CReal.PosBound (CReal.mul (CPoint.norm x0) (CPoint.norm x1)) x2) -> CReal.Equiv (CPoint.distSq x0 x1) (CReal.add (CReal.add (CReal.mul (CPoint.norm x0) (CPoint.norm x0)) (CReal.mul (CPoint.norm x1) (CPoint.norm x1))) (CReal.neg (CReal.add (CReal.mul (CReal.mul (CPoint.norm x0) (CPoint.norm x1)) (CPoint.cosAngle x0 x1 x2 x3)) (CReal.mul (CReal.mul (CPoint.norm x0) (CPoint.norm x1)) (CPoint.cosAngle x0 x1 x2 x3)))))))))

Dependencies

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

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

Evidence

kernel-CPoint.law_of_cosines

Kind: kernel-term
Status: checked

Supports: `CPoint.law_of_cosines` and `CPoint.law_of_cosines_dot` are both admitted with exactly the types their statement pins record, with empty axiom footprints. The statement pin is the companion to the footprint check because `axiom_footprint` of an undeclared name is vacuously empty.

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": "Euclid",
      "what": "Elements II.12 and II.13, the obtuse and acute cases without a cosine",
      "where": "Elements, Book II",
      "attribution": "standard attribution; this lane did not consult the primary source."
    },
    {
      "who": "al-Kashi and later trigonometric authors",
      "what": "the modern statement with a cosine",
      "where": "conventionally attributed",
      "attribution": "standard attribution; this lane did not consult the primary source."
    }
  ]
}