Learning path

Each declaration appears after its prerequisites.

Green57.tripleKernel Uniform average over pairs (x₁, x₂) in G × G, with the third variable determined by the relation x₁ + x₂ + x₃ = g
Green57.baseΦ The generating family of functions for Φ(G)
Green57.baseΦ' The generating family of functions for Φ′(G), where the third kernel depends only on x₁ + x₂
Green57.Φ The space Φ(G) of "convex combinations" of kernels from baseΦ
Green57.Φ' The restricted space Φ′(G) of "convex combinations" of kernels from baseΦ'
Green57.functional The linear functional on G → ℂ given by φ ↦ Re ∑ g, a g * φ g
Green57.supportFn The support function of a set S with respect to a linear functional a: sup_{φ ∈ S} Re ⟨a, φ⟩
Green57.green_57.variants.z3_functional For $G = \mathbb{Z}/3\mathbb{Z}$ and the functional $a(0) = -1$, $a(1) = -3$, $a(2) = 3$, does the support function of $\Phi$ at $a$ strictly exceed that of $\Phi'$?
Green57.green_57.variants.z3 Do $\Phi(\mathbb{Z}/3\mathbb{Z})$ and $\Phi'(\mathbb{Z}/3\mathbb{Z})$ coincide?
Green57.green_57 Ben Green's Problem 57: the two structured-function spaces do not always coincide
Monomial A monomial as its vector of natural-number exponents
totalDeg Total degree is the sum of a monomial's exponents
OrderIdeal A finite set of monomials closed downward under divisibility
divisorsFinset All monomial divisors of one generator as a finite set
generatedOrderIdeal The finite order ideal generated by a finite set of monomials
IsMaximalIn Maximality inside an order ideal under monomial divisibility
maximalMonomials The finite set of maximal monomials of an order ideal
IsPure Purity means every maximal monomial has the same total degree
PureOrderIdeal An order ideal packaged with purity and a maximal monomial
typePO The type is the number of maximal monomials
socleDegree The shared total degree of a pure ideal's maximal monomials
pureOSequence Degree-by-degree counts of monomials in an order ideal
IsUnimodal Unimodality of a finite sequence h up to index e: there exists a peak j ≤ e such that h is weakly increasing on [0, j] and weakly decreasing on [j, e]
IsLogConcaveUpTo Log-concavity at every internal degree through a chosen endpoint
mXYZ The monomial xyz encoded as an exponent vector in 3 variables
mXZ2 The monomial xz^2 encoded as an exponent vector in 3 variables
GammaP1 The order ideal generated by the two monomials from P1
ProblemP1 P1 statement: the degree-counting values for the generated order ideal are (1, 3, 4, 2)
ProblemP2CoeffFormula P2 (coefficient-level): one-generator degree counts match the product-formula coefficients
ProblemP2Type1Unimodal P2 consequence: every type-1 pure O-sequence is unimodal
ProblemP2Type1LogConcave P2 consequence: every type-1 pure O-sequence is log-concave
ProblemP2 P2 statement, split into a coefficient-level formula plus two sequence consequences
ProblemP3 P3 statement: in codimension 3, first-half log-concavity up to e / 2
ProblemP4 P4 statement: codimension 3 and type 2 imply unimodality
ExistsNonLogConcavePureOSeq Helper predicate for open problems about non-log-concavity at fixed codimension/type
ProblemP5 P5: in codimension 3, every type-2 pure O-sequence is log-concave
ProblemP6 P6: for fixed r ≥ 5, every type-2 pure O-sequence in codimension r is unimodal
ProblemP7 P7: threshold existence for eventual log-concavity failure in codimension r
LCFailureThreshold Helper: t0 is a threshold after which all types admit a non-log-concave example
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_1.lean P8: least threshold for eventual log-concavity failure in codimension r
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_2.lean P8: least threshold for eventual log-concavity failure in codimension r
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_3.lean P8: least threshold for eventual log-concavity failure in codimension r
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_4.lean P8: least threshold for eventual log-concavity failure in codimension r
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean P8: least threshold for eventual log-concavity failure in codimension r
type_two_implies_two_maximals Type two produces exactly two distinct maximal monomials
ideal_carrier_eq_union A type-two pure ideal is the union of two principal divisor sets
exists_single_greater_var Equal-degree distinct triples can be oriented around one exceptional coordinate
reduced_monomial The residual monomial after removing the exceptional-coordinate shift
pureOSeq_decomposition Split the union's degree count into a principal sequence and a shifted residual sequence
h_seq Degree counts for the divisors of one monomial
diff The first backward difference of an integer-valued sequence
diff2 The second backward difference of an integer-valued sequence
L_seq@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean Count a diagonal slice of a two-dimensional exponent box
delta_L The first difference of a box slice is three threshold indicators
H_calc Assemble a three-dimensional degree slice from two-dimensional slices
H_eq_H_calc The box-count formula equals the actual monomial divisor count
delta_H_calc First difference of the three-dimensional box count
Z_calc The seven-threshold formula for discrete curvature
diff2_H_calc_eq_1 Verify the curvature formula at the first positive degree
diff2_H_calc_d_unfold Expand a positive second difference into two neighbouring slice differences
diff2_H_calc_L2 Normalize the shifted slice difference across its threshold
diff2_H_calc_eq_d Derive the seven-indicator curvature formula above the boundary
diff2_H_calc_eq The box count has the manuscript's curvature formula at every positive degree
Z_calc_le_one The curvature indicator expression never exceeds one
diff2_eq_func Pointwise equal sequences have equal second differences
diff2_h_seq_le_one A single monomial's degree-count sequence has second difference at most one
log_concave_core Reduce log-concavity to the only two positive second-difference cases
diff_eq Reconstruct a sequence value from its preceding value and first difference
diff2_eq Advance the first difference using the second difference
shifted_h_seq Shift a principal divisor sequence behind a degree threshold
diff_add First differences distribute over pointwise addition
diff2_add Second differences distribute over pointwise addition
H_seq The decomposed degree sequence for the two-generator order ideal
H_seq_eq_add Expose the decomposed Hilbert sequence as an explicit pointwise sum
diff2_h_seq_eq_Z_calc The actual monomial divisor sequence has the seven-indicator curvature
Z_calc_eq_zero_cases Classify where the curvature indicator can vanish
Z_calc_eq_one_cases Curvature one occurs only in the lower or upper box region
diff2_h_seq_eq_one_implies_pos Positive-degree curvature one forces a lower-or-upper region certificate
diff2_h_seq_eq_one_implies Curvature one has the same two-region classification at every degree
diff2_shifted_h_seq_eq_zero_lt A shifted divisor sequence has zero curvature before it begins
diff2_shifted_h_seq_le_one_lt The shifted summand obeys the curvature bound below its threshold
diff2_shifted_h_seq_eq_ge Above the threshold, shifting only translates the curvature index
diff2_shifted_h_seq_le_one_ge The shifted summand obeys the curvature bound after activation
diff2_shifted_h_seq_le_one Every shifted principal sequence has second difference at most one
diff2_shifted_h_seq_eq_one_implies Curvature one proves that the shifted term has activated
diff2_shifted_h_seq_eq_one_implies_eq Transfer residual curvature one to the unshifted reduced monomial
H_seq_eval_add Evaluate the decomposed sequence as principal plus shifted residual
diff_H_seq_eval_add Split the first difference of the decomposed sequence
diff2_H_seq_eq_add Split the second difference of the decomposed sequence
diff2_H_seq_le_two The decomposed two-generator sequence has second difference at most two
L_seq_le A two-variable degree slice has at most d+1 points
h_seq_le_binom A principal three-variable degree slice is bounded by all weak compositions
h_seq_pure_lower Exact quadratic formula in the lower box region
h_seq_pure_lower_diff First difference in the lower region is d+2
h_seq_symm A monomial divisor sequence is symmetric about half its total degree
h_seq_upper_bound_int Universal complementary quadratic upper bound
h_seq_pure_upper Exact complementary quadratic formula in the upper box region
h_seq_pure_upper_diff First difference in the upper region is negative complementary distance
int_add_eq_two_of_le_one A sum of two one-bounded integers reaches two only as one plus one
diff2_H_seq_eq_two_implies_both_one Curvature two means both component curvatures equal one
int_add_eq_one_of_le_one_cases A sum of two one-bounded integers equals one in exactly two zero-one cases
diff2_H_seq_eq_one_implies_cases Curvature one splits into the manuscript's principal or residual case
log_concave_algebra_lower_eval Lower-region quadratic counts satisfy the needed square bound
log_concave_weak_lower A lower-region principal term absorbs a bounded residual term
log_concave_algebra_upper_two Two upper-tail quadratics are dominated by the squared combined slope
log_concave_algebra_upper_eval The exact upper-upper region inequality
diff2_eq_one_reduction Shift a curvature-one square bound back by one degree
H_seq_identity Reconstruct H(d−1) from H(d+1) and two first differences
H_seq_diff2_reduction Shift a critical second-difference-one bound back one degree
H_seq_diff_eq The first difference of H is the sum of the two component differences
diff2_H_seq_eq_one_implies_inl_low Curvature-one case A closes immediately in the principal lower region
inl_high_H_eval_bounds Curvature-one case A satisfies the square bound in the principal upper region
diff2_H_seq_eq_one_implies_inl_high Case A upper region is discharged by the assembled evaluation bound
diff2_H_seq_eq_one_implies_inl Case A is complete after splitting the principal sequence into lower and upper regions
shifted_h_seq_eval_lower Exact value of the shifted residual in its lower region
diff_shifted_h_seq_eval_lower Exact first difference of the shifted residual in its lower region
inr_low_H_eval_bounds Case B lower region supplies the four value-and-slope bounds
inr_low_reduction_goal_helper Case B lower region proves the later-degree square bound
diff2_H_seq_eq_one_implies_inr_low Case B lower region transfers its later-degree bound back to d−1
inr_high_H_eval_bounds Case B upper region supplies the residual upper-tail formulas
inr_high_reduction_goal_helper Case B upper region proves the later-degree square bound
diff2_H_seq_eq_one_implies_inr_high Case B upper region transfers its later-degree bound back to d−1
diff2_H_seq_eq_one_implies_inr Case B is complete after classifying the translated residual sequence
diff2_H_seq_eq_one_implies The full curvature-one implication is the union of cases A and B
h1_high_h2_low_contradiction In the curvature-two case, principal-upper and residual-lower regions are incompatible
h1_low_h2_high_contradiction In the curvature-two case, a principal lower region is impossible after shift activation
diff2_H_seq_eq_two_implies_inr_inr The curvature-two upper-upper case satisfies the doubled square bound
h1_low_contradiction Shift activation alone rules out the principal lower region
diff2_H_seq_eq_two_implies The full curvature-two implication leaves only the upper-upper case
sum_log_concave_helper The principal-plus-shifted-residual sequence is log-concave
pureOSeq_eq_sum Identify the original pure O-sequence with the decomposed sequence
P5@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_5.lean Pure O-sequences of codimension 3 and type 2 are log-concave
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_7.lean P8: least threshold for eventual log-concavity failure in codimension r
ProblemP8@APNOutputs/AICollaborator/AlgebraicGeometry/hilbert_functions_8.lean P8: least threshold for eventual log-concavity failure in codimension r
WrittenOnTheWallII.GraphConjecture2.conjecture2 Graffiti.pc Conjecture 2: average local independence forces many spanning-tree leaves
BipartiteIso A graph isomorphism that preserves both sides of the bipartition
isBipartiteWith_deleteIncidenceSet Deleting the incidence set of a vertex keeps the graph bipartite with the same partitions
bipartiteDeck The multiset of incidence-deleted cards up to bipartite isomorphism
degreeProfile The multiset of degrees seen around a vertex
τ A vertex type combines its degree with its neighbors' degrees
R The typecount R(u, t) is the number of neighbors of u in rightV whose type τ equals t
doubleDeck The double deck is D_2(G) = {G - x - y := x ≠ y ∈ U ⊔ V} viewed unlabeled up t bipartite isomorphism
multiset_map_eq_implies_bij Equal unlabeled decks can be matched card by card
edgeCount_deleteIncidenceSet An incidence-deleted card loses exactly the degree of its isolated vertex
bipartiteDeck_determines_edgeCount Recover the original number of edges from the deck
degreeMultiset The unlabeled multiset of all vertex degrees
bipartiteDeck_determines_degreeMultiset Equal decks determine the complete degree distribution
count_degreeMultiset_deleteIncidenceSet_add The degree-count recurrence before and after deleting one incidence set
profile_eq_of_iso A matched card and global degrees determine the deleted vertex's degree profile
unique_isolated_of_2_connected The deleted vertex is the unique isolated vertex of its card
f_preserves_partitions Card matching preserves the named left and right parts
H_is_2_connected Matched incidence-deleted cards transfer 2-connectivity to H
typeDrop How a neighbor's type changes when one incident edge is removed
rightV_types_del_eq Split the opposite side into changed neighbor types and unchanged non-neighbor types
S_add_map_T_eq Matched cards give a cancellable equation for neighboring-type multisets
S_multiset_eq Descending degree induction recovers each neighboring-type multiset
typeProfile The multiset of full vertex types around one vertex
count_typeProfile_eq_one_iff_adj Distinct vertex types turn profile membership into adjacency
adjacency_preserved_left Type and type-profile preservation force adjacency preservation from the left side
type_preserving_bijection_is_iso Upgrade the card-matching bijection to a bipartite graph isomorphism
Conjecture2 Reconstructing a typed bipartite graph from its incidence-deletion deck
Arxiv.«1905.10899».F_operator Operator G(z) = (∇_x L(z), -∇_y L(z))
Arxiv.«1905.10899».step Anchored Simultaneous Gradient Descent z_{t+1} = z_t - α_t * G(z_t) + β_t * (z_0 - z_t)
Arxiv.«1905.10899».last_iterate_convergence Exact last-iterate O(1/T) convergence for anchored gradient descent-ascent
OpenQuantumProblem35.Config A computational-basis configuration of $n$ parties with local dimension $d$
OpenQuantumProblem35.StateVector A state vector in the computational basis, viewed as a finite-dimensional Hilbert space
OpenQuantumProblem35.mkStateVector Build a state vector from its computational-basis amplitudes
OpenQuantumProblem35.mkStateVector_apply A state built from amplitudes has those amplitudes as its coordinates
OpenQuantumProblem35.IsNormalized A state vector is normalized if it has $L^2$ norm $1$
OpenQuantumProblem35.isNormalized_iff_norm_sq_eq_one A state is normalized iff its squared $L^2$ norm is $1$
OpenQuantumProblem35.permuteConfig Permute the parties of a configuration
OpenQuantumProblem35.permuteConfig_refl The identity permutation leaves a configuration unchanged
OpenQuantumProblem35.permuteState Permute the parties of a state vector
OpenQuantumProblem35.permuteState_apply Evaluating a permuted state vector reads the amplitude at the permuted configuration
OpenQuantumProblem35.permuteState_refl The identity permutation leaves a state vector unchanged
OpenQuantumProblem35.combineFirst Merge a configuration on the first $m$ parties and a configuration on the remaining $n-m$ parties into a configuration on all $n$ parties
OpenQuantumProblem35.leftIndex The embedding of the first $m$ indices into $\mathrm{Fin}\, n$
OpenQuantumProblem35.rightIndex The embedding of the last $n-m$ indices into $\mathrm{Fin}\, n$
OpenQuantumProblem35.combineFirst_leftIndex Combining and then restricting to the left block recovers the left input
OpenQuantumProblem35.combineFirst_rightIndex Combining and then restricting to the right block recovers the right input
OpenQuantumProblem35.reducedDensityFirst The reduced density matrix obtained by tracing out the last $n-m$ parties
OpenQuantumProblem35.maximallyMixed The maximally mixed state on $m$ parties
OpenQuantumProblem35.HasMaximallyMixedFirstReduction A state has maximally mixed reduction on the first $m$ parties
OpenQuantumProblem35.IsAME A state $\psi$ is absolutely maximally entangled
OpenQuantumProblem35.ExistsAME Existence of an $\mathrm{AME}(n,d)$ state
OpenQuantumProblem35.not_existsAME_zero_dim No absolutely maximally entangled state exists in local dimension $0$ once $n \ge 1$
OpenQuantumProblem35.card_config The number of computational-basis configurations on $m$ parties of local dimension $d$ is $d^m$
OpenQuantumProblem35.maximallyMixed_apply The matrix entries of the maximally mixed state are diagonal and equal to the inverse subsystem dimension
OpenQuantumProblem35.uniformCoeff The common amplitude of the Bell and GHZ witnesses
OpenQuantumProblem35.IsConstantConfig A configuration is constant if all coordinates agree
OpenQuantumProblem35.constantConfig The constant configuration with value $a$
OpenQuantumProblem35.isConstantConfig_constantConfig Every constant configuration is constant
OpenQuantumProblem35.not_isConstantConfig_example A simple binary two-party configuration with different entries is not constant
OpenQuantumProblem35.diagonalState The diagonal $n$-party state: the uniform superposition over constant computational-basis strings
OpenQuantumProblem35.diagonalState_apply Evaluating the diagonal state returns the uniform coefficient on constant strings and 0 otherwise
OpenQuantumProblem35.bellState The standard $d$-dimensional Bell state
OpenQuantumProblem35.ghzState The standard $d$-dimensional GHZ state on $3$ parties
OpenQuantumProblem35.ghzState4 The standard $d$-dimensional GHZ state on $4$ parties
OpenQuantumProblem35.constantCompletion The completion function for constant-support states reduced to one party
OpenQuantumProblem35.constantConfig_injective On a nonempty index type, different constants give different constant configurations
OpenQuantumProblem35.isConstantConfig_iff_exists_constantConfig A configuration on a nonempty index type is constant iff it is equal to some constant configuration
OpenQuantumProblem35.uniformCoeff_norm_sq The squared norm of the uniform coefficient is the inverse local dimension
OpenQuantumProblem35.uniformCoeff_mul_star The squared norm of the uniform coefficient is the inverse local dimension
OpenQuantumProblem35.diagonalState_isNormalized For $n \ge 1$ and $d \ge 1$, the diagonal state is normalized
OpenQuantumProblem35.isConstantConfig_permute_iff Permuting the parties preserves the property of being a constant configuration
OpenQuantumProblem35.diagonalState_permute The diagonal state is invariant under permutations of the parties
OpenQuantumProblem35.constantCompletion_eq_iff A tail configuration equals the constant completion of $x$ iff all of its entries agree with the unique entry of $x$
OpenQuantumProblem35.eq_leftIndex_zero_or_eq_rightIndex Every index in $\mathrm{Fin}\, n$ is either the unique left index or a right index when the left block has size $1$
OpenQuantumProblem35.constantCompletion_injective The completion map for constant configurations is injective once $n \ge 2$
OpenQuantumProblem35.isConstantConfig_combineFirst_one_iff A configuration obtained by combining one entry with a tail is constant iff the tail is the constant completion of that entry
OpenQuantumProblem35.diagonalState_combineFirst_one The diagonal state on a split configuration is nonzero exactly on the graph of the constant completion map
OpenQuantumProblem35.reducedDensityFirst_of_completion A uniform superposition over the graph of an injective completion map has reduced density matrix $(c\overline c) I$ on the first subsystem
OpenQuantumProblem35.hasMaximallyMixedFirstReduction_of_completion The completion criterion gives a maximally mixed reduced state once the coefficient has the correct squared norm
OpenQuantumProblem35.diagonalState_hasMaximallyMixedFirstReduction_one The diagonal state has maximally mixed one-party reductions once $n \ge 2$
OpenQuantumProblem35.diagonalState_isAME_of_div_two_eq_one If $\lfloor n/2 \rfloor = 1$, then the diagonal state is $\mathrm{AME}(n,d)$ for every $d \ge 2$
OpenQuantumProblem35.bellState_isAME The standard Bell state is $\mathrm{AME}(2,d)$ for every physical local dimension $d \ge 2$
OpenQuantumProblem35.ghzState_isAME The standard $3$-party GHZ state is $\mathrm{AME}(3,d)$ for every physical local dimension $d \ge 2$
OpenQuantumProblem35.ame_2_exists The Bell state witnesses the existence of $\mathrm{AME}(2,d)$ for every local dimension $d \ge 2$
OpenQuantumProblem35.ame_3_exists The $3$-party GHZ state witnesses the existence of $\mathrm{AME}(3,d)$ for every local dimension $d \ge 2$
OpenQuantumProblem35.diagonalState_combineFirst_two_of_ne On $4$ parties, the diagonal state vanishes on any split configuration whose first two entries are different
OpenQuantumProblem35.ghzState4_not_ame Sanity check: the standard GHZ family on $4$ parties is not absolutely maximally entangled for any local dimension $d \ge 2$
OpenQuantumProblem35.ame_2_2_exists Source-backed benchmark statement: the Bell state witnesses the existence of an $\mathrm{AME}(2,2)$ state
OpenQuantumProblem35.ame_3_2_exists Source-backed benchmark statement: the three-qubit GHZ state witnesses the existence of an $\mathrm{AME}(3,2)$ state
OpenQuantumProblem35.ame_5_2_exists Source-backed benchmark statement: an $\mathrm{AME}(5,2)$ state exists
OpenQuantumProblem35.ame_6_2_exists Source-backed benchmark statement: an $\mathrm{AME}(6,2)$ state exists
OpenQuantumProblem35.ame_4_2_not_exists Source-backed benchmark statement: no $\mathrm{AME}(4,2)$ state exists; see Higuchi--Sudbery (2000) and the OQP page
OpenQuantumProblem35.ame_7_2_not_exists Source-backed benchmark statement: no $\mathrm{AME}(7,2)$ state exists; see Huber--Gühne--Siewert (2017) and the OQP page
OpenQuantumProblem35.ame_4_3_exists Source-backed benchmark statement: an $\mathrm{AME}(4,3)$ state exists; see Helwig et al
OpenQuantumProblem35.ame_4_6_exists Source-backed benchmark statement: an $\mathrm{AME}(4,6)$ state exists; see Rather et al
OpenQuantumProblem35.ame_7_6_open Open benchmark statement: does an $\mathrm{AME}(7,6)$ state exist?
OpenQuantumProblem35.ame_7_10_open Open benchmark statement: does an $\mathrm{AME}(7,10)$ state exist?
OpenQuantumProblem35.ame_8_4_open Open benchmark statement: does an $\mathrm{AME}(8,4)$ state exist?
OpenQuantumProblem35.ame_8_6_open Open benchmark statement: does an $\mathrm{AME}(8,6)$ state exist?
OpenQuantumProblem35.ame_8_10_open Open benchmark statement: does an $\mathrm{AME}(8,10)$ state exist?
OpenQuantumProblem35.ame_9_6_open Open benchmark statement: does an $\mathrm{AME}(9,6)$ state exist?
OpenQuantumProblem35.ame_9_10_open Open benchmark statement: does an $\mathrm{AME}(9,10)$ state exist?
OpenQuantumProblem35.ame_10_6_open Open benchmark statement: does an $\mathrm{AME}(10,6)$ state exist?
OpenQuantumProblem35.ame_10_10_open Open benchmark statement: does an $\mathrm{AME}(10,10)$ state exist?
OpenQuantumProblem35.ame_11_3_open Open benchmark statement: does an $\mathrm{AME}(11,3)$ state exist?
OpenQuantumProblem35.ame_11_4_open Open benchmark statement: does an $\mathrm{AME}(11,4)$ state exist?
OpenQuantumProblem35.ame_11_5_open An explicit absolutely maximally entangled state for 11 five-level parties
OpenQuantumProblem35.ame_11_6_open Open benchmark statement: does an $\mathrm{AME}(11,6)$ state exist?
OpenQuantumProblem35.ame_11_10_open Open benchmark statement: does an $\mathrm{AME}(11,10)$ state exist?
OpenQuantumProblem35.ame_12_5_open Open benchmark statement: does an $\mathrm{AME}(12,5)$ state exist?
OpenQuantumProblem35.ame_12_6_open Open benchmark statement: does an $\mathrm{AME}(12,6)$ state exist?
OpenQuantumProblem35.ame_12_10_open Open benchmark statement: does an $\mathrm{AME}(12,10)$ state exist?
OpenQuantumProblem35.oqp_35 Open Quantum Problem 35: classify all pairs $(n,d)$ with $n \ge 2$ and $d \ge 2$ for which an $\mathrm{AME}(n,d)$ state exists
MonochromaticQuantumGraph.V Vertices of $K_N$
MonochromaticQuantumGraph.EdgeN Edge label for $K_N$ with endpoint indices in Fin D
MonochromaticQuantumGraph.WeightsN Weights on edges
MonochromaticQuantumGraph.mkEdge Helper: build an EdgeN from endpoints and endpoint indices
MonochromaticQuantumGraph.vertices Ordered vertex list $[0, 1, \ldots, N-1]$
MonochromaticQuantumGraph.allEqualList Chain-equality along a list of vertices
MonochromaticQuantumGraph.allEqual All indices equal on Fin N (using the canonical ordered vertex list)
MonochromaticQuantumGraph.pmSumListAux Auxiliary perfect-matching sum on a vertex list, using a fuel parameter n for termination
MonochromaticQuantumGraph.pmSumList Perfect-matching sum on a list: run pmSumListAux with fuel = L.length
MonochromaticQuantumGraph.pmSumN The perfect-matching sum for $K_N$: use the canonical ordered vertex list vertices N
MonochromaticQuantumGraph.EqSystemN The monochromatic quantum graph equation system for $K_N$
MonochromaticQuantumGraph.instDecidableEqSystemN Instance: EqSystemN N D W is decidable when α has decidable equality
MonochromaticQuantumGraph.eqSystem4_d2_nat Sanity check over ℕ using native_decide
MonochromaticQuantumGraph.eqSystem4_d3_nat Sanity check over ℕ using native_decide
MonochromaticQuantumGraph.eqSystem6_d2_nat Sanity check over ℕ using native_decide
MonochromaticQuantumGraph.eqSystem4_no_solution_nnreal_ge4 Bogdanov: for $N = 4$ and all $D \geq 4$, no solution exists over $\mathbb{R}_{\geq 0}$
MonochromaticQuantumGraph.eqSystem_no_solution_nnreal_even_ge6_ge3 Bogdanov: for all even $N \geq 6$ and $D \geq 3$, no solution exists over $\mathbb{R}_{\geq 0}$
MonochromaticQuantumGraph.eqSystem_no_solution_even_ge4_d_eq_n_explicit No equal-dimension monochromatic quantum graph for even numbers of parties at least four
MonochromaticQuantumGraph.eqSystem6_no_solution_d3 For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d4 For $N = 6$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d5 For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_ge3 For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d3 For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d10 For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d3 For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d4 For $N = 10$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d5 For $N = 10$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d6 For $N = 10$ and $D = 6$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d7 For $N = 10$ and $D = 7$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d8 For $N = 10$ and $D = 8$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d9 For $N = 10$ and $D = 9$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem12_no_solution_d3 For $N = 12$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem14_no_solution_d3 For $N = 14$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem16_no_solution_d3 For $N = 16$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3 For all even $N \geq 6$ and $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{C}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d3_real For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d5_real For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_real For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d3_real For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d10_real For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d3_real For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_real For all even $N \geq 6$ and $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{R}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d3_int For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d5_int For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_int For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d3_int For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d10_int For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d3_int For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_int For all even $N \geq 6$ and $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$?
MonochromaticQuantumGraph.eqSystem4_no_solution_d4_trinary_int For $N = 4$ and $D = 4$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d3_trinary_int For $N = 6$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_d5_trinary_int For $N = 6$ and $D = 5$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem6_no_solution_ge3_trinary_int For $N = 6$ and all $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d3_trinary_int For $N = 8$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem8_no_solution_d10_trinary_int For $N = 8$ and $D = 10$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem10_no_solution_d3_trinary_int For $N = 10$ and $D = 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
MonochromaticQuantumGraph.eqSystem_no_solution_ge6_ge3_trinary_int For all even $N \geq 6$ and $D \geq 3$, does there exist no solution to the monochromatic quantum graph equation system over $\mathbb{Z}$ with weights in $\{-1, 0, 1\}$?
Erdos12.IsGood Property P: no member divides the sum of two larger distinct members
Erdos12.exists_prime_bounded Find a controlled next prime
Erdos12.q A recursively chosen increasing sequence of primes
Erdos12.q_prime Every chosen modulus is prime
Erdos12.q_gt Successive chosen primes strictly increase
Erdos12.q_ge_5 Every chosen prime is at least five
Erdos12.K The accumulated modulus from all earlier primes
Erdos12.P The full period for block $m$
Erdos12.M The rapidly growing scale separating the blocks
Erdos12.MyGoodSet The Lean proof's congruence-block witness
Erdos12.K_pos The accumulated modulus is positive
Erdos12.P_pos The joint period is positive
Erdos12.M_succ Successive block scales differ by an eighth power
Erdos12.pow_eight_le Eighth powers preserve order on naturals
Erdos12.M_increasing Consecutive block scales are more than a factor of two apart
Erdos12.M_monotone Block scales are monotone
Erdos12.m_le_of_lt Numerical order respects block order
Erdos12.q_dvd_K Every earlier prime is absorbed into later accumulated moduli
Erdos12.mod_q_of_lt A later block is $1$ modulo every earlier block prime
Erdos12.q_div_a Zero remainder gives divisibility by the block prime
Erdos12.K_mod_3 Every accumulated modulus is divisible by three
Erdos12.mod_3_eq_1 The block residue forces residue one modulo three
Erdos12.prime_dvd_K Prime factors of an accumulated modulus precede the current prime
Erdos12.K_q_coprime The accumulated modulus and the new prime are coprime
Erdos12.K_ge_3 The accumulated modulus is never smaller than three
Erdos12.P_dvd_M The joint period divides the block scale
Erdos12.K_dvd_P The accumulated modulus divides the joint period
Erdos12.q_dvd_P The current prime divides the joint period
Erdos12.K_dvd_M The accumulated modulus divides the block scale
Erdos12.q_dvd_M The current prime divides the block scale
Erdos12.pow_four_le Fourth powers preserve order on naturals
Erdos12.r_val A Chinese-remainder solution for the two block residues
Erdos12.x_val The canonical block offset modulo the full period
Erdos12.x_val_lt_P Choose the canonical residue below one period
Erdos12.x_val_mod_K The canonical offset is $1$ modulo the accumulated modulus
Erdos12.x_val_mod_q The canonical offset is $0$ modulo the block's new prime
Erdos12.exists_good_in_block Every block contains at least one admissible residue
Erdos12.M_gt_m Block scales eventually dominate their indices immediately
Erdos12.my_good_set_infinite The congruence-block witness is infinite
Erdos12.my_good_set_is_good The congruences exclude every forbidden divisibility triple
Erdos12.f_val Enumerate the arithmetic progression inside one block
Erdos12.P_le_M One period fits inside its block scale
Erdos12.q_bound_le An exponential upper bound for the chosen primes
Erdos12.P_lower_bound An exponential lower bound for the joint periods
Erdos12.q_pow_four_bound_helper Compare the explicit exponential envelopes
Erdos12.q_pow_four_bound The next prime grows slowly relative to the current period
Erdos12.f_val_bound Progression offsets occupy at most half a block
Erdos12.P_le_M_half Even one full period fits inside half a block
Erdos12.f_val_in_good_set Every bounded progression index produces a valid block member
Erdos12.f_val_inj Distinct progression indices give distinct block members
Erdos12.finset_coe_ncard Set cardinality agrees with finite-set cardinality
Erdos12.good_set_inter_finite A bounded slice of the witness set is finite
Erdos12.count_interval Each block contains at least half a fourth power of points
Erdos12.density_ineq_x A floor-division estimate beyond ten
Erdos12.density_ineq_x_sq A squared floor-division estimate beyond twenty
Erdos12.density_helper_pow The density envelopes separate exponentially
Erdos12.density_ineq_q_helper Compare prime-growth and period-growth envelopes
Erdos12.density_ineq_q Bound the fifth power of the next prime
Erdos12.density_ineq The next scale is controlled by the square of the block count
Erdos12.exists_M_interval Locate every sufficiently large $N$ between consecutive block scales
Erdos12.density_ratio_bound Convert a square count bound into a normalized density bound
Erdos12.density_bound_N A uniform lower bound for every sufficiently large cutoff
Erdos12.sum_P_pow_four Earlier fourth-power periods are dominated by the latest one
Erdos12.dvd_sub_of_mod_eq Equal residues make the difference divisible by the modulus
Erdos12.div_eq_implies_sub_lt Equal quotient cells are narrower than one period
Erdos12.good_set_inj A block and quotient cell contain at most one admissible number
Erdos12.block_unique A number has only one compatible block index
Erdos12.g_block Select the scale interval containing a number
Erdos12.g_block_spec The selected block really contains the number
Erdos12.my_good_set_has_block Every witness-set member lies between consecutive scales
Erdos12.g_val Encode a good-set member by its block and progression cell
Erdos12.g_val_inj The block-and-cell coordinate is injective on the witness set
Erdos12.target_set A finite coordinate box for all earlier blocks
Erdos12.target_set_card Bound the finite code space for all earlier blocks
Erdos12.g_val_maps_to Every early witness-set member has a bounded block code
Erdos12.count_upper_bound The witness count at a block scale is at most twice a fourth power
Erdos12.exists_f_le_two The normalized count is at most two infinitely often
Erdos12.bdd_above_of_frequently_le A frequent upper bound caps every eventual lower bound
Erdos12.my_good_set_density The normalized counting function has positive lower limit
Erdos12.target_theorem_0@APNOutputs/ErdosProblems/erdos_12.parts.i.lean Erdős problem 12(i): a dense infinite set avoiding the divisibility pattern
Erdos12.target_theorem_0@APNOutputs/ErdosProblems/erdos_12.parts.ii.lean Erdős problem 12(ii): no universal power saving for every admissible set
Erdos125.zero_in_A Zero belongs to the base-3 digit set
Erdos125.zero_in_B Zero belongs to the base-4 digit set
Erdos125.zero_in_A_plus_B The sumset contains zero
Erdos125.A_max_k The largest k-digit base-3 number using only zero and one
Erdos125.B_max_m The largest m-digit base-4 number using only zero and one
Erdos125.A_B_gap A common digit-scale gap in the sumset
Erdos125.A_decomp Split a base-3 digit string into top and bottom blocks
Erdos125.B_decomp Split a base-4 digit string into top and bottom blocks
Erdos125.log_ratio_irrational The logarithms of four and three have irrational ratio
Erdos125.exists_small_pos_lin_comb_help A positive irrational has arbitrarily small positive integer linear combinations
Erdos125.exists_small_pos_lin_comb Make m log 4 minus k log 3 positive and arbitrarily small
Erdos125.exists_small_pos_lin_comb_large_k Obtain the logarithmic approximation beyond any requested scale
Erdos125.dirichlet_approx Choose nearby powers of three and four at a large scale
Erdos125.hz_eq_lemma Rewrite a sum using the smaller common scale
Erdos125.scale_step Reduce density by a fixed factor at a larger scale
Erdos125.density_multi_scale Iterate the contraction through arbitrarily many scales
Erdos125.limit_11_12 Powers of eleven twelfths fall below every positive threshold
Erdos125.density_tends_to_zero Find a cutoff with density below any positive epsilon
Erdos125.target_theorem_0 Erdős problem 125: the base-3 plus base-4 digit sumset has zero lower density
Erdos138.monoAP_guarantee_set Interval lengths that force a monochromatic arithmetic progression
Erdos138.monoAPNumber The least interval length that forces a monochromatic progression
Erdos138.W The two-colour van der Waerden number W(k)
Erdos138.HasMonoAP An explicit monochromatic arithmetic progression inside [1,N]
Erdos138.ap_must_end Any newly created (k+1)-progression must end at the new point
Erdos138.extend_one_step At least one colour safely extends the progression-free interval
Erdos138.has_mono_ap_ext The progression predicate depends only on colours inside [1,N]
Erdos138.extend_j_steps Iterating the safe extension for up to k new points
Erdos138.extend_coloring Extend a finite interval colouring to every natural number
Erdos138.ap_equiv Indexing a positive-step arithmetic progression by Fin k
Erdos138.card_ap_eq_k A positive-step k-term progression has exactly k elements
Erdos138.card_ap_pos_d More than one progression term forces a positive step
Erdos138.contains_mono_ap_imp Convert Mathlib's set-valued progression witness to HasMonoAP
Erdos138.imp_contains_mono_ap Convert HasMonoAP back to Mathlib's interval predicate
Erdos138.not_guarantee_extend A countercolouring for k extends to one for k+1
Erdos138.not_in_set_of_lt_sInf Nothing below a natural-number infimum belongs to the set
Erdos138.U_limit_color The ultrafilter-limit colour at one integer
Erdos138.U_limit_color_mem The chosen limit colour occurs on a U-large set of indices
Erdos138.U_inter_mem Finitely many progression positions agree with the limit colouring together
Erdos138.U_atTop_mem_large A U-large set contains arbitrarily large indices
Erdos138.W_is_nonempty Van der Waerden forcing lengths exist for every progression length
Erdos138.Icc_subset_succ The interval [1,N] sits inside [1,N+1]
Erdos138.guarantee_upward_closed Once an interval length guarantees a progression, every larger one does
Erdos138.not_in_guarantee_lt_sInf A non-guaranteeing length lies below the van der Waerden number
Erdos138.W_not_guarantee One less than a positive van der Waerden number is a counterexample length
Erdos138.W_diff_bound_gt0 The quantitative gap bound when W(k) is positive
Erdos138.W_diff_ge_k The gap bound for every natural k
Erdos138.W_diff_ge_k_all The pointwise lower bound used to prove divergence
Erdos138.target_theorem_0 Erdős problem 138: consecutive van der Waerden numbers separate without bound
Erdos152.f Define f n to be the minimum of |{s | s - 1 ∉ A + A, s ∈ A + A, s + 1 ∉ A + A}| as A ranges over all Sidon sets of size n
Erdos152.target_theorem_0 Erdős problem 152: Sidon sumsets have quadratically many isolated sums
Erdos26.IsThick A sequence of naturals $(a_i)$ is thick if their sum of reciprocals diverges: $$ \sum_i \frac{1}{a_i} = \infty $$
Erdos26.MultiplesOf The set of multiples of a sequence $(a_i)$ is $\{na_i | n \in \mathbb{N}, i\}$
Erdos26.IsBehrend A sequence of naturals $(a_i)$ is Behrend if almost all integers are a multiple of some $a_i$
Erdos26.IsWeaklyBehrend A sequence of naturals $(a_i)$ is weakly Behrend with respect to $\varepsilon \in \mathbb{R}$ if at least $1 - \varepsilon$ density of all numbers are a multiple of $A$
Erdos26.target_theorem_0 Erdős problem 26 variant: a thick sequence whose shifted multiples stay sparse
Erdos741.S_x The lower observation scale in the Erdős 741 counterexample
Erdos741.S_y The upper endpoint: ten times the lower scale
Erdos741.S_C The sparse union of fat intervals that drives density oscillation
Erdos741.split1 Put each binary digit into the 0-or-1 part of a base-four number
Erdos741.split2 Put the complementary 0-or-2 contribution into the second base-four stream
Erdos741.B1 The carry-free base-four set with digits 0 and 1
Erdos741.B2 The complementary carry-free base-four set with digits 0 and 2
Erdos741.SandorA The strict-natural-density counterexample set
Erdos741.B1_sum_ncard Below 4^d, the first self-sumset has at most 3^d values
Erdos741.B2_sum_ncard The second carry-free self-sumset obeys the same 3^d bound
Erdos741.B1_add_B2_eq_univ The two complementary digit sets add to every natural number
Erdos741.SandorA_add_SandorA_eq_univ The counterexample's full self-sumset is all naturals
Erdos741.SandorA_has_pos_density The full sumset has natural density one
Erdos741.B_partition_alpha_bound Any convergent two-colour split pays a cross-term density deficit
Erdos741.sandor_cross_sums A fat interval forces almost twice its size in monochromatic sums
Erdos741.SandorA_fluctuation_bounds Positive limiting densities would still oscillate by a fixed amount
Erdos741.SandorA_no_valid_partition No disjoint two-part split can give both self-sumsets positive natural density
Erdos741.exists_erdos_counterexample The explicit witness refuting the strict-natural-density statement
Erdos741.target_theorem_0@APNOutputs/ErdosProblems/erdos_741.parts.i.lean Erdős problem 741(i): strict natural density is false, upper density is true
Erdos741.target_theorem_0@APNOutputs/ErdosProblems/erdos_741.parts.ii.lean Erdős problem 741(ii): an order-two basis with no syndetic two-part split
Erdos846.NonTrilinearFor We say a subset A of points in the plane is ε-non-trilinear if any subset B of A, contains a non-trilinear subset C of size at least ε|B|
Erdos846.WeaklyNonTrilinear We say a subset A of points in the plane is weakly non-trilinear if it is a finite union of non-trilinear sets
Erdos846.target_theorem_0 Erdős problem 846: robustly non-collinear sets need not split into finitely many general-position sets
A224515 A224515: $a(n) = \text{least } k \text{ such that } \sqrt{k^2 \operatorname{XOR} (k+1)^2} = 2n+1, \text{ } a(n) = -1 \text{ if there is no such } k$
a@APNOutputs/OEIS/A309132_conjecture_carmichael.lean A309132: a(n) is the denominator of F(n) = A027641(n-1)/n + A027642(n-1)/n^2
is_carmichael_number Definition of a Carmichael number $n$: a composite number s.t
is_composite Helper definition for "composite number"
A382590_pair Helper function for A382590, computing the pair $(a(n), b(n))$ such that: $a(n) = a(n-1)b(n-2) + a(n-2)b(n-1)$ $b(n) = a(n-1)b(n-2) - a(n-2)b(n-1)$
A382590 A382590
kth_prime_factor The k-th prime factor of an integer n (where k>=1), counted with multiplicity
a@APNOutputs/OEIS/a091669_conjecture_primitive_root.lean A091669: $a(n) = \frac{2^{n-1}}{n!} \prod_{k=1}^{n-1} (2^k-1)$
a@APNOutputs/OEIS/a325046_odd_terms_at_k_times_k_plus_1.lean A325046: G.f.: $\sum_{n \ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 - x^{n+1})^{n+1}}$
a@APNOutputs/OEIS/oeis_103311_conjecture_0.lean A103311: A transform of the Fibonacci numbers
a@APNOutputs/OEIS/oeis_108_conjecture_2.lean A000108 Catalan numbers: C(n) = binomial(2n,n)/(n+1)
catalan_reciprocal_sum The sum $\sum_{i=j}^k \frac{1}{a(i)}$ of reciprocals of Catalan numbers
oeis_108_index_cond The index condition on $(j, k)$ from the conjecture: $0 < \min\{2,k\} \le j \le k$
frac_part The fractional part of a rational number, viewed as a real number
a@APNOutputs/OEIS/oeis_113254_conjecture_0.lean A113254: Corresponds to $m = 8$ in a family of 4th-order linear recurrence sequences
a@APNOutputs/OEIS/oeis_175386_conjecture_0.lean A175386: $a(n)$ is the denominator of the sum $$\sum_{i=1}^n \frac{1}{i} \binom{2n-i-1}{i-1}$$
S@APNOutputs/OEIS/oeis_175386_conjecture_0.lean The sum which A175386 $a(n)$ is the denominator of
set_prod The set of all products of elements from a Finset S
a@APNOutputs/OEIS/oeis_194806_conjecture_0.lean A194806: Size of the smallest subset $S$ of $T = \{1,2,3,\dots,n\}$ such that $S \cdot S$ contains $T$, where $S \cdot S$ is the set of all products of elements of $S$
A227582_base The sequence $b_n$ such that $A227582(n) = b_{n-1}$ for $n \ge 1$
a@APNOutputs/OEIS/oeis_227582_conjecture_0.lean A227582: Expansion of $(2+3*x+2*x^2+2*x^3+3*x^4+x^5-x^6)/(1-2x+x^2-x^5+2*x^6-x^7)$
A005259' A005259: The auxiliary sequence used for the Hankel matrix, defined as $$\sum_{k=0}^n \binom{n}{k}^2 \binom{n+k}{k}^2$$
a@APNOutputs/OEIS/oeis_228143_conjecture_1.lean A228143: Determinant of the $(n+1) \times (n+1)$ Hankel-type matrix with $(i,j)$-entry equal to A005259$(i+j)$ for all $i,j = 0,\dots,n$
OGF_A_scaled The power series $A(x/3) = \sum_{n=0}^\infty \frac{a(n)}{3^n} x^n$ over ℚ
a@APNOutputs/OEIS/oeis_243106_conjecture_0.lean A243106: The sequence $$a(n) = \sum_{k=1}^n (-1)^{\operatorname{isprime}(k)} 10^k$$ where the sign is $-1$ if $k$ is prime, and $1$ if $k$ is not prime
a@APNOutputs/OEIS/oeis_248802_conjecture_0.lean A248802: Smallest prime factor of $2^{(2^n+2)} + 3$
a@APNOutputs/OEIS/oeis_248802_conjecture_4.lean A248802: Smallest prime factor of $2^{(2^n+2)} + 3$
covered_by_C1 An index k is covered by Conjecture 1 if k = 10m + 2 for some m >= 0, predicting a(k)=67
covered_by_C2 An index k is covered by Conjecture 2 if k = 36m + 16 for some m >= 0, and m is not 1 mod 5, predicting a(k)=271
covered_by_C3 An index k is covered by Conjecture 3 if k = 84m + 22 for some m >= 0, and m is not 0 mod 5, predicting a(k)=523
A256012 A256012: Number of partitions of $n$ into distinct parts that are not squarefree
ca_rule_167 The rule function for Rule 167
ca_state The state of the Rule 167 elementary cellular automaton at time $t$ and position $x$
middle_column_bit The sequence of bits forming the middle column of the CA pattern, $C_{t, 0}$
a@APNOutputs/OEIS/oeis_267581_conjecture_0.lean A267581: Decimal representation of the middle column of the "Rule 167" elementary cellular automaton starting with a single ON (black) cell
oeis_floor_term The floor term in the conjectured recurrence relation for A267581
tribonacci The Tribonacci numbers $T_n$ (A000073)
a@APNOutputs/OEIS/oeis_271591_conjecture_0.lean A271591: Second most significant bit of the tribonacci number A000073(n)
A278070 A278070: $a(n) = \text{hypergeometric}([n, -n], [], -1)$
A282779 A282779: Period of cubes mod $n$
period_of_power_mod The length of the minimal positive period of the sequence $k^p \pmod n$
A289411 A289411: $\mathrm{a}(n) = \sum_{k=0}^n \mathrm{sign}(\mathrm{A007953}(5k) - \mathrm{A007953}(k))$
a@APNOutputs/OEIS/oeis_2897_conjecture_0.lean The sequence $a(n)$ is defined by $a(n) = \binom{2n}{n}^3$
xyz_pow_n The finsupp corresponding to the monomial $x^n y^n z^n$
P_n The polynomial $P_n(X, Y, Z) = (1 + X + Y + Z)^{2n} (1 + X + Y - Z)^n (1 + X - Y + Z)^n$
A306424_condition A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each $b = 3..k-1$ never contains more than two distinct digits
a@APNOutputs/OEIS/oeis_306424_conjecture_0.lean The sequence A306424: Numbers $k$ such that the base $b$ expansion of $k$ for each $b = 3..k-1$ never contains more than two distinct digits
a@APNOutputs/OEIS/oeis_307865_conjecture_0.lean A307865: $a(n)$ is the number of natural bases $b < 2n+1$ such that $b^n \equiv -1 \pmod{2n+1}$
IsAbsoluteEulerPseudoprime A natural number $m > 1$ is an absolute Euler pseudoprime if it is composite and for all $b$ coprime to $m$, $b^{(m-1)/2} \equiv \pm 1 \pmod m$
a@APNOutputs/OEIS/oeis_323557_conjecture_0.lean A323557: G.f.: $\sum_{n\ge 0} x^n \cdot \frac{(1 + x^n)^n}{(1 + x^{n+1})^{n+1}}$
A340737 A340737: Numerators of a sequence of fractions converging to $e$
A340738 A340738: Denominators of a sequence of fractions converging to $e$
r_const The constant $r = (2 + \sqrt{5})/2$
r_sq The constant $r^2$
a@APNOutputs/OEIS/oeis_341254_conjecture_0.lean A341254: $a(n) = \lfloor r \cdot \lfloor r \cdot n \rfloor \rfloor$, where $r = (2 + \sqrt{5})/2$
continued_fraction_denominator Helper function for A363347, which computes the denominator $R_k(n)$ of the continued fraction expression
A363347 A363347: Denominator of the continued fraction
continued_fraction_tail Recursive function to compute $A_k(n)$, the denominator tail $k - \frac{k+1}{A_{k+1}(n)}$
continued_fraction_val The total value of the continued fraction $C_n$
a@APNOutputs/OEIS/oeis_372761_conjecture_2.lean A372761: Denominator of the continued fraction $$ \frac{1}{2 - \frac{3}{3 - \frac{4}{4 - \frac{5}{\dots - \frac{n-1}{(n-1) - \frac{n}{n+4}}}}}} $$
A051293 A051293: Number of nonempty subsets of $\{1, 2, 3, \dots, n\}$ whose elements have an integer average
P_poly@APNOutputs/OEIS/oeis_51293_conjecture_0.lean S_real n k is the number of $k$-element subsets of $\{1, 2, \dots, n\}$ whose sum is divisible by $k$
target_theorem_0@APNOutputs/OEIS/oeis_51293_conjecture_0.lean OEIS A051293: a six-term asymptotic expansion for subsets with integer average
reverse_nat The number whose digits in base 10 are $n$'s digits reversed
a@APNOutputs/OEIS/oeis_62567_conjecture_0.lean A062567: First multiple of $n$ whose reverse is also divisible by $n$, or 0 if no such multiple exists
digits_lt_10 Helper lemmas for finite cases
a_gt_4 Helper lemma for the general inequality when n >= 5
a@APNOutputs/OEIS/oeis_A028859_conjecture_1.lean A028859 (OEIS): $a(n+2) = 2 \cdot a(n+1) + 2 \cdot a(n)$; $a(0) = 1$, $a(1) = 3$
A258667_inner_sum The inner sum of the formula used in A258667: $$\sum_{\max(k-n+5, 0) \le j \le \min(k,4)} \binom{8-j}{j}\binom{2n-k+j-10}{k-j}$$
A258667 A258667: A total of $n$ married couples, including a mathematician M and his wife, are to be seated at the $2n$ chairs around a circular table, with no man seated next to his wife
menage_denom_term The denominator term $k! (n-1)_k$ represented as a Real number
A258667_asymptotic_sum_part The infinite series part of the asymptotic expansion: $\sum_{k \ge 1} \frac{(-1)^k}{k!(n-1)_k}$
A258667_asymptotic_term The proposed asymptotic expression for A258667(n)
a@APNOutputs/OEIS/oeis_a211417_conjecture_specific.lean Integral factorial ratio sequence: $$a(n) = \frac{(30n)! n!}{(15n)! (10n)! (6n)!}$$
divisor_product The product term in the denominator of the general conjecture
a@APNOutputs/OEIS/oeis_a237271_conjecture_2.lean A237271: Number of parts in the symmetric representation of $\sigma(n)$
num_2_dense_sublists Number of maximal contiguous sublists of divisors of n where each adjacent pair (d_k, d_{k+1}) satisfies d_{k+1} <= 2 * d_k
a@APNOutputs/OEIS/oeis_a300997_finite_difference_is_one_or_two.lean A300997
a051403 Auxiliary sequence A051403, defined as $$\frac{(n+2) \sum_{k=0}^n k!}{2}$$
a@APNOutputs/OEIS/oeis_a363102_conjecture_1.lean A363102: Denominator of the continued fraction $1/(2-3/(3-4/(4-5/(...(n-1)-n/(-2)))))$
a@APNOutputs/OEIS/oeis_a368692_conjecture_integrality.lean A368692: $$a(n) = \frac{(12n + 6)! \cdot (6n + 9)!}{108 \cdot (4n + 2)! \cdot (2n + 3)! \cdot ((6n + 5)!)^2}$$ It is conjectured that $a(n)$ are integers
reduced_quotient_directed_idempotents Helper lemma: quotient of a reduced ring by an idempotent is reduced
NormalDomain.powerSeries The power series ring over a Noetherian normal domain is a normal domain