The Cauchy-Schwarz inequality over the constructed reals, in squared form, with the dot product a genuine inner product

Identifier: F:cauchy-schwarz-over-constructed-plane
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any two points (vectors) U, V of the plane CPoint = CReal x CReal over the constructed (Bishop) reals, (U.V)^2 <= (U.U)(V.V), where U.V is CPoint.dot and <= is CReal.le. THIS IS THE SQUARED FORM AND IT IS NOT A WEAKENING: the familiar |<U,V>| <= ||U||*||V|| requires a square root on CReal, which this kernel does not have -- only CReal.natSqrt, an integer square root -- so the norm form is not expressible here at all, not merely inconvenient. The squared form is equivalent to it modulo sqrt and is what every downstream estimate uses. Alongside it, CPoint.dot satisfies all three inner-product axioms over this carrier: symmetry (CPoint.dot_comm), bilinearity (the dot_add_left/right, dot_sub_left/right, dot_neg_left family), and positive-definiteness (CPoint.dot_self_zero_iff : dot V V ~ 0 <-> V ~ 0). Equality throughout is CReal.Equiv / CPoint.Equiv, DEFINED Prop relations on a setoid, never Eq.

Formal statement

theorem CPoint.cauchy_schwarz : ((x0 : CPoint) -> ((x1 : CPoint) -> CReal.le (CReal.mul (CPoint.dot x0 x1) (CPoint.dot x0 x1)) (CReal.mul (CPoint.dot x0 x0) (CPoint.dot x1 x1))))

Dependencies

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

21 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-CPoint.cauchy_schwarz

Kind: kernel-term
Status: checked

Supports: `CPoint.cauchy_schwarz` is admitted with exactly the type in formal.statement. The proof is ALGEBRA, not analysis: `CPoint.lagrange_identity` establishes (a^2+b^2)(c^2+e^2) - (ac+be)^2 = (ae-bc)^2 as a ring identity over CReal, so the gap between the two sides of Cauchy-Schwarz is a square, and one application of CReal.sq_nonneg closes it. Landing Lagrange's identity as its own named theorem rather than inlining it records WHERE the inequality comes from.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal_point::creal_point_tests::cauchy_schwarz_statement_is_exact -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

A footprint check cannot carry this claim: a theorem stating something weaker -- the two factors on the right transposed, or a different inequality direction -- has exactly the same empty footprint. Mutation-verified: changing `CPoint.dot x0 x0` to `CPoint.dot x0 x1` in the pinned string makes cargo report `40 passed; 1 failed`, naming this test and no other; restored, 41/41 green. The command re-derives from source every run, rebuilding CPointPrelude through add_declaration, and is anchored on the exact `1 passed; 0 failed` count so an unmatched filter -- which prints `running 0 tests ... ok` and exits 0 -- cannot read as success.

footprint-CPoint.cauchy_schwarz

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for cauchy_schwarz, lagrange_identity, dot_self_nonneg, dot_self_zero_iff and everything beneath them -- the CReal ordered field, sq_nonneg, and the dot bilinearity family. The `cpoint` prelude's trusted surface is 0: no Axiom, no Opaque, no Quotient.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib creal_point::creal_point_tests::every_theorem_here_is_axiom_free -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Counting Declaration::Axiom alone would not suffice in this kernel (Opaque has no proof body and Quotient admits Quot.sound); axiom_footprint covers all three. Presence matters as much as the footprint -- axiom_footprint of a name interned but never DECLARED is vacuously empty -- which is why the statement pin, which fetches the declaration from the environment and panics if absent, is the companion check and not optional.

Provenance

{
  "date": "2026-08-24",
  "established_by": "lane agent-capability-assurance (2026-08-24) via two dispatched lanes: CPoint.cauchy_schwarz and CPoint.lagrange_identity in creal_point.rs, then CPoint.dot_self_zero_iff and CReal.eq_zero_of_add_eq_zero_of_nonneg completing the inner-product axioms. Kernel theorems over CReal (the constructed reals, ADR-0512), all with empty axiom_footprint.",
  "source": "classical",
  "prior_art": [
    {
      "who": "Augustin-Louis Cauchy",
      "what": "the inequality for finite sums",
      "year": 1821,
      "where": "Cours d'Analyse de l'Ecole Royale Polytechnique, Note II",
      "attribution": "standard attribution; this lane did not consult the primary source."
    },
    {
      "who": "Viktor Bunyakovsky and Hermann Schwarz",
      "what": "the integral forms",
      "year": 1859,
      "where": "Bunyakovsky 1859; Schwarz 1888",
      "attribution": "conventional. The plane case proved here is Cauchy's finite-sum version at n = 2 and does not require the integral generalisation."
    },
    {
      "who": "Joseph-Louis Lagrange",
      "what": "the identity (a^2+b^2)(c^2+e^2) - (ac+be)^2 = (ae-bc)^2",
      "year": 1773,
      "where": "conventionally attributed; the two-square case is older in substance",
      "attribution": "noted because the proof here goes through the identity rather than through an analytic argument, so the identity is the load-bearing prior art."
    }
  ]
}