Source-pinned research

Research proof index

Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.

This index contains 423 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

423 results

Clear filters
Project-declaredLean 4.31.0

Joint Agreement implies lin Span proximity

ProximityGap.jointAgreement_implies_linSpan_proximity

Plain-language statement

Generalisation of jointAgreement_implies_second_proximity to an arbitrary word stack over a submodule code. If a stack W : Fin k → ι → F jointly agrees with a submodule C ⊆ ι → F, then every element of the linear span of the stack is δ-close to C. The pointwise case W i ∈ C is the special case x = W i (choose coefficients c to be the i-th...

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Prob coeff eq prob affine

ProximityGap.prob_coeff_eq_prob_affine

Plain-language statement

The coefficient-parameterised probability equals the subtype probability. The map r ↦ u₀ + ∑ rᵢ • dᵢ has constant-cardinality fibers (cosets of the kernel of the linear part), so pushforward of uniform gives uniform.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Rel Dist From Code smul eq

ProximityGap.relDistFromCode_smul_eq

Plain-language statement

Relative distance to a submodule is invariant under scaling by a unit: δᵣ(z • u, V) = δᵣ(u, V) for z ≠ 0 and V a submodule. Key step in BCIKS20 §6.3 (Step 1c).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

E le dist over 3

ProximityToRS.e_le_dist_over_3

Plain-language statement

Lemma 4.4, [AHIV22] (mutual-exclusion corollary). Either all points on the affine line are e-close to the Reed–Solomon code, or at most ‖RS‖₀ points are. The assumptions v ≠ 0 and ‖RS‖₀ < |F| are necessary for mutual exclusion: if v = 0, the affine line degenerates to a singleton and the two branches can hold simultaneously.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Ps coprime case constant

ps_coprime_case_constant

Plain-language statement

If A and B are coprime and agree on sufficiently many lines, then A is constant.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Ps exists p

ps_exists_p

Plain-language statement

Main existence: if B/A agrees with low-degree quotients on enough lines, then A ∣ B.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record