IndisputableMonolith.Compat.Mathlib
Compat.Mathlib supplies Mathlib compatibility shims for the project. It defines four lemmas adjusting division and positivity statements on the reals. The import structure allows IndisputableMonolith.Compat to expose these to the rest of the codebase. No proofs are present; the module is purely definitional.
claimThe module provides shims for reciprocal positivity: $0 < x o 0 < 1/x$, nonnegativity $0 \leq x o 0 \leq 1/x$, multiplication $(1/x) \cdot y = y/x$, and equivalence $0 < 1/x o 0 < x$.
background
The module imports Mathlib as its sole dependency. It introduces no new definitions from the Recognition Science framework but supplies adjusted versions of standard lemmas on the reals. This supports the arithmetic foundations required for the J-cost function and defectDist calculations.
proof idea
This is a definition module with no proofs. It opens with an import of Mathlib and then declares four sibling shims for division properties.
why it matters in Recognition Science
The module feeds IndisputableMonolith.Compat, described as the central compatibility imports for the project. It enables access to shims and constants for downstream modules working on the phi-ladder and eight-tick octave.
scope and limits
- Does not introduce Recognition Science specific constants such as phi or G.
- Does not contain any theorem statements or proofs.
- Does not import any project-internal modules beyond Mathlib.
- Does not address the Recognition Composition Law or mass formula.