DI0009 — divisor_complement_prefix_permutation

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 expanded first-order arithmetic statement

forall n b c. ~(n=0) -> (forall dvi_index_permutation_prefix. (exists pvs_gap_permutation_prefixdomain. pvs_gap_permutation_prefixdomain + S (dvi_index_permutation_prefix) = (S n)) -> exists dvi_value_permutation_prefix. ((((exists ff_h_pvs_permutation_prefixentry. ff_h_pvs_permutation_prefixentry + S (dvi_value_permutation_prefix) = S ((S (dvi_index_permutation_prefix)) * c)) /\ exists ff_q_pvs_permutation_prefixentry. b = ff_q_pvs_permutation_prefixentry * S ((S (dvi_index_permutation_prefix)) * c) + (dvi_value_permutation_prefix))) /\ ((((~((dvi_index_permutation_prefix)=0)) /\ ((n)=(dvi_index_permutation_prefix)*(dvi_value_permutation_prefix)))) \/ ((((dvi_index_permutation_prefix)=0 \/ ~(exists pvs_factor_permutation_prefixgraphnondivisor. (n) = (dvi_index_permutation_prefix) * pvs_factor_permutation_prefixgraphnondivisor)) /\ ((dvi_value_permutation_prefix)=(dvi_index_permutation_prefix))))))) -> (((forall pfp_i_permutation_resultbounded. (exists pfp_gap_permutation_resultboundedindex. pfp_gap_permutation_resultboundedindex + S (pfp_i_permutation_resultbounded) = (S n)) -> exists pfp_a_permutation_resultbounded. (((exists ff_h_pfp_permutation_resultboundedentry. ff_h_pfp_permutation_resultboundedentry + S (pfp_a_permutation_resultbounded) = S ((S (pfp_i_permutation_resultbounded)) * c)) /\ exists ff_q_pfp_permutation_resultboundedentry. b = ff_q_pfp_permutation_resultboundedentry * S ((S (pfp_i_permutation_resultbounded)) * c) + (pfp_a_permutation_resultbounded))) /\ (exists pfp_gap_permutation_resultboundedvalue. pfp_gap_permutation_resultboundedvalue + S (pfp_a_permutation_resultbounded) = (S n))) /\ (((forall pfp_i_permutation_resultinjective pfp_j_permutation_resultinjective pfp_a_permutation_resultinjective. (exists pfp_gap_permutation_resultinjectivefirst. pfp_gap_permutation_resultinjectivefirst + S (pfp_i_permutation_resultinjective) = (S n)) -> (exists pfp_gap_permutation_resultinjectivesecond. pfp_gap_permutation_resultinjectivesecond + S (pfp_j_permutation_resultinjective) = (S n)) -> (((exists ff_h_pfp_permutation_resultinjectiveleft. ff_h_pfp_permutation_resultinjectiveleft + S (pfp_a_permutation_resultinjective) = S ((S (pfp_i_permutation_resultinjective)) * c)) /\ exists ff_q_pfp_permutation_resultinjectiveleft. b = ff_q_pfp_permutation_resultinjectiveleft * S ((S (pfp_i_permutation_resultinjective)) * c) + (pfp_a_permutation_resultinjective))) -> (((exists ff_h_pfp_permutation_resultinjectiveright. ff_h_pfp_permutation_resultinjectiveright + S (pfp_a_permutation_resultinjective) = S ((S (pfp_j_permutation_resultinjective)) * c)) /\ exists ff_q_pfp_permutation_resultinjectiveright. b = ff_q_pfp_permutation_resultinjectiveright * S ((S (pfp_j_permutation_resultinjective)) * c) + (pfp_a_permutation_resultinjective))) -> pfp_i_permutation_resultinjective = pfp_j_permutation_resultinjective) /\ (forall pfp_a_permutation_resultsurjective. (exists pfp_gap_permutation_resultsurjectivevalue. pfp_gap_permutation_resultsurjectivevalue + S (pfp_a_permutation_resultsurjective) = (S n)) -> exists pfp_i_permutation_resultsurjective. (exists pfp_gap_permutation_resultsurjectiveindex. pfp_gap_permutation_resultsurjectiveindex + S (pfp_i_permutation_resultsurjective) = (S n)) /\ (((exists ff_h_pfp_permutation_resultsurjectiveentry. ff_h_pfp_permutation_resultsurjectiveentry + S (pfp_a_permutation_resultsurjective) = S ((S (pfp_i_permutation_resultsurjective)) * c)) /\ exists ff_q_pfp_permutation_resultsurjectiveentry. b = ff_q_pfp_permutation_resultsurjectiveentry * S ((S (pfp_i_permutation_resultsurjective)) * c) + (pfp_a_permutation_resultsurjective))))))))

Constructive proof overview

Generated structural guide

The real S n-entry complement code is bounded and injective by its proved involution; constructive finite surjectivity yields a genuine permutation.

The unchanged tactic script uses 7 declared prerequisites and contains 83 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

succ_le_succ Stable theorem; checked-use authorized DI0006 divisor_complement_bounded le_of_succ_le_succ Stable theorem; checked-use authorized DI0003 divisor_complement_functional DI0005 divisor_complement_symmetric DI0008 divisor_complement_prefix_lookup finite_bounded_injective_surjective Stable theorem; checked-use authorized

Direct dependents

DI000A positive_divisor_involution_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

83 script commands · 17 reading checkpoints · 3 local claims

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.

Named ingredients (4)

divisor complement bounded divisor complement functional divisor complement symmetric divisor complement prefix lookup

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

L1
intro n
L2
intro b
L3
intro c
L4
intro hn
L5
intro hp

02Establish hbL6–8

Establish this local claim before using it. It is not an additional assumption.

L6
have hb : BoundedPrefix(b,c,S n)Definitions: BoundedPrefix
L7
intro i
L8
intro hi

03Establish hvL9–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hp.

L9
have hv : exists q. (((((exists ff_h_pvs_permutation_at. ff_h_pvs_permutation_at + S (q) = S ((S (i)) * c)) /\ exists ff_q_pvs_permutation_at. b = ff_q_pvs_permutation_at * S ((S (i)) * c) + (q))) /\ ((((~((i)=0)) /\ ((n)=(i)*(q)))) \/ ((((i)=0 \/ ~(exists pvs_factor_permutation_compnondivisor. (n) = (i) * pvs_factor_permutation_compnondivisor)) /\ ((q)=(i)))))))
L10
specialize hp (i)
L11
apply hp
L12
exact hi

04Separate the logical casesL13–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L13
cases hv
L14
cases hv_witness

05Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

L15
exists x

06Separate the logical casesL16–16

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

L16
split

07Use earlier factsL17–26