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 ⋯

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.

@[instance_reducible]

instance Hex.Nat.instDecidableEqPMinusOneAttempt : DecidableEq PMinusOneAttempt

Equations

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

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

Equations

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

def Hex.Nat.smoothBoundCap : Nat

Accepted stage-1 smoothness cap. It remains inside the complete table range, but is independent of later table-policy growth so search cost and retry-ladder coverage do not change as a side effect of a larger certification table.

Equations

• Hex.Nat.smoothBoundCap = 9999

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

Clamp a requested stage-1 bound to the complete committed-table 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, never an incomplete extension beyond the committed prime table.

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 complete prime-table 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.