Cauchy-Schwarz in R^n at SYMBOLIC dimension, in its unsquared norm form

Identifier: F:rn-cauchy-schwarz-symbolic-dimension
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For vectors u, v of R^n and every natural number n, <u,v>_n <= ||u||_n * ||v||_n, where <u,v>_n is the sum of u_i*v_i for i < n and ||u||_n is the square root of <u,u>_n. The dimension n is a UNIVERSALLY QUANTIFIED VARIABLE, not a literal: this is one theorem about every finite-dimensional real inner-product space, not a family of theorems one per dimension. Two things distinguish it from what the library had. First the form: `Rat.dotN_cauchy_schwarz` (rationals, symbolic dimension) and `CPoint.cauchy_schwarz` (reals, dimension 2) are both SQUARED, because Q has no square root and because the plane development predates `CReal.sqrt`; the unsquared form needs a norm and hence a root. Second the dimension: `Metric.CPoint.dotLeSqrtMul` is unsquared but only on the plane. This statement is the first that is both.

Formal statement

theorem RN.cauchy_schwarz : ((x0 : RN.Vec) -> ((x1 : RN.Vec) -> ((x2 : AxNat) -> CReal.le (RN.dot x0 x1 x2) (CReal.mul (RN.norm x0 x2) (RN.norm x1 x2)))))

Dependencies

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

3 direct dependencies 1 direct dependents

Evidence

kernel-RN.cauchy_schwarz

Kind: kernel-term
Status: checked

Supports: RN.cauchy_schwarz is admitted by the trusted kernel gate with the type recorded in formal.statement, and Kernel::axiom_footprint reports 0 assumed names.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection -- --require-declaration RN.cauchy_schwarz | grep -cE '^found[[:space:]]+rn[[:space:]]+theorem[[:space:]]+RN\.cauchy_schwarz[[:space:]]+0$'

Evidence notes

The exit status depends on the finding twice over: kernel_declaration_projection exits NON-ZERO when the named declaration is in no constructed prelude's environment, and grep -c then exits 1 printing 0 if the anchored row is absent or its axiom-footprint column is not 0. Anchored with [[:space:]], never \t: in a scripted (GNU) grep \t is a literal t, and 68 fact checkers in this ledger were wrong for exactly that reason. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this binary builds creal/complex/cpoint/metric/rn, which overflow the default debug thread stack. The `rn` label did not exist in this tool before the commit of record; without it the tool is blind to the prelude, which is indistinguishable from the declaration not existing -- exactly the failure ADR-1602 recorded for `metric`.

rn-statement-exactness

Kind: witness-replay
Status: checked

Supports: that the statement is the UNSQUARED form at a bound dimension, and not a squared or fixed-dimension statement that would also typecheck

Checker command

cargo test --release -p axeyum-lean-kernel --lib rn:: -- --test-threads=2

Evidence notes

24 tests, all green, ~75 s in release. Mutation-verified: substituting the real distance into the squared-distance instance control kills exactly one test, and dropping one row from the declaration list kills exactly one test.

Provenance

{
  "date": "2026-09-04",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_rn_prelude (crates/axeyum-lean-kernel/src/rn.rs)",
  "source": "Lane `rn-carrier`, roadmap W2-4 (convergence point C7), design recorded in ADR-1606 (docs/research/09-decisions/adr-1606-rn-is-a-function-carrier-with-the-dimension-in-the-relation.md). formal.statement is Kernel::render_lean of the declaration's type, taken verbatim from the unfiltered emit of `kernel_declaration_projection`; axiom_footprint is that tool's footprint-size column, which reads Kernel::axiom_footprint."
}