# A finite-dimensional Hilbert certificate from one matrix

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-real-hilbert-space/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-real-hilbert-space-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Verify the consistent inner product, norm, metric and completeness of R^2 with A=[[2,1],[1,2]].

Only this finite-dimensional real carrier; no infinite-dimensional, compactness or separability claim.





## Givens and symbols


- algebra
- inner_norm_metric
- finite_dim_complete


- G1 — V=R^2, A=[[2,1],[1,2]]; define <x,y>_A=x^T A y and derive both norm and metric from this same inner product.


- A — fixed positive-definite matrix
- \|\ \|_A,d_A — matching norm and metric





## Rules and sources


- mko_definition · cited — The carrier, inner product, induced norm, induced metric and completeness certificate must describe the same space. This slice uses named completeness-theorem certificates for finite-dimensional R^n with a standard or positive-definite-matrix inner product. Sampled Cauchy sequences do not establish completeness. · mko-real-hilbert-space
- algebra · prerequisite — Use real-field identities; division requires a nonzero denominator and multiplication by a positive number preserves inequalities.
- inner_norm_metric · prerequisite — A positive-definite symmetric bilinear form defines a real inner product; its square-root self-product is a norm, including the triangle inequality, and the difference norm is a metric.
- finite_dim_complete · prerequisite — Named completeness certificate: every finite-dimensional real inner-product space is complete in the norm and metric induced by that inner product.





## Main derivation

S01 · equivalentBefore

x=(x_1,x_2),\ y=(y_1,y_2)

After

\langle x,y\rangle_A=2x_1y_1+x_1y_2+x_2y_1+2x_2y_2

Conditions: none

Rule: algebra · Uses: G1

Leaf basis: algebra

Expand the matrix product, fixing A as the common source of every structure.



S02 · equivalentBefore

\langle ax+bz,y\rangle_A

After

a\langle x,y\rangle_A+b\langle z,y\rangle_A

Conditions: none

Rule: algebra · Uses: S01

Leaf basis: algebra

Distributivity gives real bilinearity termwise; the expanded expression also gives symmetry.



S03 · equivalentBefore

\langle x,x\rangle_A=2x_1^2+2x_1x_2+2x_2^2

After

\langle x,x\rangle_A=(x_1+x_2)^2+x_1^2+x_2^2\ge0

Conditions: none

Rule: algebra · Uses: S01

Leaf basis: algebra

The sum of squares is nonnegative, and equality forces both coordinates zero, proving positive definiteness.



S04 · impliesBefore

V=\mathbb R^2,\ \langle\ ,\ \rangle_A\text{ symmetric bilinear positive definite}

After

(V,\langle\ ,\ \rangle_A)\text{ is a real inner-product space}

Conditions: none

Rule: inner_norm_metric · Uses: G1, S02, S03

Leaf basis: inner_norm_metric

All inner-product obligations are met, qualifying the space first.



S05 · theorem_applicationBefore

\|x\|_A=\sqrt{\langle x,x\rangle_A}

After

\|x\|_A=\sqrt{2x_1^2+2x_1x_2+2x_2^2}

Conditions: none

Rule: inner_norm_metric · Uses: S04

Leaf basis: inner_norm_metric

By the inner-product induced-norm theorem this is a norm, using the nonnegative square root.



S06 · theorem_applicationBefore

d_A(x,y)=\|x-y\|_A

After

d_A(x,y)=\sqrt{2(x_1-y_1)^2+2(x_1-y_1)(x_2-y_2)+2(x_2-y_2)^2}

Conditions: none

Rule: inner_norm_metric · Uses: S05

Leaf basis: inner_norm_metric

The same norm induces the metric; its norm properties give nonnegativity, separation, symmetry and triangle inequality.



S07 · impliesBefore

(x_1+x_2)^2\le2(x_1^2+x_2^2)

After

\|x\|_2^2\le\|x\|_A^2\le3\|x\|_2^2

Conditions: none

Rule: algebra · Uses: S03, S05

Leaf basis: algebra

The upper bound follows from (x_1-x_2)^2≥0 and the lower from the sum of squares, additionally checking the norm binding.



S08 · theorem_applicationBefore

\dim_{\mathbb R}V=2<\infty

After

(V,\langle\ ,\ \rangle_A,\|\ \|_A,d_A)\text{ is a real Hilbert space}

Conditions: V=\mathbb R^2; A=A^T\text{ positive definite}

Rule: finite_dim_complete · Uses: G1, S04, S05, S06

Leaf basis: finite_dim_complete

Apply the named finite-dimensional real-inner-product completeness theorem: every d_A-Cauchy sequence has a d_A-limit in the same V, which supplies the Hilbert obligation.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S04, S05, S06 — The certificate binds the same carrier, product, norm and metric; sampled Cauchy sequences cannot replace it.
- S07 · premise_audit · S03, S05 — The bounds hold for all real vectors but imply no unprovided infinite-dimensional result.
- S06 · premise_audit · S05 — Every difference vector stays in the same V.
- S05 · premise_audit · S04 — No different matrix or unbound norm may be substituted.
- S04 · premise_audit · G1, S02, S03 — The carrier remains R^2, not the subset of rational vectors.
- S03 · inverse_equivalence · S01 — No determinant shortcut or numerical sample replaces the all-x proof.
- S02 · inverse_equivalence · S01 — a,b are arbitrary real scalars, not sampled integers.
- S01 · inverse_equivalence · G1 — Swapping x,y preserves the expression, including both cross coefficients.





## Error controls and negative controls

Five-way bindingKeep V, A, inner product, norm and metric consistently bound.

Named completenessExplicitly apply finite-dimensional real-inner-product completeness, not samples.


- Replacing R^2 by Q^2 permits the same real finite-dimensional theorem. → reject — Q^2 is not a real vector space, so the carrier premise fails.
- Finitely checking Cauchy sequences proves completeness. → reject — Completeness quantifies over every Cauchy sequence.
- Hilbert therefore makes this space compact. → reject — No compactness certificate is supplied; R^2 itself is unbounded.





## Result and limitations

This R^2, with all structures induced by the same A, is a real Hilbert space; completeness is supplied by the finite-dimensional completeness theorem.







## Verification and source binding

1 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 4930257bba12534036e760dca2b4c1277cdaeb84ac961481c36f384db87a6209
- original source SHA-256: 1dfb783bf683beff32490fed97cb7f8755ddeca7526828da95db41018e1e36fd
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-real-hilbert-space-01.json)