Press n or j to go to the next uncovered block, b, p or k for the previous block.
| 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 | 1x 1x 1x 1x 1x 1x 1x 1x 307x 307x 1x 1x 44x 44x 1x 1x 441x 441x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 26x 26x 1x 1x 47x 47x 1x 1x 6x 6x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 1x 32x 32x | /** Distance between two points (canonical: IDs sorted lexicographically) */
export interface DistancePair {
readonly a: string
readonly b: string
}
/** Create a canonical DistancePair (IDs sorted lexicographically) */
export function distancePair(p: string, q: string): DistancePair {
return p <= q ? { a: p, b: q } : { a: q, b: p }
}
export function distancePairsEqual(x: DistancePair, y: DistancePair): boolean {
return x.a === y.a && x.b === y.b
}
export function distancePairKey(dp: DistancePair): string {
return `${dp.a}|${dp.b}`
}
// ── Angle measure ─────────────────────────────────────────────────
/** An angle defined by a vertex and two ray endpoints (canonical: ray endpoints sorted) */
export interface AngleMeasure {
readonly vertex: string
readonly ray1: string
readonly ray2: string
}
/** Create a canonical AngleMeasure (ray endpoints sorted lexicographically) */
export function angleMeasure(vertex: string, r1: string, r2: string): AngleMeasure {
return r1 <= r2 ? { vertex, ray1: r1, ray2: r2 } : { vertex, ray1: r2, ray2: r1 }
}
export function angleMeasureKey(am: AngleMeasure): string {
return `∠${am.vertex}|${am.ray1}|${am.ray2}`
}
export function angleMeasuresEqual(x: AngleMeasure, y: AngleMeasure): boolean {
return x.vertex === y.vertex && x.ray1 === y.ray1 && x.ray2 === y.ray2
}
// ── Citations ─────────────────────────────────────────────────────
export type Citation =
| { type: 'def15'; circleId: string }
| { type: 'cn1'; via: DistancePair } // transitivity through shared equal
| { type: 'cn2' } // addition (C.N.2)
| { type: 'cn3'; whole: DistancePair; part: DistancePair } // subtraction
| { type: 'cn3-angle'; whole: AngleMeasure; part: AngleMeasure } // angle subtraction
| { type: 'cn4' } // superposition (C.N.4)
| { type: 'given' } // hypothesis / given fact
| { type: 'prop'; propId: number }
// ── Equality facts ────────────────────────────────────────────────
export interface EqualityFact {
readonly id: number
readonly left: DistancePair
readonly right: DistancePair
readonly citation: Citation
readonly statement: string // "CA = AB"
readonly justification: string // "Def.15: C on circle centered at A through B"
readonly atStep: number
}
export interface AngleEqualityFact {
readonly id: number
readonly left: AngleMeasure
readonly right: AngleMeasure
readonly citation: Citation
readonly statement: string // "∠ABC = ∠DEF"
readonly justification: string
readonly atStep: number
}
/** Union of all fact types in the proof engine */
export type ProofFact = EqualityFact | AngleEqualityFact
/** Type guard: true if the fact is an AngleEqualityFact */
export function isAngleFact(fact: ProofFact): fact is AngleEqualityFact {
return 'vertex' in fact.left
}
|