From 1cdc5c1b62f97758f1be358074c00b5f436d45ff Mon Sep 17 00:00:00 2001 From: Robb Walters Date: Wed, 13 May 2026 05:13:11 -0700 Subject: [PATCH] fix(mechanic): wire annotations into cauchy-schwarz-oq-03-oq-02 index.ts MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The slug's index.ts was a 4-line stub re-exporting raw meta/annotations JSON. Because `module.default` is the truthy meta dict, the `getProofAsync` fallback at src/data/proofs/index.ts never fires and ProofPage destructures undefined for `.proof`/`.annotations` — leaving 8 annotations and 10KB of section content silently unrendered. Apply the canonical full template (see merged precedents lebesgue-measure-oq-01-oq-01 #18764, konigsberg-oq-03-oq-02 #18755): typed `Proof` / `Annotation[]` / `ProofData` exports keyed off `metaJson` and a lazy import of `proofs/Proofs/CauchySchwarzOQ03OQ02.lean?raw`. Sole change: src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts (+43/-3). No meta.json / annotations.json / Lean source touched. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.7 --- .../cauchy-schwarz-oq-03-oq-02/index.ts | 46 +++++++++++++++++-- 1 file changed, 43 insertions(+), 3 deletions(-) diff --git a/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts b/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts index b98fd7b6df1..1e16449b2cc 100644 --- a/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts +++ b/src/data/proofs/cauchy-schwarz-oq-03-oq-02/index.ts @@ -1,4 +1,44 @@ -import meta from "./meta.json"; -import annotations from "./annotations.json"; +import type { Proof, Annotation, ProofData, ProofMeta, ProofSection, ProofOverview, ProofConclusion, CrossReference } from '@/types/proof' +import metaJson from './meta.json' +import annotationsJson from './annotations.json' -export { meta, annotations }; +const meta = metaJson as unknown as { + id: string + title: string + slug: string + description: string + meta: ProofMeta + sections: ProofSection[] + overview?: ProofOverview + conclusion?: ProofConclusion + crossReferences?: CrossReference[] +} + +const leanSource = () => import('../../../../proofs/Proofs/CauchySchwarzOQ03OQ02.lean?raw') + +export const cauchySchwarzOq03Oq02Proof: Proof = { + id: meta.id, + title: meta.title, + slug: meta.slug, + description: meta.description, + meta: meta.meta, + sections: meta.sections, + source: '', + overview: meta.overview, + conclusion: meta.conclusion, + crossReferences: meta.crossReferences, +} + +export const cauchySchwarzOq03Oq02Annotations: Annotation[] = annotationsJson as unknown as Annotation[] + +export const cauchySchwarzOq03Oq02Data: ProofData = { + proof: cauchySchwarzOq03Oq02Proof, + annotations: cauchySchwarzOq03Oq02Annotations, +} + +export async function getProofSource(): Promise { + const module = await leanSource() + return module.default +} + +export default cauchySchwarzOq03Oq02Data