Pith. sign in
module module moderate

IndisputableMonolith.Foundation.Gap45_Exact_v2

show as:
view Lean formalization →

Foundation module packaging the exact Gap-45 certificate (version 2): a domain cost, its pointwise evaluation identity and nonnegativity, a strictly positive canonical threshold, and an inhabited certificate record. Mass-ladder and residue-arithmetic arguments in RS cite this bundle when they need a closed Gap-45 witness. The module is mostly definitional scaffolding plus short positivity and equality lemmas over Cost and Constants.

claimThe module introduces a domain cost $C$, the identity relating $C$ at a distinguished point, the inequality $C \ge 0$, a canonical threshold $\tau > 0$, and an inhabited certificate type witnessing the exact Gap-45 (v2) package in RS-native units.

background

Recognition Science builds particle and geometric structure on the J-cost and the phi-ladder. The Cost import supplies the cost primitive (the unique symmetric convex generator fixed by the Recognition Composition Law and T5). Constants supplies the RS time quantum $\tau_0 = 1$ tick and the golden-ratio units in which rung arithmetic is written.

Gap-45 is the exact integer offset that appears in the mass-ladder exponent (yardstick times $\phi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$) and in related residue counts. This module is the v2 packaging of that exact gap: it names a domain-restricted cost, records how that cost evaluates, proves nonnegativity, and fixes a positive canonical threshold against which the gap certificate is checked.

Sibling names in the module (domain cost, threshold positivity, certificate inhabitance) indicate a small closed data bundle rather than a long forcing-chain derivation. Upstream edges are only the Constants and Cost modules.

proof idea

Definition-and-certificate module, not a deep tactic proof. It defines the domain cost and the canonical threshold, then records short supporting facts: evaluation identity at the distinguished point, nonnegativity of the cost, positivity of the threshold, and inhabitance of the Gap45ExactV2Cert record (via an explicit cert value). No multi-step forcing or analytic estimates appear at module scope; the work is packaging and discharging the certificate interface over Cost/Constants.

why it matters in Recognition Science

Gives a reusable, exact Gap-45 (v2) witness inside Foundation so later mass-ladder, residue, or certificate-driven arguments can import one inhabited record instead of re-proving cost nonnegativity and threshold positivity. Downstream use edges are empty in the current graph, so this module is a leaf provider rather than a step inside a named parent theorem. It sits beside the phi-ladder mass formula and the Z-dependent gap term in the RS primer, and it depends only on the cost primitive and RS-native constants. Anyone auditing exact integer gap claims in the monolith should treat this as the v2 source of the Gap-45 certificate shape.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)