inductive Hex.Nat.PMinusOneResult : Type

The three semantically distinct stage-1 gcd outcomes.

• noFactor : PMinusOneResult
• factor (value : Nat) : PMinusOneResult
• whole : PMinusOneResult

@[instance_reducible]

instance Hex.Nat.instReprPMinusOneResult : Repr PMinusOneResult

Equations

• Hex.Nat.instReprPMinusOneResult = { reprPrec := Hex.Nat.instReprPMinusOneResult.repr }

def Hex.Nat.instReprPMinusOneResult.repr : PMinusOneResult → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.instDecidableEqPMinusOneResult : DecidableEq PMinusOneResult

Equations

• Hex.Nat.instDecidableEqPMinusOneResult = Hex.Nat.instDecidableEqPMinusOneResult.decEq

def Hex.Nat.instDecidableEqPMinusOneResult.decEq (x✝ x✝¹ : PMinusOneResult) : Decidable (x✝ = x✝¹)

Equations

• Hex.Nat.instDecidableEqPMinusOneResult.decEq Hex.Nat.PMinusOneResult.noFactor Hex.Nat.PMinusOneResult.noFactor = isTrue ⋯
• Hex.Nat.instDecidableEqPMinusOneResult.decEq Hex.Nat.PMinusOneResult.noFactor (Hex.Nat.PMinusOneResult.factor value) = isFalse ⋯
• Hex.Nat.instDecidableEqPMinusOneResult.decEq Hex.Nat.PMinusOneResult.noFactor Hex.Nat.PMinusOneResult.whole = isFalse Hex.Nat.instDecidableEqPMinusOneResult.decEq._proof_2✝
• Hex.Nat.instDecidableEqPMinusOneResult.decEq (Hex.Nat.PMinusOneResult.factor value) Hex.Nat.PMinusOneResult.noFactor = isFalse ⋯
• Hex.Nat.instDecidableEqPMinusOneResult.decEq (Hex.Nat.PMinusOneResult.factor a) (Hex.Nat.PMinusOneResult.factor b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.Nat.instDecidableEqPMinusOneResult.decEq (Hex.Nat.PMinusOneResult.factor value) Hex.Nat.PMinusOneResult.whole = isFalse ⋯
• Hex.Nat.instDecidableEqPMinusOneResult.decEq Hex.Nat.PMinusOneResult.whole Hex.Nat.PMinusOneResult.noFactor = isFalse Hex.Nat.instDecidableEqPMinusOneResult.decEq._proof_7✝
• Hex.Nat.instDecidableEqPMinusOneResult.decEq Hex.Nat.PMinusOneResult.whole (Hex.Nat.PMinusOneResult.factor value) = isFalse ⋯
• Hex.Nat.instDecidableEqPMinusOneResult.decEq Hex.Nat.PMinusOneResult.whole Hex.Nat.PMinusOneResult.whole = isTrue ⋯

@[instance_reducible]

instance Hex.Nat.instInhabitedPMinusOneResult : Inhabited PMinusOneResult

Equations

• Hex.Nat.instInhabitedPMinusOneResult = { default := Hex.Nat.instInhabitedPMinusOneResult.default }

structure Hex.Nat.PMinusOneAttempt : Type

The result of one counted deterministic stage-1 call. A call is one attempt on every terminal gcd outcome. Pollard p - 1 draws no randomness, so the returned generator is exactly the supplied state; carrying it here lets randomized callers resume through the same boundary as rho.

• result : PMinusOneResult

  The terminal gcd outcome.

• attempts : Nat

  Semantic stage-1 calls executed; always one at this boundary.

• rand : Rand

  The unchanged generator state.

@[instance_reducible]

instance Hex.Nat.instReprPMinusOneAttempt : Repr PMinusOneAttempt

Equations

• Hex.Nat.instReprPMinusOneAttempt = { reprPrec := Hex.Nat.instReprPMinusOneAttempt.repr }

def Hex.Nat.instReprPMinusOneAttempt.repr : PMinusOneAttempt → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.instDecidableEqPMinusOneAttempt.decEq (x✝ x✝¹ : PMinusOneAttempt) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.instDecidableEqPMinusOneAttempt : DecidableEq PMinusOneAttempt

Equations

• Hex.Nat.instDecidableEqPMinusOneAttempt = Hex.Nat.instDecidableEqPMinusOneAttempt.decEq

def Hex.Nat.smoothBoundCap : Nat

Maximum supported stage-one bound. Stage primes come from the verified runtime sieve, independently of the committed table. Ordinary search policies may select smaller bounds.

Equations

• Hex.Nat.smoothBoundCap = 524288

def Hex.Nat.smoothBound (bound : Nat) : Nat

Clamp a requested stage-1 bound to the supported runtime range.

Equations

• Hex.Nat.smoothBound bound = min bound Hex.Nat.smoothBoundCap

@[simp]

theorem Hex.Nat.smoothBound_idem (bound : Nat) : smoothBound (smoothBound bound) = smoothBound bound

def Hex.Nat.pMinusOneStage1 (n base bound : Nat) : PMinusOneResult

One deterministic Pollard p - 1 stage-1 attempt. Invalid bases or moduli return noFactor; a gcd equal to the modulus is reported separately as whole. The effective smoothness bound is smoothBound bound, with every prime up to that bound included by the runtime sieve.

Equations

• Hex.Nat.pMinusOneStage1 n base bound = Hex.Nat.pMinusOneStage1Core✝ n base (Hex.Nat.smoothBound bound)

def Hex.Nat.pMinusOneStage1Counted (n base bound : Nat) (r : Rand) : PMinusOneAttempt

One counted, resumable Pollard p - 1 stage-1 attempt. The deterministic primitive consumes no generator words, but every call costs exactly one search attempt whether it returns noFactor, a proper factor, or whole.

Equations

• Hex.Nat.pMinusOneStage1Counted n base bound r = { result := Hex.Nat.pMinusOneStage1 n base bound, attempts := 1, rand := r }

theorem Hex.Nat.pMinusOneStage1_bound (n base bound : Nat) : pMinusOneStage1 n base bound = pMinusOneStage1 n base (smoothBound bound)

Requests beyond the supported runtime range are exactly capped.

theorem Hex.Nat.pMinusOneStage1_spec {n base bound d : Nat} (h : pMinusOneStage1 n base bound = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

Every reported factor is a dynamically checked proper divisor.

theorem Hex.Nat.pMinusOneStage1Counted_spec {n base bound d : Nat} {r : Rand} (h : (pMinusOneStage1Counted n base bound r).result = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

A proper factor returned through the counted boundary satisfies the same dynamically checked contract as the compatibility result.

def Hex.Nat.PMinusOne.stage2BoundCap : Nat

Independent ceiling for the continuation's prime enumeration.

Equations

• Hex.Nat.PMinusOne.stage2BoundCap = 4194304

def Hex.Nat.PMinusOne.stage2Bound (bound : Nat) : Nat

Never increase the requested continuation bound.

Equations

• Hex.Nat.PMinusOne.stage2Bound bound = min bound Hex.Nat.PMinusOne.stage2BoundCap

@[simp]

theorem Hex.Nat.PMinusOne.stage2Bound_idem (bound : Nat) : stage2Bound (stage2Bound bound) = stage2Bound bound

structure Hex.Nat.PMinusOne.Batch : Type

One flushed product and the recovery gcds actually executed.

• firstPrime : Nat
• lastPrime : Nat
• length : Nat
• gcd : Nat
• recovery : List Nat

def Hex.Nat.PMinusOne.instReprBatch.repr : Batch → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.PMinusOne.instReprBatch : Repr Batch

Equations

• Hex.Nat.PMinusOne.instReprBatch = { reprPrec := Hex.Nat.PMinusOne.instReprBatch.repr }

def Hex.Nat.PMinusOne.instDecidableEqBatch.decEq (x✝ x✝¹ : Batch) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.PMinusOne.instDecidableEqBatch : DecidableEq Batch

Equations

• Hex.Nat.PMinusOne.instDecidableEqBatch = Hex.Nat.PMinusOne.instDecidableEqBatch.decEq

structure Hex.Nat.PMinusOne.Event : Type

Untrusted diagnostics produced by one execution, including zero-attempt policy skips. Reasons distinguish invalid inputs, empty intervals, setup factors, stage factors, whole gcds, and ready residues.

• subject : Nat
• base : Option Nat
• requestedB1 : Nat
• effectiveB1 : Nat
• requestedB2 : Option Nat
• effectiveB2 : Option Nat
• outcome : PMinusOneResult
• reason : String
• candidates : Nat
• giantAdvances : Nat
• multiplications : Nat
• setupGcds : Nat
• batchGcds : Nat
• recoveryGcds : Nat
• batches : List Batch

def Hex.Nat.PMinusOne.instReprEvent.repr : Event → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.PMinusOne.instReprEvent : Repr Event

Equations

• Hex.Nat.PMinusOne.instReprEvent = { reprPrec := Hex.Nat.PMinusOne.instReprEvent.repr }

@[instance_reducible]

instance Hex.Nat.PMinusOne.instDecidableEqEvent : DecidableEq Event

Equations

• Hex.Nat.PMinusOne.instDecidableEqEvent = Hex.Nat.PMinusOne.instDecidableEqEvent.decEq

def Hex.Nat.PMinusOne.instDecidableEqEvent.decEq (x✝ x✝¹ : Event) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.PMinusOne.instInhabitedEvent : Inhabited Event

Equations

• Hex.Nat.PMinusOne.instInhabitedEvent = { default := Hex.Nat.PMinusOne.instInhabitedEvent.default }

structure Hex.Nat.PMinusOne.Stage1 : Type

The stage boundary retains its residue only after both gcds equal one.

• result : PMinusOneResult
• residue : Option Nat
• event : Event

@[instance_reducible]

instance Hex.Nat.PMinusOne.instReprStage1 : Repr Stage1

Equations

• Hex.Nat.PMinusOne.instReprStage1 = { reprPrec := Hex.Nat.PMinusOne.instReprStage1.repr }

def Hex.Nat.PMinusOne.instReprStage1.repr : Stage1 → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.PMinusOne.instDecidableEqStage1 : DecidableEq Stage1

Equations

• Hex.Nat.PMinusOne.instDecidableEqStage1 = Hex.Nat.PMinusOne.instDecidableEqStage1.decEq

def Hex.Nat.PMinusOne.instDecidableEqStage1.decEq (x✝ x✝¹ : Stage1) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.PMinusOne.start (n a B₁ : Nat) : Stage1

Execute stage 1 once, retaining the ready residue and its diagnostics.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.Nat.PMinusOne.start_result (n a B₁ : Nat) : (start n a B₁).result = pMinusOneStage1 n a B₁

def Hex.Nat.PMinusOne.primePower (q B₁ : Nat) : Nat

Largest power of the supplied prime within the effective first bound.

Equations

• Hex.Nat.PMinusOne.primePower q B₁ = Hex.Nat.stageExponent✝ q (Hex.Nat.smoothBound B₁)

theorem Hex.Nat.PMinusOne.primePower_spec {q B₁ : Nat} (hq : Prime q) (hb : q ≤ smoothBound B₁) : ∃ (e : Nat), primePower q B₁ = q ^ e ∧ q ^ e ≤ smoothBound B₁ ∧ ∀ (j : Nat), q ^ j ≤ smoothBound B₁ → j ≤ e

The loop computes the maximal prime power, including its full exponent, not just the product of small distinct primes.

def Hex.Nat.PMinusOne.exponent (B₁ : Nat) : Nat

The stage-1 exponent, used in statements only. Execution applies each prime power successively and never constructs this product.

Equations

• Hex.Nat.PMinusOne.exponent B₁ = (List.map (fun (x : Nat) => Hex.Nat.PMinusOne.primePower x B₁) (Hex.Nat.primesBelow (Hex.Nat.smoothBound B₁ + 1))).prod

theorem Hex.Nat.PMinusOne.start_residue {n a B₁ x : Nat} (h : (start n a B₁).residue = some x) : 4 ≤ n ∧ 1 < a ∧ a < n ∧ a.Coprime n ∧ x = a ^ exponent B₁ % n ∧ ((x + n - 1) % n).gcd n = 1

A ready residue is exactly the reduced power computed by stage 1, on valid coprime input after its final gcd equals one.

theorem Hex.Nat.PMinusOne.start_residue_of {n a B₁ : Nat} (hn : 4 ≤ n) (ha : 1 < a) (han : a < n) (hc : a.Coprime n) (hg : ((a ^ exponent B₁ % n + n - 1) % n).gcd n = 1) : (start n a B₁).residue = some (a ^ exponent B₁ % n)

Conversely, valid input and the two unit gcds always expose the residue.

theorem Hex.Nat.PMinusOne.start_ready {n a B₁ x : Nat} (h : (start n a B₁).residue = some x) : x < n ∧ x.gcd n = 1 ∧ ((x + n - 1) % n).gcd n = 1

Ready residues lie in range and are units; the adjacent residue also has gcd one, which is precisely the continuation boundary.

def Hex.Nat.PMinusOne.primes (B₁ B₂ : Nat) : List Nat

Complete ascending interval, including the small primes dividing 210.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.Nat.PMinusOne.mem_primes {q B₁ B₂ : Nat} : q ∈ primes B₁ B₂ ↔ Prime q ∧ smoothBound B₁ < q ∧ q ≤ stage2Bound B₂

theorem Hex.Nat.PMinusOne.primes_pairwise (B₁ B₂ : Nat) : List.Pairwise (fun (x1 x2 : Nat) => x1 < x2) (primes B₁ B₂)

theorem Hex.Nat.PMinusOne.primes_nodup (B₁ B₂ : Nat) : (primes B₁ B₂).Nodup

def Hex.Nat.PMinusOne.recover (n : Nat) (terms : List (Nat × Nat)) : PMinusOneResult × List Nat

Recover from retained terms in their original order. A whole leaf does not hide a proper divisor in a later leaf. Returns only executed gcds.

Equations

• Hex.Nat.PMinusOne.recover n terms = (Hex.Nat.PMinusOne.Checked.result✝ (Hex.Nat.PMinusOne.recoverCore✝ n terms).fst, (Hex.Nat.PMinusOne.recoverCore✝ n terms).snd)

theorem Hex.Nat.PMinusOne.recover_spec {n d : Nat} {terms : List (Nat × Nat)} (h : (recover n terms).fst = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

def Hex.Nat.PMinusOne.babies (n x : Nat) : Array Nat × Nat

All 210 babies and the next power, built by successive multiplication.

Equations

• Hex.Nat.PMinusOne.babies n x = Hex.Nat.PMinusOne.babyPowers✝ n x 210

@[simp]

theorem Hex.Nat.PMinusOne.babies_size (n x : Nat) : (babies n x).fst.size = 210

theorem Hex.Nat.PMinusOne.babies_step (n x : Nat) : (babies n x).snd = x ^ 210 % n

theorem Hex.Nat.PMinusOne.babies_get (n x j : Nat) (hj : j < 210) : (babies n x).fst[j] = x ^ j % n

def Hex.Nat.PMinusOne.powerCost (i : Nat) : Nat

Exact multiply count of the direct binary power used for the initial giant: one square per bit plus one multiply per set bit.

Equations

• Hex.Nat.PMinusOne.powerCost i = HexArith.bitLength i + (List.filter i.testBit (List.range (HexArith.bitLength i))).length

def Hex.Nat.PMinusOne.advance (n h : Nat) : Nat → Nat → Nat

Advance the giant through every intervening block.

Equations

• Hex.Nat.PMinusOne.advance n h 0 x✝ = x✝
• Hex.Nat.PMinusOne.advance n h fuel.succ x✝ = Hex.Nat.PMinusOne.advance n h fuel (x✝ * h % n)

theorem Hex.Nat.PMinusOne.advance_eq (n h k v : Nat) : advance n h k (v % n) = v * h ^ k % n

Each giant advance is exactly multiplication by another step power.

theorem Hex.Nat.PMinusOne.giant_mul_baby (n x q : Nat) (hn : 0 < n) : HexArith.powModBits (babies n x).snd (q / 210) n * (babies n x).fst[q % 210] % n = x ^ q % n

The division/remainder index map reconstructs every candidate power.

def Hex.Nat.PMinusOne.term (n v u : Nat) : Nat

Candidate subtraction after one baby/giant multiplication.

Equations

• Hex.Nat.PMinusOne.term n v u = (v * u % n + n - 1) % n

theorem Hex.Nat.PMinusOne.term_dvd_iff {n p a M x q v u : Nat} (hn : 0 < n) (hp : Prime p) (hd : p ∣ n) (hc : a.Coprime n) (hx : x = a ^ M % n) (ht : v * u % n = x ^ q % n) : p ∣ term n v u ↔ orderOf a p ∣ M * q

A candidate captures a prime divisor exactly when the base order divides its exponent. The hypothesis identifies the actual baby/giant product.

theorem Hex.Nat.PMinusOne.start_order_not_dvd {n p a B₁ x : Nat} (hp : Prime p) (hd : p ∣ n) (hx : (start n a B₁).residue = some x) : ¬orderOf a p ∣ exponent B₁

A stage-1 gcd of one rules out the order already dividing its exponent.

def Hex.Nat.PMinusOne.stage2 (n x B₁ B₂ : Nat) : PMinusOneResult

Total raw-residue continuation. Every factor exit validates range and divisibility; no provenance of the supplied residue is assumed.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Nat.PMinusOne.stage2_spec {n x B₁ B₂ d : Nat} (h : stage2 n x B₁ B₂ = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

theorem Hex.Nat.PMinusOne.stage2_bound (n x B₁ B₂ : Nat) : stage2 n x B₁ B₂ = stage2 n x (smoothBound B₁) (stage2Bound B₂)

def Hex.Nat.PMinusOne.search (n a B₁ B₂ : Nat) : PMinusOneResult

Standalone search preserves the stage boundary instead of recomputing it.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Nat.PMinusOne.search_spec {n a B₁ B₂ d : Nat} (h : search n a B₁ B₂ = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

@[simp]

theorem Hex.Nat.PMinusOne.start_residue_bound (n a B₁ : Nat) : (start n a (smoothBound B₁)).residue = (start n a B₁).residue

theorem Hex.Nat.PMinusOne.search_bound (n a B₁ B₂ : Nat) : search n a B₁ B₂ = search n a (smoothBound B₁) (stage2Bound B₂)

structure Hex.Nat.PMinusOne.Run : Type

Counted calls preserve deterministic state, including failed calls.

• result : PMinusOneResult
• attempts : Nat
• rand : Rand
• events : List Event

def Hex.Nat.PMinusOne.instReprRun.repr : Run → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Hex.Nat.PMinusOne.instReprRun : Repr Run

Equations

• Hex.Nat.PMinusOne.instReprRun = { reprPrec := Hex.Nat.PMinusOne.instReprRun.repr }

@[instance_reducible]

instance Hex.Nat.PMinusOne.instDecidableEqRun : DecidableEq Run

Equations

• Hex.Nat.PMinusOne.instDecidableEqRun = Hex.Nat.PMinusOne.instDecidableEqRun.decEq

def Hex.Nat.PMinusOne.instDecidableEqRun.decEq (x✝ x✝¹ : Run) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.PMinusOne.smoothPower (n x B₁ : Nat) (ps : List Nat) : Nat

The stage-1 exponentiation loop on prepared primes and a normalized base. Used to measure exponentiation separately from enumeration and setup.

Equations

• Hex.Nat.PMinusOne.smoothPower n x B₁ ps = Hex.Nat.raiseSmooth✝ n (Hex.Nat.smoothBound B₁) ps x

def Hex.Nat.PMinusOne.fromPrepared (n x B₁ B₂ : Nat) (qs : List Nat) (r : Rand) (keepBatches : Bool := true) : Run

The continuation on a prepared prime interval and saved residue. This measurement boundary omits the public raw-residue preflight and enumeration; callers supply the prepared data. Factor exits are still dynamically checked. The standalone APIs perform all preparation and remain the general entry points.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.Nat.PMinusOne.fromPrepared_spec {n x B₁ B₂ d : Nat} {qs : List Nat} {r : Rand} {keepBatches : Bool} (h : (fromPrepared n x B₁ B₂ qs r keepBatches).result = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

theorem Hex.Nat.PMinusOne.fromPrepared_result (n x B₁ B₂ : Nat) (qs : List Nat) (r : Rand) (keepBatches : Bool) : (fromPrepared n x B₁ B₂ qs r keepBatches).result = (fromPrepared n x B₁ B₂ qs r).result

Retaining batch details cannot change the prepared continuation result.

@[simp]

theorem Hex.Nat.PMinusOne.fromPrepared_attempts (n x B₁ B₂ : Nat) (qs : List Nat) (r : Rand) (keepBatches : Bool) : (fromPrepared n x B₁ B₂ qs r keepBatches).attempts = 1

@[simp]

theorem Hex.Nat.PMinusOne.fromPrepared_rand (n x B₁ B₂ : Nat) (qs : List Nat) (r : Rand) (keepBatches : Bool) : (fromPrepared n x B₁ B₂ qs r keepBatches).rand = r

def Hex.Nat.PMinusOne.stage2Counted (n x B₁ B₂ : Nat) (r : Rand) : Run

One continuation always costs exactly one semantic attempt.

Equations

• One or more equations did not get rendered due to their size.

def Hex.Nat.PMinusOne.searchCounted (n a B₁ B₂ : Nat) (r : Rand) : Run

Charge stage 1 once and the continuation only when actually invoked.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.Nat.PMinusOne.stage2Counted_result (n x B₁ B₂ : Nat) (r : Rand) : (stage2Counted n x B₁ B₂ r).result = stage2 n x B₁ B₂

@[simp]

theorem Hex.Nat.PMinusOne.searchCounted_result (n a B₁ B₂ : Nat) (r : Rand) : (searchCounted n a B₁ B₂ r).result = search n a B₁ B₂

theorem Hex.Nat.PMinusOne.stage2Counted_spec {n x B₁ B₂ d : Nat} {r : Rand} (h : (stage2Counted n x B₁ B₂ r).result = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

theorem Hex.Nat.PMinusOne.searchCounted_spec {n a B₁ B₂ d : Nat} {r : Rand} (h : (searchCounted n a B₁ B₂ r).result = PMinusOneResult.factor d) : 1 < d ∧ d < n ∧ d ∣ n

@[simp]

theorem Hex.Nat.PMinusOne.stage2Counted_attempts (n x B₁ B₂ : Nat) (r : Rand) : (stage2Counted n x B₁ B₂ r).attempts = 1

theorem Hex.Nat.PMinusOne.searchCounted_attempts (n a B₁ B₂ : Nat) (r : Rand) : (searchCounted n a B₁ B₂ r).attempts = 1 + match (start n a B₁).residue with | some val => if smoothBound B₁ < stage2Bound B₂ then 1 else 0 | none => 0

@[simp]

theorem Hex.Nat.PMinusOne.stage2Counted_rand (n x B₁ B₂ : Nat) (r : Rand) : (stage2Counted n x B₁ B₂ r).rand = r

@[simp]

theorem Hex.Nat.PMinusOne.searchCounted_rand (n a B₁ B₂ : Nat) (r : Rand) : (searchCounted n a B₁ B₂ r).rand = r

theorem Hex.Nat.PMinusOne.recover_success (n : Nat) (ts : List (Nat × Nat)) : (∃ (d : Nat), (recover n ts).fst = PMinusOneResult.factor d) ↔ ∃ (qt : Nat × Nat), qt ∈ ts ∧ 1 < qt.snd.gcd n ∧ qt.snd.gcd n < n

Recovery succeeds exactly when a retained leaf has a proper gcd.

def Hex.Nat.PMinusOne.batchProduct (n : Nat) (ts : List Nat) : Nat

Modular batch product, reducing after each multiplication as in the scan.

Equations

• Hex.Nat.PMinusOne.batchProduct n ts = List.foldl (fun (acc t : Nat) => acc * t % n) (1 % n) ts

theorem Hex.Nat.PMinusOne.batchProduct_eq (n : Nat) (ts : List Nat) : batchProduct n ts = ts.prod % n

theorem Hex.Nat.PMinusOne.batch_divisor {p n t : Nat} {ts : List Nat} (hp : Prime p) (hn : 0 < n) (hd : p ∣ n) (ht : t ∈ ts) (hpt : p ∣ t) : p ∣ (batchProduct n ts).gcd n ∧ 1 < (batchProduct n ts).gcd n

A captured prime divides the gcd at a reached batch flush.

def Hex.Nat.PMinusOne.flushBatch (n product : Nat) (buffer : Array (Nat × Nat)) : PMinusOneResult × Batch

Flush a retained batch; the scan calls the same implementation.

Equations

• Hex.Nat.PMinusOne.flushBatch n product buffer = (Hex.Nat.PMinusOne.Checked.result✝ (Hex.Nat.PMinusOne.flush✝ n product buffer).fst, (Hex.Nat.PMinusOne.flush✝ n product buffer).snd)

theorem Hex.Nat.PMinusOne.flush_factor {n product : Nat} {buffer : Array (Nat × Nat)} (hg : 1 < product.gcd n ∧ product.gcd n < n) : (flushBatch n product buffer).fst = PMinusOneResult.factor (product.gcd n)

A reached flush with a proper batch gcd returns that divisor immediately.

theorem Hex.Nat.PMinusOne.recover_whole (n : Nat) (ts : List (Nat × Nat)) : (recover n ts).fst = PMinusOneResult.whole ↔ ¬∃ (qt : Nat × Nat), qt ∈ ts ∧ 1 < qt.snd.gcd n ∧ qt.snd.gcd n < n

Without a proper leaf, recovery terminates with whole modulus.

theorem Hex.Nat.PMinusOne.batch_gcd {p r t : Nat} {ts : List Nat} (hr : Prime r) (ht : t ∈ ts) (hp : p ∣ t) (hs : ∀ (s : Nat), s ∈ ts → ¬r ∣ s) : (batchProduct (p * r) ts).gcd (p * r) = p

On a semiprime, a captured component and exclusion of the other component from every term force the batch gcd to equal the captured prime.

theorem Hex.Nat.PMinusOne.flush_recover {n product : Nat} {buffer : Array (Nat × Nat)} (hg : product.gcd n = n) : (flushBatch n product buffer).fst = (recover n buffer.toList).fst

Whole-product recovery is precisely the retained-leaf scan.