Exact expanded PA statement
exists bpr_le_gap_bb8c_twenty_three_forty_three. bpr_le_gap_bb8c_twenty_three_forty_three + (43) = (23 + 23)Structural proof guide
The checked finite cover inequality from 23 to 43.
Direct prerequisites: none. The authored body proceeds by closed numeral normalization (1).
Proof neighborhood
Direct dependencies
none
Direct dependents
Formal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.