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.
Exact expanded PA statement
forall n. 1 * n = nStructural proof guide
Generated structural guide
One is a left identity for multiplication.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (1), certified simplification (2).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
PA000N mul_eq_one_components PA001P gauss_coprime_cancel PA002N le_scaled_nonzero PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA005E pow_predecessor_parity_mod PA005T pow_one_from_zero_successor PA00AK bounded_mod_inverse_unique PA007N beta_product_pointwise_mul_exact PA007Q beta_product_pointwise_scale_mod PA00AO inverse_prefix_zero_fixed PA00B9 beta_adjacent_unit_pairs_product_one PA00BI mod_one_product_restore_predecessor PA00DQ odd_half_cross_product_gapFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.