MC000E — divisor_prime_toggle_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.

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ n. ∀ p. ∀ b. ∀ c. ¬n = 0 → Prime(p) → Dvd(p,n) → DivisorPrimeTogglePrefix(n,p,b,c,S n) → PermutationPrefix(b,c,S n)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PermutationPrefix(b,c,l) · 1 DivisorPrimeToggle(n,p,d,e) · 1 DivisorPrimeTogglePrefix(n,p,b,c,l) · 1 Dvd(d,n) · 1 Prime(p) · 1 BetaAt(b,c,i,x) · 1 BoundedPrefix(b,c,l) · 1 InjectivePrefix(b,c,l) · 1

Actual proof prerequisites

succ_le_succ · checked external prerequisite divisor_prime_toggle_bounded le_of_succ_le_succ · checked external prerequisite divisor_prime_toggle_functional divisor_prime_toggle_symmetric divisor_prime_toggle_prefix_lookup finite_bounded_injective_surjective · checked external prerequisite

Original expanded first-order statement

forall n p b c. ~(n=0) -> (~((p) = 1) /\ forall pvs_left_permutation_prime pvs_right_permutation_prime. (p) = pvs_left_permutation_prime * pvs_right_permutation_prime -> pvs_left_permutation_prime = 1 \/ pvs_right_permutation_prime = 1) -> (exists pvs_factor_permutation_prime_divisor. (n) = (p) * pvs_factor_permutation_prime_divisor) -> (forall dvi_index_permutation_source. (exists pvs_gap_permutation_sourcedomain. pvs_gap_permutation_sourcedomain + S (dvi_index_permutation_source) = (S n)) -> exists dvi_value_permutation_source. ((((exists ff_h_pvs_permutation_sourceentry. ff_h_pvs_permutation_sourceentry + S (dvi_value_permutation_source) = S ((S (dvi_index_permutation_source)) * c)) /\ exists ff_q_pvs_permutation_sourceentry. b = ff_q_pvs_permutation_sourceentry * S ((S (dvi_index_permutation_source)) * c) + (dvi_value_permutation_source))) /\ ((((~((dvi_index_permutation_source)=0)) /\ (((exists pvs_factor_permutation_sourcegraphdivisor. (n) = (dvi_index_permutation_source) * pvs_factor_permutation_sourcegraphdivisor) /\ ((((~(exists pvs_factor_permutation_sourcegraphtogglefresh_input. (dvi_index_permutation_source) = (p) * pvs_factor_permutation_sourcegraphtogglefresh_input)) /\ ((dvi_value_permutation_source)=(p)*(dvi_index_permutation_source)))) \/ (((((dvi_index_permutation_source)=(p)*(dvi_value_permutation_source)) /\ (~(exists pvs_factor_permutation_sourcegraphtogglefresh_output. (dvi_value_permutation_source) = (p) * pvs_factor_permutation_sourcegraphtogglefresh_output)))) \/ (((exists pvs_factor_permutation_sourcegraphtogglesquare. (dvi_index_permutation_source) = ((p)*(p)) * pvs_factor_permutation_sourcegraphtogglesquare) /\ ((dvi_value_permutation_source)=(dvi_index_permutation_source)))))))))) \/ ((((dvi_index_permutation_source)=0 \/ ~(exists pvs_factor_permutation_sourcegraphnondivisor. (n) = (dvi_index_permutation_source) * pvs_factor_permutation_sourcegraphnondivisor)) /\ ((dvi_value_permutation_source)=(dvi_index_permutation_source))))))) -> (((forall pfp_i_permutation_targetbounded. (exists pfp_gap_permutation_targetboundedindex. pfp_gap_permutation_targetboundedindex + S (pfp_i_permutation_targetbounded) = (S n)) -> exists pfp_a_permutation_targetbounded. (((exists ff_h_pfp_permutation_targetboundedentry. ff_h_pfp_permutation_targetboundedentry + S (pfp_a_permutation_targetbounded) = S ((S (pfp_i_permutation_targetbounded)) * c)) /\ exists ff_q_pfp_permutation_targetboundedentry. b = ff_q_pfp_permutation_targetboundedentry * S ((S (pfp_i_permutation_targetbounded)) * c) + (pfp_a_permutation_targetbounded))) /\ (exists pfp_gap_permutation_targetboundedvalue. pfp_gap_permutation_targetboundedvalue + S (pfp_a_permutation_targetbounded) = (S n))) /\ (((forall pfp_i_permutation_targetinjective pfp_j_permutation_targetinjective pfp_a_permutation_targetinjective. (exists pfp_gap_permutation_targetinjectivefirst. pfp_gap_permutation_targetinjectivefirst + S (pfp_i_permutation_targetinjective) = (S n)) -> (exists pfp_gap_permutation_targetinjectivesecond. pfp_gap_permutation_targetinjectivesecond + S (pfp_j_permutation_targetinjective) = (S n)) -> (((exists ff_h_pfp_permutation_targetinjectiveleft. ff_h_pfp_permutation_targetinjectiveleft + S (pfp_a_permutation_targetinjective) = S ((S (pfp_i_permutation_targetinjective)) * c)) /\ exists ff_q_pfp_permutation_targetinjectiveleft. b = ff_q_pfp_permutation_targetinjectiveleft * S ((S (pfp_i_permutation_targetinjective)) * c) + (pfp_a_permutation_targetinjective))) -> (((exists ff_h_pfp_permutation_targetinjectiveright. ff_h_pfp_permutation_targetinjectiveright + S (pfp_a_permutation_targetinjective) = S ((S (pfp_j_permutation_targetinjective)) * c)) /\ exists ff_q_pfp_permutation_targetinjectiveright. b = ff_q_pfp_permutation_targetinjectiveright * S ((S (pfp_j_permutation_targetinjective)) * c) + (pfp_a_permutation_targetinjective))) -> pfp_i_permutation_targetinjective = pfp_j_permutation_targetinjective) /\ (forall pfp_a_permutation_targetsurjective. (exists pfp_gap_permutation_targetsurjectivevalue. pfp_gap_permutation_targetsurjectivevalue + S (pfp_a_permutation_targetsurjective) = (S n)) -> exists pfp_i_permutation_targetsurjective. (exists pfp_gap_permutation_targetsurjectiveindex. pfp_gap_permutation_targetsurjectiveindex + S (pfp_i_permutation_targetsurjective) = (S n)) /\ (((exists ff_h_pfp_permutation_targetsurjectiveentry. ff_h_pfp_permutation_targetsurjectiveentry + S (pfp_a_permutation_targetsurjective) = S ((S (pfp_i_permutation_targetsurjective)) * c)) /\ exists ff_q_pfp_permutation_targetsurjectiveentry. b = ff_q_pfp_permutation_targetsurjectiveentry * S ((S (pfp_i_permutation_targetsurjective)) * c) + (pfp_a_permutation_targetsurjective))))))))

Complete tactic proof in conservative notation

All 99 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

99 script commands · 18 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)

divisor prime toggle bounded divisor prime toggle functional divisor prime toggle symmetric divisor prime toggle prefix lookup

01Fix variables and assumptionsL1–8

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

L1
intro n
L2
intro p
L3
intro b
L4
intro c
L5
intro hn
L6
intro hp
L7
intro hpn
L8
intro hprefix

02Establish hbL9–11

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

L9
have hb : BoundedPrefix(b,c,S n)Definitions: BoundedPrefix(b,c,S n)Original native command in the exact edition
L10
intro i
L11
intro hi

03Establish hvL12–15

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

L12
have hv : ∃ e. BetaAt(b,c,i,e) ∧ DivisorPrimeToggle(n,p,i,e)Definitions: BetaAt(b,c,i,e)DivisorPrimeToggle(n,p,i,e)Original native command in the exact edition
L13
specialize hprefix (i)
L14
apply hprefix
L15
exact hi

04Separate the logical casesL16–17

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

L16
cases hv
L17
cases hv_witness

05Construct an explicit witnessL18–18

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

L18
exists x

06Separate the logical casesL19–19

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

L19
split

07Use earlier factsL20–29