pith. sign in
module module high

IndisputableMonolith.NumberTheory.HonestPhaseAdmissibility

show as:
view Lean formalization →

HonestPhaseAdmissibility module defines when honest phase data counts as admissible by requiring its realized sampled family to carry finite total annular J-cost. Researchers assembling the analytic trace to RH bridge cite it as the finite-budget gate. The module supplies definitions and equivalence statements after importing the axiom-free AnalyticTrace infrastructure.

claimHonest phase data is admissible when its realized sampled family has finite recognition budget, i.e., bounded total annular J-cost.

background

The module imports AnalyticTrace, whose documentation states it assembles the full RH bridge from analytic trace infrastructure after replacing former axioms with contour winding results. In Recognition Science, J-cost is the recognition effort functional appearing in the Recognition Composition Law, and annular sampling refers to phase data collected in successive annuli around the origin. The module introduces HonestPhaseAdmissible together with charge-zero equivalences and bridge maps that link admissibility to zero-free criteria.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the admissibility gate consumed by RH_From_RCL, the final assembly that reduces the Riemann Hypothesis to the explicit BoundaryTransportCert form of the RS physical bridge. The module therefore closes the analytic admissibility step between the trace infrastructure and the RCL-derived RH statement.

scope and limits

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)