mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
allaun
00e9eed399
Replace the TODO(lean-port) sorry with a complete proof of the
projectionOrdering theorem: for positive SourceValue pairs s1 < s2
with s2 ≤ maxExpected, projectToCoding preserves strict ordering
of the Q0_64 values.
The proof uses Nat-only arithmetic (no Float) and handles two cases:
- a2 < d: both values fit in Q0_64 range, ordering follows from
monotonicity of integer division
- a2 = d: a2*s/d = s clamped to q0_64MaxRaw; a1*s/d < q0_64MaxRaw
via the key inequality (d-1)*s < (s-1)*d
Build: 8598 jobs, 0 errors (lake build)
|
||
|---|---|---|
| .. | ||
| ARTIFACT_NORMALIZATION.md | ||
| AUTHORITY_MATRIX.md | ||
| GITHUB_MISSING_MAP.md | ||
| GRAPH_TOPOLOGY_EXPORT.md | ||
| PLUMBING_V0_COMPLETION_GATE.md | ||
| PROJECT_DOMAIN_TYPE_MAP.md | ||