The law of sines over the constructed reals, as |U x V| = ||U|| ||V|| sin, with the cross product identified with the existing triangle determinant

Identifier: F:law-of-sines-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, |U x V| ~ ||U|| ||V|| sinAngle(U,V), where |.| is CReal.abs, U x V is CPoint.crossV, and ~ is CReal.Equiv. Separately and definitionally, CPoint.cross_eq_crossV proves cross A B C ~ crossV (sub B A) (sub C B) BY equiv_refl: the three-point triangle determinant the library already had IS the two-vector cross product at the two edge vectors. So the left side is twice the area of the triangle, and this is also the (1/2) a b sin C area formula.

Formal statement

theorem CPoint.law_of_sines : ((x0 : CPoint) -> ((x1 : CPoint) -> ((x2 : AxNat) -> ((x3 : CReal.PosBound (CReal.mul (CPoint.norm x0) (CPoint.norm x1)) x2) -> CReal.Equiv (CReal.abs (CPoint.crossV x0 x1)) (CReal.mul (CReal.mul (CPoint.norm x0) (CPoint.norm x1)) (CPoint.sinAngle 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_sines

Kind: kernel-term
Status: checked

Supports: `CPoint.law_of_sines` and `CPoint.cross_eq_crossV` are admitted with exactly the types their statement pins record, with empty axiom footprints. `new_definitions_have_the_intended_value` additionally pins `crossV`'s VALUE at a symbolic argument and asserts it still contains a `CReal.neg`, because the kernel cannot tell you a definition is wrong -- a symmetric `crossV` would type-check and would make this statement false.

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": "Nasir al-Din al-Tusi and earlier Indian and Islamic authors",
      "what": "the law of sines for plane triangles",
      "where": "conventionally attributed",
      "attribution": "standard attribution; this lane did not consult the primary source."
    }
  ]
}