IndisputableMonolith.Compat.Mathlib
This module supplies targeted compatibility shims for Mathlib real-number operations inside the Recognition Science codebase. It is imported by the central Compat module so that downstream files obtain consistent access to division and positivity lemmas. The module structure is a single Mathlib import followed by four alias-style definitions.
claimCompatibility layer exporting the statements $0 < x → 0 < 1/x$, $0 ≤ x → 0 ≤ 1/x$, $(1/x)·y = y/x$, and the equivalence $0 < 1/x ↔ 0 < x$ for $x, y ∈ ℝ$.
background
The module resides in the Compat domain and performs a single import of Mathlib. It supplies four shims that re-express standard division and positivity facts under project-specific naming. These shims sit between the raw Mathlib library and the central compatibility interface used by the rest of the Recognition monolith.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module feeds the central IndisputableMonolith.Compat interface, which in turn supplies compatibility shims and project-wide constants to all downstream Recognition Science files.
scope and limits
- Does not contain any theorem proofs.
- Does not introduce new mathematical content beyond shims.
- Does not alter Mathlib definitions or axioms.
- Limited to four basic real-division lemmas.