pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.NumberTheory.UniformFailureFloor

show as:
view Lean formalization →

The module defines the RS phase-failure floor scale KTheta. Phase-dynamics researchers cite it when bounding unresolved phases in recovered integer ledgers. It supplies the KTheta definition plus positivity lemmas drawn from J-cost and phi properties.

claimThe uniform phase-failure floor scale $K_θ$ in Recognition Science, satisfying $K_θ > 0$ and $K_θ ≥ 0$, derived from J-cost positivity on the phi ladder.

background

Recognition Science treats phase failures through a uniform floor scale that prevents persistent invisibility in integer ledgers. The module imports the RS time quantum τ₀ = 1 tick from Constants and J-cost functions from Cost. Sibling declarations introduce KTheta together with Jcost_phi_pos, KTheta_pos and KTheta_nonneg to establish the required positivity.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies the explicit KThetaFailureFloorHypothesis required by BoundedPhaseVisibility. That downstream result states that a stable unresolved-phase budget plus uniform KTheta floor implies finite phase invisibility cannot persist beyond the supplied bound. The module therefore closes the uniform-floor step in the phase-visibility chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)