PD0013 · conservative definition

BetaAt

x is the bounded beta-decoded value at index i.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Readable signature

BetaAt(b, c, i, x)

Exact expansion

((exists ff_h_defined_beta_at. ff_h_defined_beta_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_defined_beta_at. b = ff_q_defined_beta_at * S ((S (i)) * c) + (x))

This node is conservative notation, not a theorem, axiom, predicate constant, or kernel rule. Its expansion remains in the unchanged first-order language.

Definition neighborhood

Depends on conservative definitions

none

Used by conservative definitions

PD0015 Sum PD0016 AllBits PD0018 Range PD0014 Product PD0019 Repeat

All transitive conservative prerequisites

none

Used by theorem statements or local proof propositions

SL0007 bounded_gauss_lemma_complete SL000K doubling_gauss_initial_segment_complement SL000M doubling_gauss_count_shape_from_initial_segment_complement SL000N doubling_gauss_reflection_count_shape SL000Q quadratic_supplement_two_half_complete

Grand-campaign planning vocabulary

Locate Beta in the global campaign vocabulary →

Reviewed BetaAt corresponds to blueprint Beta with checked argument positions [0, 1, 2, 3].

The global atlas describes planning vocabulary and does not itself certify a definition or theorem. The reviewed expansion and conservative dependency DAG on this page are the actual family-local reading definitions.